Merge branch 'master' of https://github.com/CVC4/CVC4

12 files changed, 95 insertions, 108 deletions

diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4
index a1a8cb786..c96bbe03d 100755
--- a/contrib/get-cryptominisat4
+++ b/contrib/get-cryptominisat4
@@ -47,7 +47,7 @@ patch -p0 < ../../contrib/cryptominisat-4.2.0.second.patch
 mkdir ../build
 cd ../build
 
-cmake -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH/install -DSTATICCOMPILE="ON" ../cryptominisat-$version
+cmake -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH/install -DSTATICCOMPILE="ON" -DNOM4RI="ON"  ../cryptominisat-$version
 make install -j2
 
 cd ../
diff --git a/contrib/run-script-smtcomp2016 b/contrib/run-script-smtcomp2016
index 0db378a80..ad036ad05 100644
--- a/contrib/run-script-smtcomp2016
+++ b/contrib/run-script-smtcomp2016
@@ -41,7 +41,7 @@ QF_NIA)
   trywith 1800 --solve-int-as-bv=16 --bitblast=eager
   finishwith --solve-int-as-bv=32 --bitblast=eager
   ;;
-ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA)
   # the following is designed for a run time of 2400s (40 min).
   # initial runs 1min
   trywith 20 --simplification=none --full-saturate-quant
@@ -72,8 +72,14 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   # finish 12min
   finishwith --full-saturate-quant
   ;;
+UFBV)
+  # many problems in UFBV are essentially BV
+  trywith 300 --full-saturate-quant 
+  trywith 300 --finite-model-find
+  finishwith --cbqi-all --full-saturate-quant
+  ;;
 BV)
-  trywith 30 --finite-model-find
+  trywith 300 --finite-model-find
   finishwith --cbqi-all --full-saturate-quant
   ;;
 LIA|LRA|NIA|NRA)
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 80a9396ac..37e9f4476 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -19,7 +19,7 @@
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
-
+#include "smt/smt_statistics_registry.h"
 
 #ifdef CVC4_USE_ABC
 // Function is defined as static in ABC. Not sure how else to do this. 
@@ -144,7 +144,8 @@ AigBitblaster::AigBitblaster()
   switch(options::bvSatSolver()) {
   case SAT_SOLVER_MINISAT: {
     prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext,
-										"AigBitblaster");
+                                                                                smtStatisticsRegistry(),
+                                                                                "AigBitblaster");
     MinisatEmptyNotify* notify = new MinisatEmptyNotify();
     minisat->setNotify(notify);
     d_satSolver = minisat;
@@ -415,7 +416,7 @@ void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
       prop::SatLiteral lit(sat_variables[index-1], int_lit < 0); 
       clause.push_back(lit); 
     }
-    d_satSolver->addClause(clause, false, RULE_INVALID);
+    d_satSolver->addClause(clause, false);
   }
 }
 
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index f9f5361d3..929bccada 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -306,7 +306,7 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
   
   static Abc_Ntk_t* abcAigNetwork;
   context::Context* d_nullContext;
-  prop::BVSatSolverInterface* d_satSolver;
+  prop::SatSolver* d_satSolver;
   TNodeAigMap d_aigCache;
   NodeAigMap d_bbAtoms;
   
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 80066d690..a00d6d8a1 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -30,17 +30,30 @@ struct sortTypeOrder {
 };
 
 Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
+  std::map< Node, bool > visited;
   while( !tt.empty() ){
     if( tt.size()==arg_index.size()+1 ){
       Node t = tt.back();
-      Node op = t.hasOperator() ? t.getOperator() : t;
-      arg_index.push_back( 0 );
+      Node op;
+      if( t.hasOperator() ){
+        if( visited.find( t )==visited.end() ){
+          visited[t] = true;
+          op = t.getOperator();
+          arg_index.push_back( 0 );
+        }else{
+          op = t;
+          arg_index.push_back( -1 );
+        }
+      }else{
+        op = t;
+        arg_index.push_back( 0 );
+      }
       Trace("aeq-debug") << op << " ";
       aen = &(aen->d_children[op][t.getNumChildren()]);
     }else{
       Node t = tt.back();
       int i = arg_index.back();
-      if( i==(int)t.getNumChildren() ){
+      if( i==-1 || i==(int)t.getNumChildren() ){
         tt.pop_back();
         arg_index.pop_back();
       }else{
@@ -56,9 +69,9 @@ Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE
   }else{
     if( q.getNumChildren()==2 ){
       //lemma ( q <=> d_quant )
-      Trace("quant-ae") << "Alpha equivalent : " << std::endl;
-      Trace("quant-ae") << "  " << q << std::endl;
-      Trace("quant-ae") << "  " << aen->d_quant << std::endl;
+      Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
+      Trace("alpha-eq") << "  " << q << std::endl;
+      Trace("alpha-eq") << "  " << aen->d_quant << std::endl;
       lem = q.iffNode( aen->d_quant );
     }else{
       //do not reduce annotated quantified formulas based on alpha equivalence 
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 7489196b7..cd263e90c 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -22,6 +22,9 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
 
+#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
+
 //#define MBP_STRICT_ASSERTIONS
 
 using namespace std;
@@ -466,6 +469,36 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                 }
               }
             }
+            /*   TODO: algebraic reasoning for bitvector instantiation
+            else if( pvtn.isBitVector() ){
+              if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){
+                for( unsigned t=0; t<2; t++ ){
+                  if( atom[t]==pv ){
+                    computeProgVars( atom[1-t] );
+                    if( d_inelig.find( atom[1-t] )==d_inelig.end() ){
+                      //only ground terms  TODO: more
+                      if( d_prog_var[atom[1-t]].empty() ){
+                        Node veq_c;
+                        Node uval;
+                        if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){
+                          uval = atom[1-t];
+                        }else{
+                          uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], 
+                                                                   bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) );
+                        }
+                        if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
+                          subs_proc[uval][veq_c] = true;
+                          if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                            return true;
+                          }
+                        }
+                      }
+                    }
+                  }
+                }
+              }
+            }
+            */
           }
         }
       }
