From: Andrew Reynolds Date: Fri, 13 Oct 2017 05:12:02 +0000 (-0500) Subject: CBQI BV quick heuristics (#1239) X-Git-Tag: cvc5-1.0.0~5557 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39a85cc99f3b9f3d203490f5918ebe56bd916d64;p=cvc5.git 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. --- 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(), one); + Node bv_one = NodeManager::currentNM()->mkConst(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 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; jsecond.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::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::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::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; jsecond[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)