Fix model construction for BV with cbqi. Minor change to defaults.

3 files changed, 88 insertions, 2 deletions

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 9c31204e8..eb28efdf6 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -89,8 +89,9 @@ TESTS =	\
 	bug749-rounding.smt2 \
 	RNDPRE_4_1-dd-nqe.smt2 \
 	mix-complete-strat.smt2 \
-	cbqi-sdlx-fixpoint-3-dd.smt2
-
+	cbqi-sdlx-fixpoint-3-dd.smt2 \
+	qbv-simp.smt2 \
+	psyco-001-bv.smt2
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2
diff --git a/test/regress/regress0/quantifiers/psyco-001-bv.smt2 b/test/regress/regress0/quantifiers/psyco-001-bv.smt2
new file mode 100644
index 000000000..e3428de17
--- /dev/null
+++ b/test/regress/regress0/quantifiers/psyco-001-bv.smt2
@@ -0,0 +1,76 @@
+(set-logic BV)
+(set-info :status sat)
+(declare-fun W_S1_V1 () Bool)
+(declare-fun W_S1_V2 () Bool)
+(declare-fun W_S1_V4 () Bool)
+(declare-fun R_S1_V1 () Bool)
+(declare-fun R_E1_V1 () Bool)
+(declare-fun R_E1_V3 () Bool)
+(declare-fun R_E1_V2 () Bool)
+(declare-fun R_E1_V4 () Bool)
+(declare-fun DISJ_W_S1_R_E1 () Bool)
+(declare-fun R_S1_V3 () Bool)
+(declare-fun R_S1_V2 () Bool)
+(declare-fun R_S1_V4 () Bool)
+(declare-fun DISJ_W_S1_R_S1 () Bool)
+(declare-fun W_S1_V3 () Bool)
+(assert
+ (let
+ (($x324
+   (forall
+    ((V4_0 (_ BitVec 32)) (V2_0 (_ BitVec 32)) 
+     (V3_0 (_ BitVec 32)) (V1_0 (_ BitVec 32)) 
+     (MW_S1_V4 Bool) (MW_S1_V2 Bool) 
+     (MW_S1_V3 Bool) (MW_S1_V1 Bool) 
+     (S1_V3_!14 (_ BitVec 32)) (S1_V3_!20 (_ BitVec 32)) 
+     (E1_!11 (_ BitVec 32)) (E1_!16 (_ BitVec 32)) 
+     (E1_!17 (_ BitVec 32)) (S1_V1_!15 (_ BitVec 32)) 
+     (S1_V1_!21 (_ BitVec 32)) (S1_V2_!13 (_ BitVec 32)) 
+     (S1_V2_!19 (_ BitVec 32)) (S1_V4_!12 (_ BitVec 32)) 
+     (S1_V4_!18 (_ BitVec 32)))
+    (let
+    (($x267
+      (and (= (ite MW_S1_V4 S1_V4_!12 V4_0) (ite MW_S1_V4 S1_V4_!18 V4_0))
+      (= E1_!16 (ite MW_S1_V1 S1_V1_!21 E1_!17))
+      (= (ite MW_S1_V3 S1_V3_!14 V3_0) (ite MW_S1_V3 S1_V3_!20 V3_0))
+      (= (ite MW_S1_V1 S1_V1_!15 E1_!11) (ite MW_S1_V1 S1_V1_!21 E1_!17)))))
+    (let
+    (($x297
+      (and (or (not R_E1_V4) (= (ite MW_S1_V4 S1_V4_!12 V4_0) V4_0))
+      (or (not R_E1_V2) (= (ite MW_S1_V2 S1_V2_!13 V2_0) V2_0))
+      (or (not R_E1_V3) (= (ite MW_S1_V3 S1_V3_!14 V3_0) V3_0))
+      (or (not R_E1_V1) (= (ite MW_S1_V1 S1_V1_!15 E1_!11) V1_0)))))
+    (let
+    (($x310
+      (and (or (not R_E1_V4) (= V4_0 (ite MW_S1_V4 S1_V4_!12 V4_0)))
+      (or (not R_E1_V2) (= V2_0 (ite MW_S1_V2 S1_V2_!13 V2_0)))
+      (or (not R_E1_V3) (= V3_0 (ite MW_S1_V3 S1_V3_!14 V3_0)))
+      (or (not R_E1_V1) (= V1_0 (ite MW_S1_V1 S1_V1_!15 E1_!11))))))
+    (let
+    (($x321
+      (and
+      (or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V3_!20 S1_V3_!14))
+      (or (not $x310) (= E1_!11 E1_!16)) 
+      (= E1_!11 E1_!17) (or (not $x297) (= E1_!16 E1_!17))
+      (or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V1_!21 S1_V1_!15))
+      (or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V2_!19 S1_V2_!13))
+      (or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V4_!18 S1_V4_!12))
+      (or (not MW_S1_V4) W_S1_V4) 
+      (or (not MW_S1_V2) W_S1_V2) 
+      (or (not MW_S1_V1) W_S1_V1)))) 
+    (or (not $x321) $x267))))))))
+ (let
+ (($x40
+   (or (and W_S1_V4 R_E1_V4) 
+   (and W_S1_V2 R_E1_V2) R_E1_V3 
+   (and W_S1_V1 R_E1_V1))))
+ (let (($x42 (= DISJ_W_S1_R_E1 (not $x40))))
+ (let
+ (($x37
+   (or (and W_S1_V4 R_S1_V4) 
+   (and W_S1_V2 R_S1_V2) R_S1_V3 
+   (and W_S1_V1 R_S1_V1))))
+ (let (($x39 (= DISJ_W_S1_R_S1 (not $x37)))) (and W_S1_V3 $x39 $x42 $x324)))))))
+(check-sat)
+(exit)
+
diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2
new file mode 100644
index 000000000..1f72d44e4
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-simp.smt2
@@ -0,0 +1,9 @@
+(set-logic BV)
+(set-info :status unsat)
+(assert
+   (forall
+    ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)))
+      (or (and (= A B) (= C D)) (and (= A C) (= B D)))))
+      
+(check-sat)
+