@@ -685,7 +718,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
 
     //[5] resort to using value in model
     // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype
-    if( ( effort>0 || pvtn.isBoolean() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){
+    if( ( effort>0 || pvtn.isBoolean() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){
       Node mv = getModelValue( pv );
       Node pv_coeff_m;
       Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 5c28e4ab5..d1685bdd1 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -433,7 +433,7 @@ void TheoryUF::addSharedTerm(TNode t) {
   d_equalityEngine.addTriggerTerm(t, THEORY_UF);
 }
 
-/*
+//TODO: move quantifiers::TermArgTrie to src/theory/
 void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ){
   if( depth==arity ){
     if( t2!=NULL ){
@@ -498,13 +498,11 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
     }
   }
 }
-*/
 
 void TheoryUF::computeCareGraph() {
 
   if (d_sharedTerms.size() > 0) {
-
-/*  TODO : this does (almost) the same as below, and is 1-2 order of magnitudes faster
+    //use term indexing 
     Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
     std::map< Node, quantifiers::TermArgTrie > index;
     std::map< Node, unsigned > arity;
@@ -530,92 +528,6 @@ void TheoryUF::computeCareGraph() {
       Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
       addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
     }
- */
-    vector< pair<TNode, TNode> > currentPairs;
-
-    // Go through the function terms and see if there are any to split on
-    unsigned functionTerms = d_functionsTerms.size();
-    for (unsigned i = 0; i < functionTerms; ++ i) {
-
-      TNode f1 = d_functionsTerms[i];
-      Node op = f1.getOperator();
-
-      for (unsigned j = i + 1; j < functionTerms; ++ j) {
-
-        TNode f2 = d_functionsTerms[j];
-
-        // If the operators are not the same, we can skip this pair
-        if (f2.getOperator() != op) {
-          continue;
-        }
-
-        Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
-
-        // If the terms are already known to be equal, we are also in good shape
-        if (d_equalityEngine.areEqual(f1, f2)) {
-          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal, skipping" << std::endl;
-          continue;
-        }
-
-        // We have two functions f(x1, ..., xn) and f(y1, ..., yn) no known to be equal
-        // We split on the argument pairs that are are not known, unless there is some
-        // argument pair that is already dis-equal.
-        bool somePairIsDisequal = false;
-        currentPairs.clear();
-        for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
-
-          TNode x = f1[k];
-          TNode y = f2[k];
-
-          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking arguments " << x << " and " << y << std::endl;
-
-          if (d_equalityEngine.areDisequal(x, y, false)) {
-            // Mark that there is a dis-equal pair and break
-            somePairIsDisequal = true;
-            Debug("uf::sharing") << "TheoryUf::computeCareGraph(): disequal, disregarding all" << std::endl;
-            break;
-          }
-
-          if (d_equalityEngine.areEqual(x, y)) {
-            // We don't need this one
-            Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal" << std::endl;
-            continue;
-          }
-
-          if (!d_equalityEngine.isTriggerTerm(x, THEORY_UF) || !d_equalityEngine.isTriggerTerm(y, THEORY_UF)) {
-            // Not connected to shared terms, we don't care
-            continue;
-          }
-
-          // Get representative trigger terms
-          TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
-          TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
-
-          EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
-          switch (eqStatusDomain) {
-          case EQUALITY_FALSE_AND_PROPAGATED:
-          case EQUALITY_FALSE:
-          case EQUALITY_FALSE_IN_MODEL:
-            somePairIsDisequal = true;
-            continue;
-            break;
-          default:
-            break;
-            // nothing
-          }
-
-          // Otherwise, we need to figure it out
-          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl;
-          currentPairs.push_back(make_pair(x_shared, y_shared));
-        }
-
-        if (!somePairIsDisequal) {
-          for (unsigned i = 0; i < currentPairs.size(); ++ i) {
-            addCarePair(currentPairs[i].first, currentPairs[i].second);
-          }
-        }
-      }
-    }
   }
 }/* TheoryUF::computeCareGraph() */
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index ff7d7419a..3a83decec 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -209,8 +209,8 @@ public:
   StrongSolverTheoryUF* getStrongSolver() {
     return d_thss;
   }
-//private:
-  //void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
+private:
+  void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index ed28cc2fc..cda94e1c4 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1670,6 +1670,12 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
   }
 }
 
+StrongSolverTheoryUF::~StrongSolverTheoryUF() { 
+  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+    delete it->second;
+  }
+}
+
 SortInference* StrongSolverTheoryUF::getSortInference() {
   return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference();
 }
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 11f0664f3..4e4dbef83 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -414,7 +414,7 @@ private:
   SubsortSymmetryBreaker* d_sym_break;
 public:
   StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th);
