From fbaa1e2bdb2d10465b76fc6fc3fbfd3318612493 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 7 Jun 2012 15:31:08 +0000
Subject: [PATCH] Added small test case for diseq propagation

---
 test/regress/regress0/aufbv/diseqprop.01.smt | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test/regress/regress0/aufbv/diseqprop.01.smt

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]))
+)
+)
-- 
2.30.2