CBQI BV quick heuristics (#1239)

Adds two heuristics for cbqi-bv, both disabled by default.

The first optimistically solves for boundary points of inequalities.
The second randomly interleaves inversion and value instantiations.
Adds some newly solved regressions from SMT LIB.

6 files changed, 182 insertions, 71 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 2e765ce6b..d3f8c9f6a 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -334,7 +334,11 @@ option quantEprMatching --quant-epr-match bool :default true
  
 # CEGQI for BV
 option cbqiBv --cbqi-bv bool :read-write :default false
- use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors
+  use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors
+option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false
+  interleave model value instantiation with word-level inversion approach
+option cbqiBvSlackIneq --cbqi-bv-slack-ineq bool :read-write :default true
+  use model slack values when solving inequalities with word-level inversion approach
  
 ### local theory extensions options 
 
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 91c29c6de..ad99f1135 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -897,12 +897,15 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf,
     unsigned iid = d_inst_id_counter;
     Node inst = d_inverter->solve_bv_lit( sv, slit, true, path, &m, d_inst_id_to_status[iid] );
     if( !inst.isNull() ){
+      inst = Rewriter::rewrite(inst);
+      Trace("cegqi-bv") << "...solved form is " << inst << std::endl;
       // store information for id and increment
       d_var_to_inst_id[pv].push_back( iid );
       d_inst_id_to_term[iid] = inst;
       d_inst_id_to_alit[iid] = alit;
       d_inst_id_counter++;
     }else{
+      Trace("cegqi-bv") << "...failed to solve." << std::endl;
       // cleanup information if we failed to solve
       d_inst_id_to_status.erase( iid );
     }
@@ -920,11 +923,23 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
       return lit;
     }
   } else {
+    bool useSlack = false;
+    if (k == EQUAL) {
+      // always use slack for disequalities
+      useSlack = true;
+    } else if (k == BITVECTOR_ULT || k == BITVECTOR_SLT) {
+      if (options::cbqiBvSlackIneq()) {
+        useSlack = true;
+      }
+    } else {
+      // others should be rewritten
+      Assert(false);
+      return Node::null();
+    }
     // for all other predicates, we convert them to a positive equality based on
     // the current model M, e.g.:
     //   (not) s ~ t  --->  s = t + ( s^M - t^M )
-    if (k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_ULE ||
-        k == BITVECTOR_SLT || k == BITVECTOR_SLE) {
+    if (useSlack) {
       Node s = atom[0];
       Node t = atom[1];
       // only handle equalities between bitvectors
@@ -934,19 +949,43 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf,
         Assert(!sm.isNull() && sm.isConst());
         Node tm = ci->getModelValue(t);
         Assert(!tm.isNull() && tm.isConst());
+        Node ret;
         if (sm != tm) {
           Node slack =
               Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, sm, tm));
           Assert(slack.isConst());
           // remember the slack value for the asserted literal
           d_alit_to_model_slack[lit] = slack;
-          Node ret = nm->mkNode(kind::EQUAL, s,
-                                nm->mkNode(kind::BITVECTOR_PLUS, t, slack));
+          ret = nm->mkNode(kind::EQUAL, s,
+                           nm->mkNode(kind::BITVECTOR_PLUS, t, slack));
           Trace("cegqi-bv") << "Process " << lit << " as " << ret
                             << ", slack is " << slack << std::endl;
-          return ret;
+        }else{
+          ret = s.eqNode(t);          
+          Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
         }
+        return ret;
+      }
+    } else {
+      // otherwise, we optimistically solve for the boundary point of an inequality
+      // for example
+      //   for s < t, we solve s+1 = t
+      //   for ~( s < t ), we solve s = t
+      // notice that this equality does not necessarily hold in the model, and
+      // hence the corresponding instantiation strategy is not guaranteed to be
+      // monotonic.
+      Node ret;
+      if (!pol) {
+        ret = atom[0].eqNode(atom[1]);
+      } else {
+        unsigned one = 1;
+        BitVector bval(atom[0].getType().getConst<BitVectorSize>(), one);
+        Node bv_one = NodeManager::currentNM()->mkConst<BitVector>(bval);
+        ret = NodeManager::currentNM()
+                  ->mkNode(kind::BITVECTOR_PLUS, atom[0], bv_one)
+                  .eqNode(atom[1]);
       }
+      return ret;
     }
   }
   return Node::null();
