diff options
Diffstat (limited to 'test/regress/regress0/aufbv')
| -rw-r--r-- | test/regress/regress0/aufbv/diseqprop.01.smt | 12 |
1 files changed, 12 insertions, 0 deletions
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])) +) +) |