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 (file)
index 0000000..543684e
--- /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]))
+)
+)