@@ -976,79 +1015,94 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
   std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv );
   if( iti!=d_var_to_inst_id.end() ){
     Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl;
-    // get inst id list
-    Trace("cegqi-bv") << "  " << iti->second.size() << " candidate instantiations for " << pv << " : " << std::endl;
-    // the order of instantiation ids we will try
-    std::vector< unsigned > inst_ids_try;
-    // until we have a model-preserving selection function for BV, this must be heuristic (we only pick one literal)
-    // hence we randomize the list
-    // this helps robustness, since picking the same literal every time may be lead to a stream of value instantiations
-    std::random_shuffle( iti->second.begin(), iti->second.end() );
+    // if interleaving, do not do inversion half the time
+    if (!options::cbqiBvInterleaveValue() || rand() % 2 == 0) {
+      // get inst id list
+      Trace("cegqi-bv") << "  " << iti->second.size()
+                        << " candidate instantiations for " << pv << " : "
+                        << std::endl;
+      // the order of instantiation ids we will try
+      std::vector<unsigned> inst_ids_try;
+      // until we have a model-preserving selection function for BV, this must
+      // be heuristic (we only pick one literal)
+      // hence we randomize the list
+      // this helps robustness, since picking the same literal every time may
+      // lead to a stream of value instantiations, whereas with randomization
+      // we may find an invertible literal that leads to a useful instantiation.
+      std::random_shuffle(iti->second.begin(), iti->second.end());
 
-    for( unsigned j=0; j<iti->second.size(); j++ ){
-      unsigned inst_id = iti->second[j];
-      Assert( d_inst_id_to_term.find(inst_id)!=d_inst_id_to_term.end() );
-      Node inst_term = d_inst_id_to_term[inst_id];
-      Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end());
-      Node alit = d_inst_id_to_alit[inst_id];
+      for (unsigned j = 0; j < iti->second.size(); j++) {
+        unsigned inst_id = iti->second[j];
+        Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
+        Node inst_term = d_inst_id_to_term[inst_id];
+        Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end());
+        Node alit = d_inst_id_to_alit[inst_id];
 
-      // get the slack value introduced for the asserted literal
-      Node curr_slack_val;
-      std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
-          d_alit_to_model_slack.find(alit);
-      if (itms != d_alit_to_model_slack.end()) {
-        curr_slack_val = itms->second;
-      }
-
-      // debug printing
-      if( Trace.isOn("cegqi-bv") ){
-        Trace("cegqi-bv") << "   [" << j << "] : ";
-        Trace("cegqi-bv") << inst_term << std::endl;
-        if (!curr_slack_val.isNull()) {
-          Trace("cegqi-bv") << "   ...with slack value : " << curr_slack_val
-                            << std::endl;
+        // get the slack value introduced for the asserted literal
+        Node curr_slack_val;
+        std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
+            d_alit_to_model_slack.find(alit);
+        if (itms != d_alit_to_model_slack.end()) {
+          curr_slack_val = itms->second;
         }
-        // process information about solved status
-        std::unordered_map< unsigned, BvInverterStatus >::iterator its = d_inst_id_to_status.find( inst_id );
-        Assert( its!=d_inst_id_to_status.end() );
-        if( !(*its).second.d_conds.empty() ){
-          Trace("cegqi-bv") << "   ...with " << (*its).second.d_conds.size() << " side conditions : " << std::endl;
-          for( unsigned k=0; k<(*its).second.d_conds.size(); k++ ){
-            Node cond = (*its).second.d_conds[k];
-            Trace("cegqi-bv") << "       " << cond << std::endl;
+
+        // debug printing
+        if (Trace.isOn("cegqi-bv")) {
+          Trace("cegqi-bv") << "   [" << j << "] : ";
+          Trace("cegqi-bv") << inst_term << std::endl;
+          if (!curr_slack_val.isNull()) {
+            Trace("cegqi-bv") << "   ...with slack value : " << curr_slack_val
+                              << std::endl;
+          }
+          // process information about solved status
+          std::unordered_map<unsigned, BvInverterStatus>::iterator its =
+              d_inst_id_to_status.find(inst_id);
+          Assert(its != d_inst_id_to_status.end());
+          if (!its->second.d_conds.empty()) {
+            Trace("cegqi-bv") << "   ...with " << its->second.d_conds.size()
+                              << " side conditions : " << std::endl;
+            for (unsigned k = 0; k < its->second.d_conds.size(); k++) {
+              Node cond = its->second.d_conds[k];
+              Trace("cegqi-bv") << "       " << cond << std::endl;
+            }
           }
+          Trace("cegqi-bv") << std::endl;
         }
-        Trace("cegqi-bv") << std::endl;
-      }
-
-      // currently we take select the first literal
-      if( inst_ids_try.empty() ){
-        // try the first one
-        inst_ids_try.push_back( inst_id );
-      } else {
-        // selection criteria across multiple literals goes here
-
 
+        // currently we select the first literal
+        if (inst_ids_try.empty()) {
+          // try the first one
+          inst_ids_try.push_back(inst_id);
+        } else {
+          // selection criteria across multiple literals goes here
+        }
       }
-    }
-    
-    // now, try all instantiation ids we want to try
-    // typically size( inst_ids_try )=0, otherwise worst-case performance for constructing
-    // instantiations is exponential on the number of variables in this quantifier
-    for( unsigned j = 0; j<inst_ids_try.size(); j++ ){
-      unsigned inst_id = iti->second[j];
-      Assert( d_inst_id_to_term.find(inst_id)!=d_inst_id_to_term.end() );
-      Node inst_term = d_inst_id_to_term[inst_id];
-      // try instantiation pv -> inst_term
-      TermProperties pv_prop_bv;
-      Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl;
-      d_var_to_curr_inst_id[pv] = inst_id;
-      if( ci->doAddInstantiationInc( pv, inst_term, pv_prop_bv, sf, effort ) ){
-        return true;
+
+      // now, try all instantiation ids we want to try
+      // typically size( inst_ids_try )=0, otherwise worst-case performance for
+      // constructing
+      // instantiations is exponential on the number of variables in this
+      // quantifier
+      for (unsigned j = 0; j < inst_ids_try.size(); j++) {
+        unsigned inst_id = iti->second[j];
+        Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
+        Node inst_term = d_inst_id_to_term[inst_id];
+        // try instantiation pv -> inst_term
+        TermProperties pv_prop_bv;
+        Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term
+                          << std::endl;
+        d_var_to_curr_inst_id[pv] = inst_id;
+        if (ci->doAddInstantiationInc(pv, inst_term, pv_prop_bv, sf, effort)) {
+          return true;
+        }
       }
+      Trace("cegqi-bv") << "...failed to add instantiation for " << pv
+                        << std::endl;
+      d_var_to_curr_inst_id.erase(pv);
+    } else {
+      Trace("cegqi-bv") << "...do not do instantiation for " << pv
+                        << " (skip, based on heuristic)" << std::endl;
     }
-    Trace("cegqi-bv") << "...failed to add instantiation for " << pv << std::endl;
-    d_var_to_curr_inst_id.erase( pv );
   }
 
   return false;
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 14e5244b4..ec24fdd8b 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -103,7 +103,12 @@ TESTS =	\
 	qbv-simple-2vars-vo.smt2 \
 	qbv-test-urem-rewrite.smt2 \
 	qbv-inequality2.smt2 \
-	qbv-test-invert-bvult-1.smt2
+	qbv-test-invert-bvult-1.smt2 \
+	intersection-example-onelane.proof-node22337.smt2 
+	
+# solved, but fail an assertion due to unhandled EXTRACT case
+#	nested9_true-unreach-call.i_575.smt2 
+#	small-pipeline-fixpoint-3.smt2
  
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2
new file mode 100644
index 000000000..38a4ed127
--- /dev/null
+++ b/test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun xI () (_ BitVec 32))
+(declare-fun A () (_ BitVec 32))
+(declare-fun B () (_ BitVec 32))
+(declare-fun vuscore2dollarskuscore80 () (_ BitVec 32))
+(declare-fun I1 () (_ BitVec 32))
+(declare-fun xuscore2dollarskuscore74 () (_ BitVec 32))
+(declare-fun v () (_ BitVec 32))
+(declare-fun ts49uscore0 () (_ BitVec 32))
+(declare-fun V () (_ BitVec 32))
+(declare-fun t87uscore0dollarskuscore0 () (_ BitVec 32))
+(declare-fun ep () (_ BitVec 32))
+(declare-fun I1uscore2dollarskuscore74 () (_ BitVec 32))
+(declare-fun x () (_ BitVec 32))
+(assert (not (exists ((ts49uscore0 (_ BitVec 32))) (let ((?v_0 (bvsge vuscore2dollarskuscore80 (_ bv0 32))) (?v_1 (bvsle vuscore2dollarskuscore80 V)) (?v_3 (bvsdiv (bvmul vuscore2dollarskuscore80 vuscore2dollarskuscore80) (bvmul (_ bv2 32) B))) (?v_2 (bvmul (bvsdiv (_ bv1 32) (_ bv2 32)) (bvadd (bvmul (bvmul (_ bv2 32) t87uscore0dollarskuscore0) vuscore2dollarskuscore80) (bvmul (_ bv2 32) xuscore2dollarskuscore74))))) (=> (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= I1uscore2dollarskuscore74 (_ bv2 32)) (=> (and (bvsle (_ bv0 32) ts49uscore0) (bvsle ts49uscore0 t87uscore0dollarskuscore0)) (and (and ?v_0 ?v_1) (bvsle ts49uscore0 ep)))) (bvsge t87uscore0dollarskuscore0 (_ bv0 32))) (= vuscore2dollarskuscore80 (_ bv0 32))) ?v_0) ?v_1) (bvsgt xI (bvadd xuscore2dollarskuscore74 ?v_3))) (= I1 (_ bv2 32))) (bvslt xI x)) (bvsgt B (_ bv0 32))) (bvsge v (_ bv0 32))) (bvsle v V)) (bvsge A (_ bv0 32))) (bvsgt V (_ bv0 32))) (bvsgt ep (_ bv0 32))) (or (or (= xI xuscore2dollarskuscore74) (bvslt xI ?v_2)) (bvsgt xI (bvadd ?v_2 ?v_3))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/quantifiers/nested9_true-unreach-call.i_575.smt2 b/test/regress/regress0/quantifiers/nested9_true-unreach-call.i_575.smt2
new file mode 100644
index 000000000..2a46d2a21
--- /dev/null
+++ b/test/regress/regress0/quantifiers/nested9_true-unreach-call.i_575.smt2
@@ -0,0 +1,21 @@
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun c_main_~i~6 () (_ BitVec 32))
+(declare-fun c_main_~j~6 () (_ BitVec 32))
+(declare-fun c_main_~k~6 () (_ BitVec 32))
+(assert
+ (and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32))
+ (exists ((v_nnf_34 (_ BitVec 32)))
+  (and (bvsle (bvadd v_nnf_34 (_ bv3 32)) c_main_~k~6) 
+  (bvsle v_nnf_34 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_34) (_ bv1 32)))))))
+(assert
+ (not
+ (and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32))
+ (exists ((v_nnf_30 (_ BitVec 32)))
+  (and (bvsle (bvadd v_nnf_30 (_ bv1 32)) c_main_~k~6) 
+  (bvsle v_nnf_30 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_30) (_ bv1 32))))))))
+(check-sat)
+(exit)
+
diff --git a/test/regress/regress0/quantifiers/small-pipeline-fixpoint-3.smt2 b/test/regress/regress0/quantifiers/small-pipeline-fixpoint-3.smt2
new file mode 100644
index 000000000..378912490
--- /dev/null
+++ b/test/regress/regress0/quantifiers/small-pipeline-fixpoint-3.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --cbqi-bv --no-check-models
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(assert (forall ((Verilog__main.dataOut_64_0 (_ BitVec 32))) (forall ((Verilog__main.stageOne_64_0 (_ BitVec 32))) (forall ((Verilog__main.stageTwo_64_0 (_ BitVec 32))) (forall ((Verilog__main.tmp_stageOne_64_0 (_ BitVec 32))) (forall ((Verilog__main.tmp_stageTwo_64_0 (_ BitVec 32))) (forall ((Verilog__main.dataOut_64_1 (_ BitVec 32))) (forall ((Verilog__main.reset_64_0 Bool)) (forall ((Verilog__main.stageOne_64_1 (_ BitVec 32))) (forall ((Verilog__main.dataIn_64_0 (_ BitVec 32))) (forall ((Verilog__main.c1_64_0 (_ BitVec 32))) (forall ((Verilog__main.stageTwo_64_1 (_ BitVec 32))) (forall ((Verilog__main.c2_64_0 (_ BitVec 32))) (forall ((Verilog__main.tmp_stageOne_64_1 (_ BitVec 32))) (forall ((Verilog__main.tmp_stageTwo_64_1 (_ BitVec 32))) (forall ((Verilog__main.dataOut_64_2 (_ BitVec 32))) (forall ((Verilog__main.reset_64_1 Bool)) (forall ((Verilog__main.stageOne_64_2 (_ BitVec 32))) (forall ((Verilog__main.dataIn_64_1 (_ BitVec 32))) (forall ((Verilog__main.c1_64_1 (_ BitVec 32))) (forall ((Verilog__main.stageTwo_64_2 (_ BitVec 32))) (forall ((Verilog__main.c2_64_1 (_ BitVec 32))) (forall ((Verilog__main.tmp_stageOne_64_2 (_ BitVec 32))) (forall ((Verilog__main.tmp_stageTwo_64_2 (_ BitVec 32))) (forall ((Verilog__main.dataOut_64_3 (_ BitVec 32))) (forall ((Verilog__main.reset_64_2 Bool)) (forall ((Verilog__main.stageOne_64_3 (_ BitVec 32))) (forall ((Verilog__main.dataIn_64_2 (_ BitVec 32))) (forall ((Verilog__main.c1_64_2 (_ BitVec 32))) (forall ((Verilog__main.stageTwo_64_3 (_ BitVec 32))) (forall ((Verilog__main.c2_64_2 (_ BitVec 32))) (forall ((Verilog__main.tmp_stageOne_64_3 (_ BitVec 32))) (forall ((Verilog__main.tmp_stageTwo_64_3 (_ BitVec 32))) (exists ((Verilog__main.dataOut_64_0_39_ (_ BitVec 32))) (exists ((Verilog__main.stageOne_64_0_39_ (_ BitVec 32))) (exists ((Verilog__main.stageTwo_64_0_39_ (_ BitVec 32))) (exists ((Verilog__main.tmp_stageOne_64_0_39_ (_ BitVec 32))) (exists ((Verilog__main.tmp_stageTwo_64_0_39_ (_ BitVec 32))) (exists ((Verilog__main.dataOut_64_1_39_ (_ BitVec 32))) (exists ((Verilog__main.reset_64_0_39_ Bool)) (exists ((Verilog__main.stageOne_64_1_39_ (_ BitVec 32))) (exists ((Verilog__main.dataIn_64_0_39_ (_ BitVec 32))) (exists ((Verilog__main.c1_64_0_39_ (_ BitVec 32))) (exists ((Verilog__main.stageTwo_64_1_39_ (_ BitVec 32))) (exists ((Verilog__main.c2_64_0_39_ (_ BitVec 32))) (exists ((Verilog__main.tmp_stageOne_64_1_39_ (_ BitVec 32))) (exists ((Verilog__main.tmp_stageTwo_64_1_39_ (_ BitVec 32))) (exists ((Verilog__main.dataOut_64_2_39_ (_ BitVec 32))) (exists ((Verilog__main.reset_64_1_39_ Bool)) (exists ((Verilog__main.stageOne_64_2_39_ (_ BitVec 32))) (exists ((Verilog__main.dataIn_64_1_39_ (_ BitVec 32))) (exists ((Verilog__main.c1_64_1_39_ (_ BitVec 32))) (exists ((Verilog__main.stageTwo_64_2_39_ (_ BitVec 32))) (exists ((Verilog__main.c2_64_1_39_ (_ BitVec 32))) (exists ((Verilog__main.tmp_stageOne_64_2_39_ (_ BitVec 32))) (exists ((Verilog__main.tmp_stageTwo_64_2_39_ (_ BitVec 32))) (=> (and (and (= Verilog__main.dataOut_64_0 (_ bv0 32)) (= Verilog__main.stageOne_64_0 (_ bv0 32)) (= Verilog__main.stageTwo_64_0 (_ bv0 32)) (= Verilog__main.tmp_stageOne_64_0 (_ bv0 32)) (= Verilog__main.tmp_stageTwo_64_0 (_ bv0 32))) (and (= Verilog__main.dataOut_64_1 (ite (not Verilog__main.reset_64_0) (bvadd Verilog__main.stageTwo_64_0 Verilog__main.stageOne_64_0) (_ bv0 32))) (= Verilog__main.stageOne_64_1 (bvadd Verilog__main.dataIn_64_0 Verilog__main.c1_64_0)) (= Verilog__main.stageTwo_64_1 (bvand Verilog__main.stageOne_64_0 Verilog__main.c2_64_0)) (= Verilog__main.tmp_stageOne_64_1 Verilog__main.stageOne_64_0) (= Verilog__main.tmp_stageTwo_64_1 Verilog__main.stageTwo_64_0)) (and (= Verilog__main.dataOut_64_2 (ite (not Verilog__main.reset_64_1) (bvadd Verilog__main.stageTwo_64_1 Verilog__main.stageOne_64_1) (_ bv0 32))) (= Verilog__main.stageOne_64_2 (bvadd Verilog__main.dataIn_64_1 Verilog__main.c1_64_1)) (= Verilog__main.stageTwo_64_2 (bvand Verilog__main.stageOne_64_1 Verilog__main.c2_64_1)) (= Verilog__main.tmp_stageOne_64_2 Verilog__main.stageOne_64_1) (= Verilog__main.tmp_stageTwo_64_2 Verilog__main.stageTwo_64_1)) (and (= Verilog__main.dataOut_64_3 (ite (not Verilog__main.reset_64_2) (bvadd Verilog__main.stageTwo_64_2 Verilog__main.stageOne_64_2) (_ bv0 32))) (= Verilog__main.stageOne_64_3 (bvadd Verilog__main.dataIn_64_2 Verilog__main.c1_64_2)) (= Verilog__main.stageTwo_64_3 (bvand Verilog__main.stageOne_64_2 Verilog__main.c2_64_2)) (= Verilog__main.tmp_stageOne_64_3 Verilog__main.stageOne_64_2) (= Verilog__main.tmp_stageTwo_64_3 Verilog__main.stageTwo_64_2))) (and (and (and (= Verilog__main.dataOut_64_0_39_ (_ bv0 32)) (= Verilog__main.stageOne_64_0_39_ (_ bv0 32)) (= Verilog__main.stageTwo_64_0_39_ (_ bv0 32)) (= Verilog__main.tmp_stageOne_64_0_39_ (_ bv0 32)) (= Verilog__main.tmp_stageTwo_64_0_39_ (_ bv0 32))) (and (= Verilog__main.dataOut_64_1_39_ (ite (not Verilog__main.reset_64_0_39_) (bvadd Verilog__main.stageTwo_64_0_39_ Verilog__main.stageOne_64_0_39_) (_ bv0 32))) (= Verilog__main.stageOne_64_1_39_ (bvadd Verilog__main.dataIn_64_0_39_ Verilog__main.c1_64_0_39_)) (= Verilog__main.stageTwo_64_1_39_ (bvand Verilog__main.stageOne_64_0_39_ Verilog__main.c2_64_0_39_)) (= Verilog__main.tmp_stageOne_64_1_39_ Verilog__main.stageOne_64_0_39_) (= Verilog__main.tmp_stageTwo_64_1_39_ Verilog__main.stageTwo_64_0_39_)) (and (= Verilog__main.dataOut_64_2_39_ (ite (not Verilog__main.reset_64_1_39_) (bvadd Verilog__main.stageTwo_64_1_39_ Verilog__main.stageOne_64_1_39_) (_ bv0 32))) (= Verilog__main.stageOne_64_2_39_ (bvadd Verilog__main.dataIn_64_1_39_ Verilog__main.c1_64_1_39_)) (= Verilog__main.stageTwo_64_2_39_ (bvand Verilog__main.stageOne_64_1_39_ Verilog__main.c2_64_1_39_)) (= Verilog__main.tmp_stageOne_64_2_39_ Verilog__main.stageOne_64_1_39_) (= Verilog__main.tmp_stageTwo_64_2_39_ Verilog__main.stageTwo_64_1_39_))) (or (and (= Verilog__main.dataOut_64_3 Verilog__main.dataOut_64_0_39_) (= Verilog__main.stageOne_64_3 Verilog__main.stageOne_64_0_39_) (= Verilog__main.stageTwo_64_3 Verilog__main.stageTwo_64_0_39_) (= Verilog__main.tmp_stageOne_64_3 Verilog__main.tmp_stageOne_64_0_39_) (= Verilog__main.tmp_stageTwo_64_3 Verilog__main.tmp_stageTwo_64_0_39_)) (and (= Verilog__main.dataOut_64_3 Verilog__main.dataOut_64_1_39_) (= Verilog__main.stageOne_64_3 Verilog__main.stageOne_64_1_39_) (= Verilog__main.stageTwo_64_3 Verilog__main.stageTwo_64_1_39_) (= Verilog__main.tmp_stageOne_64_3 Verilog__main.tmp_stageOne_64_1_39_) (= Verilog__main.tmp_stageTwo_64_3 Verilog__main.tmp_stageTwo_64_1_39_)) (and (= Verilog__main.dataOut_64_3 Verilog__main.dataOut_64_2_39_) (= Verilog__main.stageOne_64_3 Verilog__main.stageOne_64_2_39_) (= Verilog__main.stageTwo_64_3 Verilog__main.stageTwo_64_2_39_) (= Verilog__main.tmp_stageOne_64_3 Verilog__main.tmp_stageOne_64_2_39_) (= Verilog__main.tmp_stageTwo_64_3 Verilog__main.tmp_stageTwo_64_2_39_))))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
+(check-sat)
+(exit)