cleaning up the expample for the future

diff --git a/test/regress/regress0/aufbv/diseqprop.01.smt b/test/regress/regress0/aufbv/diseqprop.01.smt
index 543684e21786bcae79e708745c4450d75aa9c3bd..4b31304759840b1e012bee74927da3d80a09a1ff 100644 (file)
--- a/test/regress/regress0/aufbv/diseqprop.01.smt
+++ b/test/regress/regress0/aufbv/diseqprop.01.smt
@@ -1,12 +1,13 @@
 (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]))
-)
+  
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :extrafuns ((a Array[32:8]))
+  
+  :assumption (not (= (store a x bv0[8]) (store a x (extract[7:0] y))))
+  :assumption (= y bv0[32])
+
+  :formula true
 )