From: Clark Barrett Date: Thu, 7 Jun 2012 15:31:08 +0000 (+0000) Subject: Added small test case for diseq propagation X-Git-Tag: cvc5-1.0.0~8113 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fbaa1e2bdb2d10465b76fc6fc3fbfd3318612493;p=cvc5.git Added small test case for diseq propagation --- diff --git a/test/regress/regress0/aufbv/diseqprop.01.smt b/test/regress/regress0/aufbv/diseqprop.01.smt new file mode 100644 index 000000000..543684e21 --- /dev/null +++ b/test/regress/regress0/aufbv/diseqprop.01.smt @@ -0,0 +1,12 @@ +(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])) +) +)