-  ~StrongSolverTheoryUF() {}
+  ~StrongSolverTheoryUF();
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
   /** disequality propagator */
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 14e7da5da..f6d65958e 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -81,7 +81,8 @@ TESTS =	\
 	qcf-rel-dom-opt.smt2 \
 	parametric-lists.smt2 \
 	partial-trigger.smt2 \
-	inst-max-level-segf.smt2
+	inst-max-level-segf.smt2 \
+	small-bug1-fixpoint-3.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 b/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2
new file mode 100644
index 000000000..da48f5e68
--- /dev/null
+++ b/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --cbqi-all --no-check-models
+; EXPECT: sat
+(set-logic UFBV)
+(set-info :status sat)
+(declare-fun Verilog__main.impl_PC_valid_64_1_39_!3 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun Verilog__main.impl_flush_64_1_39_!1 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun Verilog__main.reset_64_0_39_!4 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun Verilog__main.impl_PC_valid_64_2_39_!6 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun Verilog__main.impl_flush_64_0_39_!0 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun Verilog__main.reset_64_1_39_!7 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun Verilog__main.impl_PC_valid_64_0_39_!5 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
+(declare-fun Verilog__main.impl_flush_64_2_39_!2 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
+(assert (forall ((Verilog__main.impl_flush_64_0 Bool) (Verilog__main.impl_flush_64_1 Bool) (Verilog__main.impl_flush_64_2 Bool) (Verilog__main.impl_flush_64_3 Bool) (Verilog__main.impl_PC_valid_64_1 Bool) (Verilog__main.reset_64_0 Bool) (Verilog__main.impl_PC_valid_64_0 Bool) (Verilog__main.impl_PC_valid_64_2 Bool) (Verilog__main.reset_64_1 Bool) (Verilog__main.impl_PC_valid_64_3 Bool) (Verilog__main.reset_64_2 Bool)) (=> (and (= Verilog__main.impl_flush_64_0 false) (= Verilog__main.impl_flush_64_1 false) (= Verilog__main.impl_flush_64_2 false) (= Verilog__main.impl_flush_64_3 false) (= Verilog__main.impl_PC_valid_64_1 (ite Verilog__main.reset_64_0 true (ite Verilog__main.impl_flush_64_0 false Verilog__main.impl_PC_valid_64_0))) (= Verilog__main.impl_PC_valid_64_2 (ite Verilog__main.reset_64_1 true (ite Verilog__main.impl_flush_64_1 false Verilog__main.impl_PC_valid_64_1))) (= Verilog__main.impl_PC_valid_64_3 (ite Verilog__main.reset_64_2 true (ite Verilog__main.impl_flush_64_2 false Verilog__main.impl_PC_valid_64_2)))) (and (= (Verilog__main.impl_flush_64_0_39_!0 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false) (= (Verilog__main.impl_flush_64_1_39_!1 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false) (= (Verilog__main.impl_flush_64_2_39_!2 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false) (= (Verilog__main.impl_PC_valid_64_1_39_!3 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) (ite (Verilog__main.reset_64_0_39_!4 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) true (ite (Verilog__main.impl_flush_64_0_39_!0 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false (Verilog__main.impl_PC_valid_64_0_39_!5 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)))) (= (Verilog__main.impl_PC_valid_64_2_39_!6 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) (ite (Verilog__main.reset_64_1_39_!7 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) true (ite (Verilog__main.impl_flush_64_1_39_!1 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false (Verilog__main.impl_PC_valid_64_1_39_!3 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)))) (or (and (= Verilog__main.impl_flush_64_3 (Verilog__main.impl_flush_64_0_39_!0 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)) (= Verilog__main.impl_PC_valid_64_3 (Verilog__main.impl_PC_valid_64_0_39_!5 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0))) (and (= Verilog__main.impl_flush_64_3 (Verilog__main.impl_flush_64_1_39_!1 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)) (= Verilog__main.impl_PC_valid_64_3 (Verilog__main.impl_PC_valid_64_1_39_!3 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0))) (and (= Verilog__main.impl_flush_64_3 (Verilog__main.impl_flush_64_2_39_!2 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)) (= Verilog__main.impl_PC_valid_64_3 (Verilog__main.impl_PC_valid_64_2_39_!6 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)))))) ))
+(check-sat)
+(exit)