diseqprop.01.smt « aufbv « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

index : cvc5.git

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

git repository hosting

summary refs log tree commit diff

path: root/test/regress/regress0/aufbv/diseqprop.01.smt

blob: 543684e21786bcae79e708745c4450d75aa9c3bd (plain)

(benchmark B_
  :status unsat
  :logic QF_AUFBV
  :extrafuns ((v6 BitVec[32]))
  :extrafuns ((v7 BitVec[32]))
  :extrafuns ((a1 Array[32:8]))
  :formula
 (and
(not (= (store a1 v6 bv0[8]) (store a1 v6 (extract[7:0] v7))))
(or (= v7 bv0[32]))
)
)

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback