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

[Clark Barrett]

The benchmark has been replaced on StarExec.

-Clark


On Sun, Jun 2, 2019 at 1:01 AM Mathias Preiner <mathias.preiner at gmail.com>
wrote:

> 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
> >
>
>