1 files changed, 162 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/psyco-107-bv.smt2 b/test/regress/regress0/quantifiers/psyco-107-bv.smt2
new file mode 100644
index 000000000..82b54a231
--- /dev/null
+++ b/test/regress/regress0/quantifiers/psyco-107-bv.smt2
@@ -0,0 +1,162 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=eq-boundary
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun W_S1_V6 () Bool)
+(declare-fun W_S1_V4 () Bool)
+(declare-fun W_S1_V2 () Bool)
+(declare-fun W_S1_V3 () Bool)
+(declare-fun W_S1_V1 () Bool)
+(declare-fun R_E2_V1 () Bool)
+(declare-fun R_E2_V3 () Bool)
+(declare-fun R_E1_V3 () Bool)
+(declare-fun R_E1_V1 () Bool)
+(declare-fun R_E1_V6 () Bool)
+(declare-fun R_E1_V4 () Bool)
+(declare-fun R_E1_V5 () Bool)
+(declare-fun R_E1_V2 () Bool)
+(declare-fun DISJ_W_S1_R_E1 () Bool)
+(declare-fun R_S1_V6 () Bool)
+(declare-fun R_S1_V4 () Bool)
+(declare-fun R_S1_V5 () Bool)
+(declare-fun R_S1_V2 () Bool)
+(declare-fun R_S1_V3 () Bool)
+(declare-fun R_S1_V1 () Bool)
+(declare-fun DISJ_W_S1_R_S1 () Bool)
+(declare-fun R_E2_V6 () Bool)
+(declare-fun R_E2_V4 () Bool)
+(declare-fun R_E2_V5 () Bool)
+(declare-fun R_E2_V2 () Bool)
+(declare-fun DISJ_W_S1_R_E2 () Bool)
+(declare-fun W_S1_V5 () Bool)
+(assert
+ (let
+ (($x59848
+   (forall
+    ((V1_0 (_ BitVec 32)) (V3_0 (_ BitVec 32)) 
+     (V2_0 (_ BitVec 32)) (V5_0 (_ BitVec 32)) 
+     (V4_0 (_ BitVec 32)) (V6_0 (_ BitVec 32)) 
+     (MW_S1_V1 Bool) (MW_S1_V3 Bool) 
+     (MW_S1_V2 Bool) (MW_S1_V5 Bool) 
+     (MW_S1_V4 Bool) (MW_S1_V6 Bool) 
+     (S1_V1_!5000 (_ BitVec 32)) (S1_V3_!5001 (_ BitVec 32)) 
+     (S1_V2_!5002 (_ BitVec 32)) (E1_!4994 (_ BitVec 32)) 
+     (E1_!4997 (_ BitVec 32)) (E1_!4999 (_ BitVec 32)) 
+     (S1_V5_!5003 (_ BitVec 32)) (E2_!4995 (_ BitVec 32)) 
+     (E2_!4996 (_ BitVec 32)) (E2_!4998 (_ BitVec 32)) 
+     (S1_V4_!5004 (_ BitVec 32)) (S1_V6_!5005 (_ BitVec 32)))
+    (let ((?x62719 (ite MW_S1_V6 S1_V6_!5005 V6_0)))
+    (let (($x60064 (= V6_0 ?x62719)))
+    (let ((?x61425 (ite MW_S1_V4 S1_V4_!5004 V4_0)))
+    (let (($x59873 (= V4_0 ?x61425)))
+    (let ((?x59861 (ite MW_S1_V5 S1_V5_!5003 V5_0)))
+    (let (($x62312 (= V5_0 ?x59861)))
+    (let ((?x60966 (ite MW_S1_V2 S1_V2_!5002 V2_0)))
+    (let (($x61331 (= V2_0 ?x60966)))
+    (let ((?x62280 (ite MW_S1_V3 S1_V3_!5001 E2_!4998)))
+    (let ((?x60903 (bvadd (_ bv1 32) ?x62280)))
+    (let (($x61268 (= E2_!4996 ?x60903)))
+    (let ((?x60065 (ite MW_S1_V1 S1_V1_!5000 E1_!4999)))
+    (let (($x60169 (= E1_!4994 ?x60065)))
+    (let (($x62661 (and $x60169 $x61268 $x61331 $x62312 $x59873 $x60064)))
+    (let ((?x62301 (bvadd (bvneg (_ bv1 32)) ?x61425)))
+    (let (($x61124 (bvsge ?x62280 ?x62301)))
+    (let ((?x61096 (bvadd (bvneg (_ bv1 32)) ?x60966)))
+    (let (($x60960 (bvsge ?x60065 ?x61096)))
+    (let (($x62453 (bvsle V2_0 E1_!4999)))
+    (let (($x61140 (not $x62453)))
+    (let (($x60239 (bvsle V4_0 E2_!4998)))
+    (let (($x61367 (not $x60239)))
+    (let (($x59857 (bvsle V2_0 E1_!4997)))
+    (let (($x62570 (not $x59857)))
+    (let ((?x62418 (bvadd (bvneg (_ bv1 32)) V2_0)))
+    (let (($x60189 (bvsge E1_!4994 ?x62418)))
+    (let (($x62421 (bvsge E2_!4996 V4_0)))
+    (let (($x60898 (bvsle V2_0 E1_!4994)))
+    (let (($x59938 (not $x60898)))
+    (let (($x62400 (bvsle V4_0 E2_!4995)))
+    (let (($x60971 (not $x62400)))
+    (let
+    (($x62394
+      (and $x60971 $x59938 $x62421 $x60189 $x62570 $x61367 $x61140 $x60960
+      $x61124)))
+    (let (($x62485 (not $x62394)))
+    (let (($x60905 (not MW_S1_V6)))
+    (let (($x61285 (or $x60905 W_S1_V6)))
+    (let (($x61317 (not MW_S1_V4)))
+    (let (($x60137 (or $x61317 W_S1_V4)))
+    (let (($x62306 (not MW_S1_V2)))
+    (let (($x62708 (or $x62306 W_S1_V2)))
+    (let (($x62310 (not MW_S1_V3)))
+    (let (($x60291 (or $x62310 W_S1_V3)))
+    (let (($x62641 (not MW_S1_V1)))
+    (let (($x61174 (or $x62641 W_S1_V1)))
+    (let (($x62627 (= E2_!4998 E2_!4995)))
+    (let (($x60904 (= E1_!4997 E1_!4994)))
+    (let (($x128 (not R_E2_V1)))
+    (let (($x60161 (or $x128 $x60904)))
+    (let (($x62415 (not $x60161)))
+    (let (($x62645 (or $x62415 $x62627)))
+    (let (($x60924 (= E2_!4996 E2_!4998)))
+    (let (($x62711 (= E2_!4995 V3_0)))
+    (let (($x130 (not R_E2_V3)))
+    (let (($x62623 (or $x130 $x62711)))
+    (let (($x60954 (= E1_!4994 E1_!4997)))
+    (let (($x59868 (or $x128 $x60954)))
+    (let (($x62319 (and $x59868 $x62623)))
+    (let (($x62554 (not $x62319)))
+    (let (($x60985 (or $x62554 $x60924)))
+    (let (($x62256 (= E2_!4996 E2_!4995)))
+    (let (($x62540 (not $x62623)))
+    (let (($x60968 (or $x62540 $x62256)))
+    (let (($x62486 (= E1_!4999 E1_!4997)))
+    (let (($x60109 (= E2_!4998 V3_0)))
+    (let (($x115 (not R_E1_V3)))
+    (let (($x60129 (or $x115 $x60109)))
+    (let (($x60976 (= E1_!4997 V1_0)))
+    (let (($x113 (not R_E1_V1)))
+    (let (($x62568 (or $x113 $x60976)))
+    (let (($x60942 (and $x62568 $x60129)))
+    (let (($x60209 (not $x60942)))
+    (let (($x62263 (or $x60209 $x62486)))
+    (let (($x60965 (= E1_!4999 E1_!4994)))
+    (let (($x62348 (or $x60209 $x60965)))
+    (let
+    (($x60285
+      (and $x60954 $x62348 $x62263 $x60968 $x60985 $x62645 $x61174 $x60291
+      $x62708 $x60137 $x61285)))
+    (let (($x62430 (not $x60285))) (or $x62430 $x62485 $x62661)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ (let (($x56 (and W_S1_V6 R_E1_V6)))
+ (let (($x54 (and W_S1_V4 R_E1_V4)))
+ (let (($x50 (and W_S1_V2 R_E1_V2)))
+ (let (($x48 (and W_S1_V3 R_E1_V3)))
+ (let (($x46 (and W_S1_V1 R_E1_V1)))
+ (let (($x69 (or $x46 $x48 $x50 R_E1_V5 $x54 $x56)))
+ (let (($x70 (not $x69)))
+ (let (($x71 (= DISJ_W_S1_R_E1 $x70)))
+ (let (($x40 (and W_S1_V6 R_S1_V6)))
+ (let (($x38 (and W_S1_V4 R_S1_V4)))
+ (let (($x34 (and W_S1_V2 R_S1_V2)))
+ (let (($x32 (and W_S1_V3 R_S1_V3)))
+ (let (($x30 (and W_S1_V1 R_S1_V1)))
+ (let (($x66 (or $x30 $x32 $x34 R_S1_V5 $x38 $x40)))
+ (let (($x67 (not $x66)))
+ (let (($x68 (= DISJ_W_S1_R_S1 $x67)))
+ (let (($x24 (and W_S1_V6 R_E2_V6)))
+ (let (($x21 (and W_S1_V4 R_E2_V4)))
+ (let (($x16 (and W_S1_V2 R_E2_V2)))
+ (let (($x13 (and W_S1_V3 R_E2_V3)))
+ (let (($x10 (and W_S1_V1 R_E2_V1)))
+ (let (($x63 (or $x10 $x13 $x16 R_E2_V5 $x21 $x24)))
+ (let (($x64 (not $x63)))
+ (let (($x65 (= DISJ_W_S1_R_E2 $x64)))
+ (let (($x130 (not R_E2_V3)))
+ (let (($x115 (not R_E1_V3)))
+ (let (($x113 (not R_E1_V1)))
+ (let (($x60916 (and $x113 $x115)))
+ (let (($x62291 (or $x60916 $x130)))
+ (and $x62291 W_S1_V5 $x65 $x68 $x71 $x59848))))))))))))))))))))))))))))))))
+(assert R_E2_V3)
+(check-sat)
+(exit)
+