[SMT-COMP] Incorrect status for one QF_AUFBV benchmark (non-incremental)

[Mathias Preiner]

Hi all,

The following QF_AUFBV benchmark has an incorrect status:

non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_NPT_1.smt2

The benchmark says it is unsat, however, Z3 and Boolector both say sat.
When the model is asserted also CVC4 and Yices report sat.

I already fixed the benchmark in the corresponding SMT-LIB repository.

@Clark: Can you please update the benchmark on StarExec?

Cheers,
Mathias


On 6/1/19 8:21 PM, Clark Barrett wrote:
> That's right, because those three operators are not associative.
> 
> -Clark
> 
> 
> On Sat, Jun 1, 2019 at 7:54 PM Aina Niemetz <aina.niemetz at gmail.com> wrote:
> 
>> That's my understanding, yes.
>> I actually don't know why this is the case, though.
>>
>> On 6/1/19 7:46 PM, Trevor Hansen wrote:
>>> Thanks Aina,
>>>
>>> I didn't notice that.
>>>
>>> Am I correct in understanding that bvnand, bvnor and bvcomp each must
>>> have two operands?
>>>
>>> Trev.
>>>
>>>
>>> On Sun, Jun 2, 2019 at 11:47 AM Aina Niemetz <aina.niemetz at gmail.com
>>> <mailto:aina.niemetz at gmail.com>> wrote:
>>>
>>>     Hi Trevor,
>>>
>>>     since 2017 (SMT-LIB 2.6), bvadd is left-associative, as is bvor,
>> bvand,
>>>     bvmul, bvxor and bvxnor:
>>>
>>>     http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml
>>>     http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
>>>
>>>     So, yes, this is allowed.
>>>
>>>     Cheers,
>>>     Aina
>>>
>>>
>>>     On 6/1/19 6:40 PM, Trevor Hansen wrote:
>>>     > In the incremental QF_BV benchmarks, The
>>>     >
>>>
>>  /20170501-Heizmann-UltimateAutomizer/jain_5_true-unreach-call_true-no-overflow.i.smt2
>>>     > benchmark has additions with >2 operands.
>>>     >
>>>     > For example:
>>>     >
>>>     > (set-info :smt-lib-version 2.6)
>>>     > (set-logic QF_BV)
>>>     > (declare-fun c_main_~x~4 () (_ BitVec 32))
>>>     > (declare-fun c_main_~y~4 () (_ BitVec 32))
>>>     > (assert
>>>     > (distinct
>>>     > (bvadd
>>>     >   c_main_~y~4
>>>     >   c_main_~x~4
>>>     >   (_ bv4294967266 32)
>>>     > )
>>>     > (_ bv0 32)
>>>     > )
>>>     > )
>>>     > (check-sat)
>>>     >
>>>     > This example is parsed and solved by z3, mathsat, boolector,
>>>     yices2, and
>>>     > cvc4. So addition with >2 operands has wide support.
>>>     >
>>>     > The solvers I'm involved with don't parse it. Although it's easy
>>>     for me to
>>>     > change that.
>>>     >
>>>     > Am I confused, are >2 operands allowed?
>>>     > Even if they are currently not allowed, is the use so widespread
>> they
>>>     > should be allowed?
>>>     >
>>>     > Thanks,
>>>     > Trev.
>>>     > _______________________________________________
>>>     > SMT-COMP mailing list
>>>     > SMT-COMP at cs.nyu.edu <mailto:SMT-COMP at cs.nyu.edu>
>>>     > https://cs.nyu.edu/mailman/listinfo/smt-comp
>>>     >
>>>
>>
>> _______________________________________________
>> SMT-COMP mailing list
>> SMT-COMP at cs.nyu.edu
>> https://cs.nyu.edu/mailman/listinfo/smt-comp
>>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/smt-comp
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-comp/attachments/20190602/efccfc26/attachment.asc>