Apply preprocessing to counterexample lemmas in CEGQI (#2027)

4 files changed, 373 insertions, 2 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 72633e86f..9dd0bdb04 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1475,6 +1475,9 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
     Node rlem = lems[i];
     rlem = Rewriter::rewrite( rlem );
+    // also must preprocess to ensure that the counterexample atoms we
+    // collect below are identical to the atoms that we add to the CNF stream
+    rlem = d_qe->getTheoryEngine()->preprocess(rlem);
     Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
     //record the literals that imply auxiliary variables to be equal to terms
     if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
@@ -1498,7 +1501,6 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     }*/
     lems[i] = rlem;
   }
-
   // determine variable order: must do Reals before Ints
   Trace("cbqi-debug") << "Determine variable order..." << std::endl;
   if (!d_vars.empty())
@@ -1546,7 +1548,8 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     }
   }
 
-  //collect atoms from all lemmas: we will only do bounds coming from original body
+  // collect atoms from all lemmas: we will only solve for literals coming from
+  // the original body
   d_is_nested_quant = false;
   std::map< Node, bool > visited;
   for( unsigned i=0; i<lems.size(); i++ ){
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 72bb8e1d1..b40b28dae 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1230,6 +1230,7 @@ REG1_TESTS = \
 	regress1/push-pop/quant-fun-proc-unmacro.smt2 \
 	regress1/push-pop/quant-fun-proc.smt2 \
 	regress1/quantifiers/006-cbqi-ite.smt2 \
+	regress1/quantifiers/015-psyco-pp.smt2 \
 	regress1/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2 \
 	regress1/quantifiers/Arrays_Q1-noinfer.smt2 \
 	regress1/quantifiers/NUM878.smt2 \
@@ -1295,6 +1296,7 @@ REG1_TESTS = \
 	regress1/quantifiers/ricart-agrawala6.smt2 \
 	regress1/quantifiers/set8.smt2 \
 	regress1/quantifiers/small-pipeline-fixpoint-3.smt2 \
+	regress1/quantifiers/smtcomp-qbv-053118.smt2 \
 	regress1/quantifiers/smtlib384a03.smt2 \
 	regress1/quantifiers/smtlib46f14a.smt2 \
 	regress1/quantifiers/smtlibe99bbe.smt2 \
diff --git a/test/regress/regress1/quantifiers/015-psyco-pp.smt2 b/test/regress/regress1/quantifiers/015-psyco-pp.smt2
new file mode 100644
index 000000000..c7afa8662
--- /dev/null
+++ b/test/regress/regress1/quantifiers/015-psyco-pp.smt2
@@ -0,0 +1,344 @@
+(set-info :smt-lib-version 2.6)
+(set-logic LIA)
+(set-info :status sat)
+(declare-fun R_S1_V5 () Bool)
+(declare-fun W_S2_V5 () Bool)
+(declare-fun W_S2_V3 () Bool)
+(declare-fun W_S1_V5 () Bool)
+(declare-fun R_S2_V1 () Bool)
+(declare-fun W_S1_V1 () Bool)
+(declare-fun R_S2_V3 () Bool)
+(declare-fun R_S2_V2 () Bool)
+(declare-fun W_S1_V2 () Bool)
+(declare-fun R_S2_V5 () Bool)
+(declare-fun R_S1_V1 () Bool)
+(declare-fun R_S1_V3 () Bool)
+(declare-fun R_S1_V2 () Bool)
+(declare-fun R_S2_V4 () Bool)
+(declare-fun DISJ_W_S2_R_S2 () Bool)
+(declare-fun R_S1_V4 () Bool)
+(declare-fun W_S1_V4 () Bool)
+(declare-fun DISJ_W_S1_R_S1 () Bool)
+(declare-fun W_S2_V4 () Bool)
+(declare-fun W_S1_V3 () Bool)
+(declare-fun W_S2_V1 () Bool)
+(declare-fun W_S2_V2 () Bool)
+(declare-fun DISJ_W_S2_R_S1 () Bool)
+(declare-fun DISJ_W_S1_W_S2 () Bool)
+(declare-fun DISJ_W_S1_R_S2 () Bool)
+(assert
+ (let (($x796 (not W_S2_V3)))
+ (let (($x177 (not R_S2_V3)))
+ (let
+ (($x1274
+   (forall
+    ((V4_0 Int) (V5_0 Int) 
+     (V2_0 Int) (V3_0 Int) 
+     (V1_0 Int) (MW_S1_V4 Bool) 
+     (MW_S1_V5 Bool) (MW_S1_V2 Bool) 
+     (MW_S1_V3 Bool) (MW_S1_V1 Bool) 
+     (MW_S2_V4 Bool) (MW_S2_V5 Bool) 
+     (MW_S2_V2 Bool) (MW_S2_V3 Bool) 
+     (MW_S2_V1 Bool) (S1_V4_!5047 Int) 
+     (S1_V4_!5057 Int) (S1_V4_!5072 Int) 
+     (S1_V4_!5077 Int) (S2_V4_!5052 Int) 
+     (S2_V4_!5062 Int) (S2_V4_!5067 Int) 
+     (S2_V5_!5053 Int) (S2_V5_!5063 Int) 
+     (S2_V5_!5068 Int) (S1_V1_!5051 Int) 
+     (S1_V1_!5061 Int) (S1_V1_!5076 Int) 
+     (S1_V1_!5081 Int) (S1_V3_!5050 Int) 
+     (S1_V3_!5060 Int) (S1_V3_!5075 Int) 
+     (S1_V3_!5080 Int) (S1_V2_!5049 Int) 
+     (S1_V2_!5059 Int) (S1_V2_!5074 Int) 
+     (S1_V2_!5079 Int) (S2_V1_!5056 Int) 
+     (S2_V1_!5066 Int) (S2_V1_!5071 Int) 
+     (S2_V2_!5054 Int) (S2_V2_!5064 Int) 
+     (S2_V2_!5069 Int) (S2_V3_!5055 Int) 
+     (S2_V3_!5065 Int) (S2_V3_!5070 Int) 
+     (S1_V5_!5048 Int) (S1_V5_!5058 Int) 
+     (S1_V5_!5073 Int) (S1_V5_!5078 Int))
+    (let ((?x19858 (ite MW_S1_V1 S1_V1_!5051 V1_0)))
+    (let ((?x19735 (ite MW_S2_V1 S2_V1_!5056 ?x19858)))
+    (let ((?x2666 (+ 1 ?x19735)))
+    (let ((?x19816 (ite MW_S1_V1 S1_V1_!5061 ?x2666)))
+    (let
+    (($x19044
+      (= (ite MW_S2_V1 S2_V1_!5066 ?x19816)
+      (ite MW_S1_V1 S1_V1_!5081
+      (+ 1 (ite MW_S1_V1 S1_V1_!5076 (ite MW_S2_V1 S2_V1_!5071 V1_0)))))))
+    (let
+    (($x20397
+      (=
+      (ite MW_S2_V3 S2_V3_!5065
+      (ite MW_S1_V3 S1_V3_!5060
+      (ite MW_S2_V3 S2_V3_!5055 (ite MW_S1_V3 S1_V3_!5050 V3_0))))
+      (ite MW_S1_V3 S1_V3_!5080 (ite MW_S2_V3 S2_V3_!5070 V3_0)))))
+    (let
+    (($x19931
+      (=
+      (ite MW_S2_V2 S2_V2_!5064
+      (ite MW_S1_V2 S1_V2_!5059
+      (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0))))
+      (ite MW_S1_V2 S1_V2_!5079 (ite MW_S2_V2 S2_V2_!5069 V2_0)))))
+    (let
+    (($x19917
+      (=
+      (ite MW_S2_V5 S2_V5_!5063
+      (ite MW_S1_V5 S1_V5_!5058
+      (ite MW_S2_V5 S2_V5_!5053 (ite MW_S1_V5 S1_V5_!5048 V5_0))))
+      (ite MW_S1_V5 S1_V5_!5078 (ite MW_S2_V5 S2_V5_!5068 V5_0)))))
+    (let
+    (($x19951
+      (=
+      (ite MW_S2_V4 S2_V4_!5062
+      (ite MW_S1_V4 S1_V4_!5057
+      (ite MW_S2_V4 S2_V4_!5052 (ite MW_S1_V4 S1_V4_!5047 V4_0))))
+      (ite MW_S1_V4 S1_V4_!5077 (ite MW_S2_V4 S2_V4_!5067 V4_0)))))
+    (let
+    (($x19175
+      (>=
+      (ite MW_S1_V1 S1_V1_!5081
+      (+ 1 (ite MW_S1_V1 S1_V1_!5076 (ite MW_S2_V1 S2_V1_!5071 V1_0))))
+      (+ (- 1) (ite MW_S1_V2 S1_V2_!5079 (ite MW_S2_V2 S2_V2_!5069 V2_0))))))
+    (let ((?x19970 (ite MW_S2_V1 S2_V1_!5071 V1_0)))
+    (let ((?x19876 (ite MW_S1_V1 S1_V1_!5076 ?x19970)))
+    (let ((?x20041 (+ 1 ?x19876)))
+    (let ((?x20154 (ite MW_S2_V2 S2_V2_!5069 V2_0)))
+    (let ((?x20275 (ite MW_S1_V2 S1_V2_!5074 ?x20154)))
+    (let
+    ((?x20280
+      (+ (- 1)
+      (ite MW_S2_V2 S2_V2_!5064
+      (ite MW_S1_V2 S1_V2_!5059
+      (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0)))))))
+    (let
+    (($x20340
+      (and (not (<= V2_0 V1_0))
+      (not
+      (<= (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0)) ?x2666))
+      (>= (ite MW_S2_V1 S2_V1_!5066 ?x19816) ?x20280)
+      (not (<= ?x20154 ?x19970)) 
+      (not (<= ?x20275 ?x20041)) $x19175)))
+    (let (($x164 (not R_S1_V3)))
+    (let
+    (($x16591
+      (or $x164
+      (= (ite MW_S1_V3 S1_V3_!5075 (ite MW_S2_V3 S2_V3_!5070 V3_0))
+      (ite MW_S2_V3 S2_V3_!5070 V3_0)))))
+    (let (($x160 (not R_S1_V5)))
+    (let
+    (($x4147
+      (or $x160
+      (= (ite MW_S1_V5 S1_V5_!5073 (ite MW_S2_V5 S2_V5_!5068 V5_0))
+      (ite MW_S2_V5 S2_V5_!5068 V5_0)))))
+    (let
+    (($x20079
+      (and $x4147 (or (not R_S1_V2) (= ?x20275 ?x20154)) $x16591
+      (or (not R_S1_V1) (= ?x19876 (+ (- 1) ?x19970))))))
+    (let (($x1365 (not $x20079)))
+    (let ((?x19329 (ite MW_S2_V3 S2_V3_!5070 V3_0)))
+    (let ((?x20227 (ite MW_S1_V3 S1_V3_!5075 ?x19329)))
+    (let
+    ((?x19017 (ite MW_S2_V3 S2_V3_!5055 (ite MW_S1_V3 S1_V3_!5050 V3_0))))
+    (let ((?x19159 (ite MW_S2_V5 S2_V5_!5068 V5_0)))
+    (let ((?x19823 (ite MW_S1_V5 S1_V5_!5073 ?x19159)))
+    (let ((?x19445 (ite MW_S1_V5 S1_V5_!5048 V5_0)))
+    (let ((?x19140 (ite MW_S2_V5 S2_V5_!5053 ?x19445)))
+    (let
+    (($x20082
+      (and (or $x160 (= ?x19140 ?x19823))
+      (or (not R_S1_V2)
+      (= (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0)) ?x20275))
+      (or $x164 (= ?x19017 ?x20227)) 
+      (or (not R_S1_V1) (= ?x19735 ?x19876)))))
+    (let (($x20074 (not $x20082)))
+    (let
+    (($x20083
+      (and (or $x160 (= ?x19140 ?x19159))
+      (or (not R_S1_V2)
+      (= (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0)) ?x20154))
+      (or $x164 (= ?x19017 ?x19329))
+      (or (not R_S1_V1) (= ?x19735 (+ (- 1) ?x19970))))))
+    (let (($x20084 (not $x20083)))
+    (let
+    (($x8373
+      (and (or $x160 (= ?x19140 V5_0))
+      (or (not R_S1_V2)
+      (= (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0)) V2_0))
+      (or $x164 (= ?x19017 V3_0))
+      (or (not R_S1_V1) (= ?x19735 (+ (- 1) V1_0))))))
+    (let (($x19787 (not $x8373)))
+    (let
+    (($x19719
+      (and (or $x160 (= V5_0 ?x19823)) 
+      (or (not R_S1_V2) (= V2_0 ?x20275)) 
+      (or $x164 (= V3_0 ?x20227)) 
+      (or (not R_S1_V1) (= V1_0 ?x20041)))))
+    (let (($x19712 (not $x19719)))
+    (let
+    (($x1403
+      (and (or $x160 (= V5_0 ?x19159)) 
+      (or (not R_S1_V2) (= V2_0 ?x20154)) 
+      (or $x164 (= V3_0 ?x19329)) 
+      (or (not R_S1_V1) (= V1_0 ?x19970)))))
+    (let (($x1473 (not $x1403)))
+    (let
+    (($x20361
+      (and (or (not R_S2_V4) (= V4_0 (ite MW_S1_V4 S1_V4_!5047 V4_0)))
+      (or (not R_S2_V5) (= V5_0 ?x19445))
+      (or (not R_S2_V2) (= V2_0 (ite MW_S1_V2 S1_V2_!5049 V2_0)))
+      (or (not R_S2_V1) (= V1_0 ?x19858)))))
+    (let (($x19974 (not $x20361)))
+    (let (($x175 (not R_S2_V2)))
+    (let
+    (($x19080
+      (or $x175
+      (=
+      (ite MW_S1_V2 S1_V2_!5059
+      (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0))) V2_0))))
+    (let (($x171 (not R_S2_V4)))
+    (let
+    (($x1175
+      (or $x171
+      (=
+      (ite MW_S1_V4 S1_V4_!5057
+      (ite MW_S2_V4 S2_V4_!5052 (ite MW_S1_V4 S1_V4_!5047 V4_0))) V4_0))))
+    (let
+    (($x19801
+      (and $x1175
+      (or (not R_S2_V5) (= (ite MW_S1_V5 S1_V5_!5058 ?x19140) V5_0)) $x19080
+      (or (not R_S2_V1) (= ?x19816 V1_0)))))
+    (let (($x19804 (not $x19801)))
+    (let ((?x10718 (ite MW_S1_V2 S1_V2_!5049 V2_0)))
+    (let ((?x18681 (ite MW_S2_V2 S2_V2_!5054 ?x10718)))
+    (let ((?x19161 (ite MW_S1_V2 S1_V2_!5059 ?x18681)))
+    (let ((?x19599 (ite MW_S1_V4 S1_V4_!5047 V4_0)))
+    (let
+    ((?x18788 (ite MW_S1_V4 S1_V4_!5057 (ite MW_S2_V4 S2_V4_!5052 ?x19599))))
+    (let
+    (($x3852
+      (and (or $x171 (= ?x18788 ?x19599))
+      (or (not R_S2_V5) (= (ite MW_S1_V5 S1_V5_!5058 ?x19140) ?x19445))
+      (or $x175 (= ?x19161 ?x10718)) 
+      (or (not R_S2_V1) (= ?x19816 ?x19858)))))
+    (let (($x19708 (not $x3852)))
+    (let
+    (($x20195
+      (and (or $x171 (= V4_0 ?x18788))
+      (or (not R_S2_V5) (= V5_0 (ite MW_S1_V5 S1_V5_!5058 ?x19140)))
+      (or $x175 (= V2_0 ?x19161)) 
+      (or (not R_S2_V1) (= V1_0 ?x19816)))))
+    (let
+    (($x1440
+      (and (or $x160 (= ?x19823 ?x19140))
+      (or (not R_S1_V2) (= ?x20275 ?x18681)) 
+      (or $x164 (= ?x20227 ?x19017)) 
+      (or (not R_S1_V1) (= ?x19876 ?x19735)))))
+    (let
+    (($x1199
+      (and (or $x160 (= ?x19823 V5_0)) 
+      (or (not R_S1_V2) (= ?x20275 V2_0)) 
+      (or $x164 (= ?x20227 V3_0))
+      (or (not R_S1_V1) (= ?x19876 (+ (- 1) V1_0))))))
+    (let
+    (($x1442
+      (and (or $x160 (= ?x19159 ?x19140))
+      (or (not R_S1_V2) (= ?x20154 ?x18681)) 
+      (or $x164 (= ?x19329 ?x19017)) 
+      (or (not R_S1_V1) (= ?x19970 ?x2666)))))
+    (let
+    (($x1484
+      (and (or $x160 (= V5_0 ?x19140)) 
+      (or (not R_S1_V2) (= V2_0 ?x18681)) 
+      (or $x164 (= V3_0 ?x19017)) 
+      (or (not R_S1_V1) (= V1_0 ?x2666)))))
+    (let
+    (($x19714
+      (and (or $x171 (= ?x19599 ?x18788))
+      (or (not R_S2_V5) (= ?x19445 (ite MW_S1_V5 S1_V5_!5058 ?x19140)))
+      (or $x175 (= ?x10718 ?x19161)) 
+      (or (not R_S2_V1) (= ?x19858 ?x19816)))))
+    (let
+    (($x20189
+      (and (or $x160 (= ?x19159 ?x19823))
+      (or (not R_S1_V2) (= ?x20154 ?x20275)) 
+      (or $x164 (= ?x19329 ?x20227)) 
+      (or (not R_S1_V1) (= ?x19970 ?x20041)))))
+    (let
+    (($x19788
+      (and (or $x160 (= ?x19159 V5_0)) 
+      (or (not R_S1_V2) (= ?x20154 V2_0)) 
+      (or $x164 (= ?x19329 V3_0)) 
+      (or (not R_S1_V1) (= ?x19970 V1_0)))))
+    (let
+    (($x1223
+      (and (or $x19712 (= S1_V4_!5047 S1_V4_!5077))
+      (or $x19787 (= S1_V4_!5057 S1_V4_!5047))
+      (or $x20084 (= S1_V4_!5057 S1_V4_!5072))
+      (or $x20074 (= S1_V4_!5057 S1_V4_!5077))
+      (or (not $x19788) (= S1_V4_!5072 S1_V4_!5047))
+      (or (not $x20189) (= S1_V4_!5072 S1_V4_!5077))
+      (or $x19708 (= S2_V4_!5062 S2_V4_!5052))
+      (or $x19804 (= S2_V4_!5062 S2_V4_!5067))
+      (or $x19974 (= S2_V4_!5067 S2_V4_!5052))
+      (or (not $x19714) (= S2_V5_!5053 S2_V5_!5063))
+      (or $x19974 (= S2_V5_!5068 S2_V5_!5053))
+      (or (not $x20195) (= S2_V5_!5068 S2_V5_!5063))
+      (or $x1473 (= S1_V1_!5051 S1_V1_!5076))
+      (or $x19712 (= S1_V1_!5051 S1_V1_!5081))
+      (or $x19787 (= S1_V1_!5061 S1_V1_!5051))
+      (or $x20084 (= S1_V1_!5061 S1_V1_!5076))
+      (or $x20074 (= S1_V1_!5061 S1_V1_!5081))
+      (or $x1365 (= S1_V1_!5081 S1_V1_!5076))
+      (or (not $x1484) (= S1_V3_!5050 S1_V3_!5060))
+      (or $x1473 (= S1_V3_!5050 S1_V3_!5075))
+      (or $x19712 (= S1_V3_!5050 S1_V3_!5080))
+      (or $x20084 (= S1_V3_!5060 S1_V3_!5075))
+      (or (not $x1440) (= S1_V3_!5080 S1_V3_!5060))
+      (or $x1365 (= S1_V3_!5080 S1_V3_!5075))
+      (or (not $x1484) (= S1_V2_!5049 S1_V2_!5059))
+      (or $x1473 (= S1_V2_!5049 S1_V2_!5074))
+      (or (not $x1442) (= S1_V2_!5074 S1_V2_!5059))
+      (or (not $x1199) (= S1_V2_!5079 S1_V2_!5049))
+      (or (not $x1440) (= S1_V2_!5079 S1_V2_!5059))
+      (or $x1365 (= S1_V2_!5079 S1_V2_!5074))
+      (or $x19708 (= S2_V1_!5066 S2_V1_!5056))
+      (or $x19974 (= S2_V1_!5071 S2_V1_!5056))
+      (or (not $x20195) (= S2_V1_!5071 S2_V1_!5066))
+      (or $x19708 (= S2_V2_!5064 S2_V2_!5054))
+      (or $x19804 (= S2_V2_!5064 S2_V2_!5069))
+      (or $x19974 (= S2_V2_!5069 S2_V2_!5054))
+      (or $x19708 (= S2_V3_!5065 S2_V3_!5055))
+      (or $x19804 (= S2_V3_!5065 S2_V3_!5070))
+      (or $x19974 (= S2_V3_!5070 S2_V3_!5055))
+      (or $x1473 (= S1_V5_!5048 S1_V5_!5073))
+      (or $x19712 (= S1_V5_!5048 S1_V5_!5078))
+      (or $x19787 (= S1_V5_!5058 S1_V5_!5048))
+      (or $x20084 (= S1_V5_!5058 S1_V5_!5073))
+      (or $x20074 (= S1_V5_!5058 S1_V5_!5078))
+      (or $x1365 (= S1_V5_!5078 S1_V5_!5073)) 
+      (not MW_S1_V4) (or (not MW_S1_V5) W_S1_V5) 
+      (or (not MW_S1_V2) W_S1_V2) 
+      (or (not MW_S1_V1) W_S1_V1) 
+      (or (not MW_S2_V5) W_S2_V5) 
+      (not MW_S2_V2) (not MW_S2_V3) 
+      (not MW_S2_V1))))
+    (or (not $x1223) (not $x20340)
+    (and $x19951 $x19917 $x19931 $x20397 $x19044)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ (let (($x158 (not R_S1_V4)))
+ (let (($x754 (not W_S1_V4)))
+ (let (($x23 (and W_S1_V1 R_S1_V1)))
+ (let (($x18 (and W_S1_V2 R_S1_V2)))
+ (let (($x15 (and W_S1_V5 R_S1_V5)))
+ (let (($x786 (not W_S2_V1)))
+ (let (($x783 (not W_S2_V2)))
+ (and DISJ_W_S1_R_S2 DISJ_W_S1_W_S2 DISJ_W_S2_R_S1 $x783 $x786 W_S1_V3
+ W_S2_V4 (= DISJ_W_S1_R_S1 (not (or $x15 $x18 R_S1_V3 $x23))) $x754 $x158
+ (= DISJ_W_S2_R_S2 (not (or R_S2_V4 (and W_S2_V5 R_S2_V5)))) $x1274
+ (not (and W_S1_V5 R_S2_V5)) 
+ (not (and W_S1_V2 R_S2_V2)) $x177 
+ (not (and W_S1_V1 R_S2_V1)) 
+ (not (and W_S1_V5 W_S2_V5)) $x796 
+ (not (and W_S2_V5 R_S1_V5))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2
new file mode 100644
index 000000000..6cbe4db5c
--- /dev/null
+++ b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2
@@ -0,0 +1,22 @@
+(set-info :smt-lib-version 2.6)
+(set-logic BV)
+(set-info :status sat)
+(declare-fun x () (_ BitVec 32))
+(assert 
+(forall ((u (_ BitVec 32)) (w (_ BitVec 32)) (z (_ BitVec 32)) (m (_ BitVec 32)) (n (_ BitVec 32))) (or 
+  (not (= 
+    (bvadd (bvmul (_ bv2 32) w) (bvmul (_ bv2 32) n)) 
+    (bvadd (bvneg (bvadd (bvmul (_ bv2 32) u) (bvmul (_ bv2 32) z) (bvmul (_ bv2 32) m) x)) (_ bv1 32))
+  )) 
+))
+)
+(assert (not 
+(and 
+  (forall ((m (_ BitVec 32)) (n (_ BitVec 32))) 
+    (not (= 
+      (bvadd (bvneg (bvadd m x)) (_ bv1 32)) 
+      (bvmul (_ bv2 32) n)
+    ))
+))))
+(check-sat)
+(exit)