Merge branch 'master' into run_new_logicsrun_new_logics

46 files changed, 856 insertions, 272 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 097b41d93..2836f73b4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2071,11 +2071,15 @@ void SmtEngine::setDefaults() {
   }
   //counterexample-guided instantiation for non-sygus
   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
-  if( d_logic.isQuantified() && 
-      ( ( options::decisionMode()!=decision::DECISION_STRATEGY_INTERNAL &&
-          ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) ||
-        d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV) ||
-        options::cbqiAll() ) ){
+  if (d_logic.isQuantified()
+      && ((options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL
+           && (d_logic.isTheoryEnabled(THEORY_ARITH)
+               || d_logic.isTheoryEnabled(THEORY_DATATYPES)
+               || d_logic.isTheoryEnabled(THEORY_BV)
+               || d_logic.isTheoryEnabled(THEORY_FP)))
+          || d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)
+          || options::cbqiAll()))
+  {
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
     }
@@ -2093,6 +2097,11 @@ void SmtEngine::setDefaults() {
     if( !options::rewriteDivk.wasSetByUser()) {
       options::rewriteDivk.set( true );
     }
+    if (options::incrementalSolving())
+    {
+      // cannot do nested quantifier elimination in incremental mode
+      options::cbqiNestedQE.set(false);
+    }
     if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
     {
       options::cbqiAll.set( false );
@@ -2354,10 +2363,12 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   }
 
   // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
-  if(key == "source" ||
-     key == "category" ||
-     key == "difficulty" ||
-     key == "notes") {
+  if (key == "source"
+   || key == "category"
+   || key == "difficulty"
+   || key == "notes"
+   || key == "license")
+  {
     // ignore these
     return;
   } else if(key == "name") {
diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp
index 46ee1cad5..c56587901 100644
--- a/src/theory/arith/arith_msum.cpp
+++ b/src/theory/arith/arith_msum.cpp
@@ -148,6 +148,7 @@ Node ArithMSum::mkNode(const std::map<Node, Node>& msum)
 int ArithMSum::isolate(
     Node v, const std::map<Node, Node>& msum, Node& veq_c, Node& val, Kind k)
 {
+  Assert(veq_c.isNull());
   std::map<Node, Node>::const_iterator itv = msum.find(v);
   if (itv != msum.end())
   {
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index dfa543ff3..87edbe316 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -659,6 +659,16 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     // The may equal needs the store
     d_mayEqualEqualityEngine.addTerm(store);
 
+    if (node.getType().isArray())
+    {
+      d_mayEqualEqualityEngine.addTerm(node);
+      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
+    }
+    else
+    {
+      d_equalityEngine.addTerm(node);
+    }
+
     if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) {
       // Apply RIntro1 rule to any stores equal to store if not done already
       const CTNodeList* stores = d_infoMap.getStores(store);
@@ -679,14 +689,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
       }
     }
 
-    if (node.getType().isArray()) {
-      d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
-    }
-    else {
-      d_equalityEngine.addTerm(node);
-    }
-
     Assert(d_equalityEngine.getRepresentative(store) == store);
     d_infoMap.addIndex(store, node[1]);
 
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index c04e8bde9..f0c1d5488 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -36,13 +36,14 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions,
 
   TimerStat::CodeTimer abstractionTimer(d_statistics.d_abstractionTime);
 
+  TNodeSet seen;
   for (unsigned i = 0; i < assertions.size(); ++i)
   {
     if (assertions[i].getKind() == kind::OR)
     {
       for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j)
       {
-        if (!isConjunctionOfAtoms(assertions[i][j]))
+        if (!isConjunctionOfAtoms(assertions[i][j], seen))
         {
           continue;
         }
@@ -107,25 +108,24 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions,
   return d_funcToSignature.size() != 0;
 }
 
-bool AbstractionModule::isConjunctionOfAtoms(TNode node) {
-  TNodeSet seen;
-  return isConjunctionOfAtomsRec(node, seen);
-}
-
-bool AbstractionModule::isConjunctionOfAtomsRec(TNode node, TNodeSet& seen) {
+bool AbstractionModule::isConjunctionOfAtoms(TNode node, TNodeSet& seen)
+{
   if (seen.find(node)!= seen.end())
     return true;
 
-  if (!node.getType().isBitVector()) {
-    return (node.getKind() == kind::AND || utils::isBVPredicate(node));
+  if (!node.getType().isBitVector() && node.getKind() != kind::AND)
+  {
+    return utils::isBVPredicate(node);
   }
 
   if (node.getNumChildren() == 0)
     return true;
 
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-    if (!isConjunctionOfAtomsRec(node[i], seen))
+    if (!isConjunctionOfAtoms(node[i], seen))
+    {
       return false;
+    }
   }
   seen.insert(node);
   return true;
@@ -276,7 +276,7 @@ Node AbstractionModule::computeSignature(TNode node) {
 
 Node AbstractionModule::getSignatureSkolem(TNode node)
 {
-  Assert(node.getKind() == kind::VARIABLE);
+  Assert(node.getMetaKind() == kind::metakind::VARIABLE);
   NodeManager* nm = NodeManager::currentNM();
   unsigned bitwidth = utils::getSize(node);
   if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end())
@@ -550,8 +550,9 @@ void AbstractionModule::collectArguments(TNode node, TNode signature, std::vecto
   if (seen.find(node)!= seen.end())
     return;
 
-  if (node.getKind() == kind::VARIABLE ||
-      node.getKind() == kind::CONST_BITVECTOR) {
+  if (node.getMetaKind() == kind::metakind::VARIABLE
+      || node.getKind() == kind::CONST_BITVECTOR)
+  {
     // a constant in the node can either map to an argument of the abstraction
     // or can be hard-coded and part of the abstraction
     if (signature.getKind() == kind::SKOLEM) {
@@ -666,8 +667,7 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign
   }
 
   if (signature.getNumChildren() == 0) {
-    Assert (signature.getKind() != kind::VARIABLE &&
-            signature.getKind() != kind::SKOLEM);
+    Assert(signature.getKind() != kind::metakind::VARIABLE);
     seen[signature] = signature;
     return signature;
   }
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 0d7e0ff2a..cc78a550a 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -155,8 +155,7 @@ class AbstractionModule {
   Node abstractSignatures(TNode assertion);
   Node computeSignature(TNode node);
 
-  bool isConjunctionOfAtoms(TNode node);
-  bool isConjunctionOfAtomsRec(TNode node, TNodeSet& seen);
+  bool isConjunctionOfAtoms(TNode node, TNodeSet& seen);
 
   TNode getGeneralization(TNode term);
   void storeGeneralization(TNode s, TNode t);
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 7e666bcbf..80930866f 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -139,7 +139,8 @@ AigBitblaster::AigBitblaster()
       d_nullContext(new context::Context()),
       d_aigCache(),
       d_bbAtoms(),
-      d_aigOutputNode(NULL)
+      d_aigOutputNode(NULL),
+      d_notify()
 {
   prop::SatSolver* solver = nullptr;
   switch (options::bvSatSolver())
@@ -149,8 +150,8 @@ AigBitblaster::AigBitblaster()
       prop::BVSatSolverInterface* minisat =
           prop::SatSolverFactory::createMinisat(
               d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster");
-      MinisatEmptyNotify notify;
-      minisat->setNotify(&notify);
+      d_notify.reset(new MinisatEmptyNotify());
+      minisat->setNotify(d_notify.get());
       solver = minisat;
       break;
     }
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 30f1dd00b..dea2d0429 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -67,6 +67,8 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
   // the thing we are checking for sat
   Abc_Obj_t* d_aigOutputNode;
 
+  std::unique_ptr<MinisatEmptyNotify> d_notify;
+
   void addAtom(TNode atom);
   void simplifyAig();
   void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 496066ebc..574f2e0f0 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -980,6 +980,7 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND];
     preRewriteTable[kind::VARIABLE] = rewrite::variable;
     preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
     preRewriteTable[kind::SKOLEM] = rewrite::variable;
+    preRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
 
     preRewriteTable[kind::EQUAL] = rewrite::equal;
 
@@ -1062,6 +1063,7 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND];
     postRewriteTable[kind::VARIABLE] = rewrite::variable;
     postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
     postRewriteTable[kind::SKOLEM] = rewrite::variable;
+    postRewriteTable[kind::INST_CONSTANT] = rewrite::variable;
 
     postRewriteTable[kind::EQUAL] = rewrite::equal;
 
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 72633e86f..b18ebcdce 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -153,7 +153,8 @@ CegHandledStatus CegInstantiator::isCbqiKind(Kind k)
 
   // CBQI typically works for satisfaction-complete theories
   TheoryId t = kindToTheoryId(k);
-  if (t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL)
+  if (t == THEORY_BV || t == THEORY_FP || t == THEORY_DATATYPES
+      || t == THEORY_BOOL)
   {
     return CEG_HANDLED;
   }
@@ -221,7 +222,8 @@ CegHandledStatus CegInstantiator::isCbqiSort(
     return itv->second;
   }
   CegHandledStatus ret = CEG_UNHANDLED;
-  if (tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector())
+  if (tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector()
+      || tn.isFloatingPoint())
   {
     ret = CEG_HANDLED;
   }
@@ -1475,6 +1477,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 +1503,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 +1550,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/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
index 203697fd7..0274d45cd 100644
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -198,6 +198,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
         Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) );
         //re-isolate
         Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
+        veq_c = Node::null();
         ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
         Trace("cegqi-arith-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
         Trace("cegqi-arith-debug") << "                 real part : " << realPart << std::endl;
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index 4b79c4e79..678d87156 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -344,39 +344,46 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis
   }
 }
 
-void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
+void InstStrategyCbqi::checkOwnership(Node q)
+{
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
     if (d_do_cbqi[q] == CEG_HANDLED)
     {
       //take full ownership of the quantified formula
       d_quantEngine->setOwner( q, this );
-      
-      //mark all nested quantifiers with id
-      if( options::cbqiNestedQE() ){
-        std::map< Node, Node > visited;
-        Node mq = getIdMarkedQuantNode( q[1], visited );
-        if( mq!=q[1] ){
-          // do not do cbqi, we are reducing this quantified formula to a marked
-          // one
-          d_do_cbqi[q] = CEG_UNHANDLED;
-          //instead do reduction
-          std::vector< Node > qqc;
-          qqc.push_back( q[0] );
-          qqc.push_back( mq );
-          if( q.getNumChildren()==3 ){
-            qqc.push_back( q[2] );
-          }
-          Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc );
-          Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq );
-          Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
-          d_quantEngine->getOutputChannel().lemma( mlem );
-        }
-      }
     }
   }
 }
 
-void InstStrategyCbqi::registerQuantifier( Node q ) {
+void InstStrategyCbqi::preRegisterQuantifier(Node q)
+{
+  // mark all nested quantifiers with id
+  if (options::cbqiNestedQE())
+  {
+    if( d_quantEngine->getOwner(q)==this )
+    {
+      std::map<Node, Node> visited;
+      Node mq = getIdMarkedQuantNode(q[1], visited);
+      if (mq != q[1])
+      {
+        // do not do cbqi, we are reducing this quantified formula to a marked
+        // one
+        d_do_cbqi[q] = CEG_UNHANDLED;
+        // instead do reduction
+        std::vector<Node> qqc;
+        qqc.push_back(q[0]);
+        qqc.push_back(mq);
+        if (q.getNumChildren() == 3)
+        {
+          qqc.push_back(q[2]);
+        }
+        Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc);
+        Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq);
+        Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
+        d_quantEngine->addLemma(mlem);
+      }
+    }
+  }
   if( doCbqi( q ) ){
     if( registerCbqiLemma( q ) ){
       Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
@@ -673,7 +680,8 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   }
 }
 
-void InstStrategyCegqi::registerQuantifier( Node q ) {
+void InstStrategyCegqi::preRegisterQuantifier(Node q)
+{
   if( doCbqi( q ) ){
     // get the instantiator  
     if( options::cbqiPreRegInst() ){
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
index 5a4db0e53..3445c3f9f 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
@@ -103,8 +103,8 @@ class InstStrategyCbqi : public QuantifiersModule {
   void check(Theory::Effort e, QEffort quant_e) override;
   bool checkComplete() override;
   bool checkCompleteFor(Node q) override;
+  void checkOwnership(Node q) override;
   void preRegisterQuantifier(Node q) override;
-  void registerQuantifier(Node q) override;
   /** get next decision request */
   Node getNextDecisionRequest(unsigned& priority) override;
 };
@@ -147,8 +147,8 @@ class InstStrategyCegqi : public InstStrategyCbqi {
 
   //get instantiator for quantifier
   CegInstantiator * getInstantiator( Node q );
-  //register quantifier
-  void registerQuantifier(Node q) override;
+  /** pre-register quantifier */
+  void preRegisterQuantifier(Node q) override;
   //presolve
   void presolve() override;
 };
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 404f64471..807a7a58c 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -923,14 +923,6 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
   return addedLemmas;
 }
 
-void ConjectureGenerator::registerQuantifier( Node q ) {
-
-}
-
-void ConjectureGenerator::assertNode( Node n ) {
-
-}
-
 bool ConjectureGenerator::considerTermCanon( Node ln, bool genRelevant ){
   if( !ln.isNull() ){
     //do not consider if it is non-canonical, and either:
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 2db175fae..8a6339a85 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -428,9 +428,6 @@ public:
   void reset_round(Theory::Effort e) override;
   /* Call during quantifier engine's check */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /* Called for new quantifiers */
-  void registerQuantifier(Node q) override;
-  void assertNode(Node n) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const override { return "ConjectureGenerator"; }
   // options
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 184add8c3..bd95b316d 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -157,7 +157,8 @@ bool InstantiationEngine::checkCompleteFor( Node q ) {
   return false;
 }
 
-void InstantiationEngine::preRegisterQuantifier( Node q ) {
+void InstantiationEngine::checkOwnership(Node q)
+{
   if( options::strictTriggers() && q.getNumChildren()==3 ){
     //if strict triggers, take ownership of this quantified formula
     bool hasPat = false;
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 32ddb19ed..e4cb986da 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -81,7 +81,7 @@ class InstantiationEngine : public QuantifiersModule {
   void reset_round(Theory::Effort e) override;
   void check(Theory::Effort e, QEffort quant_e) override;
   bool checkCompleteFor(Node q) override;
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   void registerQuantifier(Node q) override;
   Node explain(TNode n) { return Node::null(); }
   /** add user pattern */
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index d96fb4e05..b493d6a0c 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -384,10 +384,11 @@ void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
   Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl; 
 }
 
-void BoundedIntegers::preRegisterQuantifier( Node f ) {
+void BoundedIntegers::checkOwnership(Node f)
+{
   //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
-  Trace("bound-int") << "preRegister quantifier " << f << std::endl;
-  
+  Trace("bound-int") << "check ownership quantifier " << f << std::endl;
+
   bool success;
   do{
     std::map< Node, unsigned > bound_lit_type_map;
@@ -546,10 +547,6 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
   }
 }
 
-void BoundedIntegers::registerQuantifier( Node q ) {
-
-}
-
 void BoundedIntegers::assertNode( Node n ) {
   Trace("bound-int-assert") << "Assert " << n << std::endl;
   Node nlit = n.getKind()==NOT ? n[0] : n;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 3e990067a..93b6436d5 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -146,8 +146,7 @@ public:
   void presolve() override;
   bool needsCheck(Theory::Effort e) override;
   void check(Theory::Effort e, QEffort quant_e) override;
-  void registerQuantifier(Node q) override;
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   void assertNode(Node n) override;
   Node getNextDecisionRequest(unsigned& priority) override;
   bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index e97f716cb..9e77a31c1 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -339,12 +339,14 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
   
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
   Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
+  d_preinitialized_eqc.clear();
   d_preinitialized_types.clear();
   //traverse equality engine
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
   while( !eqcs_i.isFinished() ){
-    TypeNode tr = (*eqcs_i).getType();
-    d_preinitialized_types[tr] = true;
+    Node r = *eqcs_i;
+    TypeNode tr = r.getType();
+    d_preinitialized_eqc[tr] = r;
     ++eqcs_i;
   }
 
@@ -352,8 +354,10 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
   fm->initialize();
   for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
     Node op = it->first;
+    Trace("fmc") << "preInitialize types for " << op << std::endl;
     TypeNode tno = op.getType();
     for( unsigned i=0; i<tno.getNumChildren(); i++) {
+      Trace("fmc") << "preInitializeType " << tno[i] << std::endl;
       preInitializeType( fm, tno[i] );
     }
   }
@@ -461,6 +465,8 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     for( size_t i=0; i<add_conds.size(); i++ ){
       Node c = add_conds[i];
       Node v = add_values[i];
+      Trace("fmc-model-debug")
+          << "Add cond/value : " << c << " -> " << v << std::endl;
       std::vector< Node > children;
       std::vector< Node > entry_children;
       children.push_back(op);
@@ -486,6 +492,8 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
       }
       Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
       Node nv = fm->getRepresentative( v );
+      Trace("fmc-model-debug")
+          << "Representative of " << v << " is " << nv << std::endl;
       if( !nv.isConst() ){
         Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
         Assert( false );
@@ -562,11 +570,26 @@ void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn )
     if (!tn.isFunction() || options::ufHo())
     {
       Node mb = fm->getModelBasisTerm(tn);
-      if (!mb.isConst())
+      // if the model basis term does not exist in the model,
+      // either add it directly to the model's equality engine if no other terms
+      // of this type exist, or otherwise assert that it is equal to the first
+      // equivalence class of its type.
+      if (!fm->hasTerm(mb) && !mb.isConst())
       {
-        Trace("fmc") << "...add model basis term to EE of model " << mb << " "
-                     << tn << std::endl;
-        fm->d_equalityEngine->addTerm(mb);
+        std::map<TypeNode, Node>::iterator itpe = d_preinitialized_eqc.find(tn);
+        if (itpe == d_preinitialized_eqc.end())
+        {
+          Trace("fmc") << "...add model basis term to EE of model " << mb << " "
+                       << tn << std::endl;
+          fm->d_equalityEngine->addTerm(mb);
+        }
+        else
+        {
+          Trace("fmc") << "...add model basis eqc equality to model " << mb
+                       << " == " << itpe->second << " " << tn << std::endl;
+          bool ret = fm->assertEquality(mb, itpe->second, true);
+          AlwaysAssert(ret);
+        }
       }
     }
   }
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index a64c33303..852f96e4c 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -93,8 +93,25 @@ protected:
   std::map< TypeNode, Node > d_array_cond;
   std::map< Node, Node > d_array_term_cond;
   std::map< Node, std::vector< int > > d_star_insts;
-  std::map< TypeNode, bool > d_preinitialized_types;
+  //--------------------for preinitialization
+  /** preInitializeType
+   *
+   * This function ensures that the model fm is properly initialized with
+   * respect to type tn.
+   *
+   * In particular, this class relies on the use of "model basis" terms, which
+   * are distinguished terms that are used to specify default values for
+   * uninterpreted functions. This method enforces that the model basis term
+   * occurs in the model for each relevant type T, where a type T is relevant
+   * if a bound variable is of type T, or an uninterpreted function has an
+   * argument or a return value of type T.
+   */
   void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn );
+  /** for each type, an equivalence class of that type from the model */
+  std::map<TypeNode, Node> d_preinitialized_eqc;
+  /** map from types to whether we have called the method above */
+  std::map<TypeNode, bool> d_preinitialized_types;
+  //--------------------end for preinitialization
   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
   bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
 protected:
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 54689b32a..743e7ccc8 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -295,7 +295,6 @@ bool InstStrategyEnum::process(Node f, bool fullEffort)
   return false;
 }
 
-void InstStrategyEnum::registerQuantifier(Node q) {}
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index cf97518fc..51c0c1d0c 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -72,8 +72,6 @@ class InstStrategyEnum : public QuantifiersModule
    * quantified formulas via calls to process(...)
    */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /** Register quantifier. */
-  void registerQuantifier(Node q) override;
   /** Identify. */
   std::string identify() const override
   {
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index 375754b26..c76d97255 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -32,7 +32,8 @@ QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){
 }
 
 /** add quantifier */
-void LtePartialInst::preRegisterQuantifier( Node q ) {
+void LtePartialInst::checkOwnership(Node q)
+{
   if( !q.getAttribute(LtePartialInstAttribute()) ){
     if( d_do_inst.find( q )!=d_do_inst.end() ){
       if( d_do_inst[q] ){
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 76a781e1c..2390eb40c 100644
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -56,7 +56,7 @@ private:
 public:
   LtePartialInst( QuantifiersEngine * qe, context::Context* c );
   /** determine whether this quantified formula will be reduced */
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   /** was invoked */
   bool wasInvoked() { return d_wasInvoked; }
   
@@ -64,11 +64,8 @@ public:
   bool needsCheck(Theory::Effort e) override;
   /* Call during quantifier engine's check */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /* Called for new quantifiers */
-  void registerQuantifier(Node q) override {}
   /* check complete */
   bool checkComplete() override { return !d_wasInvoked; }
-  void assertNode(Node n) override {}
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const override { return "LtePartialInst"; }
 };
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 9a6cc6e97..a90227577 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -23,9 +23,10 @@
 #include "proof/proof_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4;
@@ -218,41 +219,15 @@ Node QuantifierMacros::solveInEquality( Node n, Node lit ){
         return lit[i==0 ? 1 : 0].negate();
       }
     }
-    //must solve for term n in the literal lit
-    if( lit[0].getType().isInteger() || lit[0].getType().isReal() ){
-      Node coeff;
-      Node term;
-      //could be solved for on LHS
-      if( lit[0].getKind()==MULT && lit[0][1]==n ){
-        Assert( lit[0][0].isConst() );
-        term = lit[1];
-        coeff = lit[0][0];
-      }else{
-        Assert( lit[1].getKind()==PLUS );
-        std::vector< Node > plus_children;
-        //find monomial with n
-        for( size_t j=0; j<lit[1].getNumChildren(); j++ ){
-          if( lit[1][j]==n ){
-            Assert( coeff.isNull() );
-            coeff = NodeManager::currentNM()->mkConst( Rational(1) );
-          }else if( lit[1][j].getKind()==MULT && lit[1][j][1]==n ){
-            Assert( coeff.isNull() );
-            Assert( lit[1][j][0].isConst() );
-            coeff = lit[1][j][0];
-          }else{
-            plus_children.push_back( lit[1][j] );
-          }
-        }
-        if( !coeff.isNull() ){
-          term = plus_children.size()==1 ? plus_children[0] : NodeManager::currentNM()->mkNode( PLUS, plus_children );
-          term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term );
-        }
-      }
-      if( !coeff.isNull() ){
-        coeff = NodeManager::currentNM()->mkConst( Rational(1) / coeff.getConst<Rational>() );
-        term = NodeManager::currentNM()->mkNode( MULT, coeff, term );
-        term = Rewriter::rewrite( term );
-        return term;
+    std::map<Node, Node> msum;
+    if (ArithMSum::getMonomialSumLit(lit, msum))
+    {
+      Node veq_c;
+      Node val;
+      int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL);
+      if (res != 0 && veq_c.isNull())
+      {
+        return val;
       }
     }
   }
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 68a0f30dc..da6b0a6b4 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -31,8 +31,8 @@ QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){
 
 }
 
-/** pre register quantifier */
-void QuantDSplit::preRegisterQuantifier( Node q ) {
+void QuantDSplit::checkOwnership(Node q)
+{
   int max_index = -1;
   int max_score = -1;
   if( q.getNumChildren()==3 ){
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 1ea57433a..94bfa0f20 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -34,7 +34,7 @@ private:
 public:
   QuantDSplit( QuantifiersEngine * qe, context::Context* c );
   /** determine whether this quantified formula will be reduced */
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
 
   /* whether this module needs to check this round */
   bool needsCheck(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index f3fdfa6f4..874baa482 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -108,19 +108,27 @@ class QuantifiersModule {
    * we are incomplete for other reasons.
    */
   virtual bool checkCompleteFor( Node q ) { return false; }
-  /** Pre register quantifier.
+  /** Check ownership
    *
-   * Called once for new quantified formulas that are
-   * pre-registered by the quantifiers theory.
+   * Called once for new quantified formulas that are registered by the
+   * quantifiers theory. The primary purpose of this function is to establish
+   * if this module is the owner of quantified formula q.
    */
-  virtual void preRegisterQuantifier( Node q ) { }
+  virtual void checkOwnership(Node q) {}
   /** Register quantifier
    *
+   * Called once for new quantified formulas q that are pre-registered by the
+   * quantifiers theory, after internal ownership of quantified formulas is
+   * finalized. This does context-dependent initialization of this module.
+   */
+  virtual void registerQuantifier(Node q) {}
+  /** Pre-register quantifier
+   *
    * Called once for new quantified formulas that are
    * pre-registered by the quantifiers theory, after
    * internal ownership of quantified formulas is finalized.
    */
-  virtual void registerQuantifier( Node q ) = 0;
+  virtual void preRegisterQuantifier(Node q) {}
   /** Assert node.
    *
    * Called when a quantified formula q is asserted to the quantifiers theory
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index bb92cbaf7..c3dcdf6dc 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -926,56 +926,35 @@ Node QuantifiersRewriter::computeVariableElimLitBv(Node lit,
   Assert(lit.getKind() == EQUAL);
   // TODO (#1494) : linearize the literal using utility
 
-  // figure out if this literal is linear and invertible on path with args
-  std::map<TNode, bool> linear;
-  std::unordered_set<TNode, TNodeHashFunction> visited;
-  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(lit);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    if (std::find(args.begin(), args.end(), cur) != args.end())
-    {
-      bool lval = linear.find(cur) == linear.end();
-      linear[cur] = lval;
-    }
-    if (visited.find(cur) == visited.end())
-    {
-      visited.insert(cur);
-
-      for (const Node& cn : cur)
-      {
-        visit.push_back(cn);
-      }
-    }
-  } while (!visit.empty());
+  // compute a subset active_args of the bound variables args that occur in lit
+  std::vector<Node> active_args;
+  computeArgVec(args, active_args, lit);
 
   BvInverter binv;
-  for (std::pair<const TNode, bool>& lp : linear)
+  for (const Node& cvar : active_args)
   {
-    if (lp.second)
+    // solve for the variable on this path using the inverter
+    std::vector<unsigned> path;
+    Node slit = binv.getPathToPv(lit, cvar, path);
+    if (!slit.isNull())
     {
-      TNode cvar = lp.first;
-      Trace("quant-velim-bv") << "...linear wrt " << cvar << std::endl;
-      std::vector<unsigned> path;
-      Node slit = binv.getPathToPv(lit, cvar, path);
-      if (!slit.isNull())
+      Node slv = binv.solveBvLit(cvar, lit, path, nullptr);
+      Trace("quant-velim-bv") << "...solution : " << slv << std::endl;
+      if (!slv.isNull())
       {
-        Node slv = binv.solveBvLit(cvar, lit, path, nullptr);
-        Trace("quant-velim-bv") << "...solution : " << slv << std::endl;
-        if (!slv.isNull())
+        var = cvar;
+        // if this is a proper variable elimination, that is, var = slv where
+        // var is not in the free variables of slv, then we can return this
+        // as the variable elimination for lit.
+        if (isVariableElim(var, slv))
         {
-          var = cvar;
           return slv;
         }
       }
-      else
-      {
-        Trace("quant-velim-bv") << "...non-invertible path." << std::endl;
-      }
+    }
+    else
+    {
+      Trace("quant-velim-bv") << "...non-invertible path." << std::endl;
     }
   }
 
@@ -1130,10 +1109,11 @@ bool QuantifiersRewriter::computeVariableElimLit(
       std::vector<Node>::iterator ita =
           std::find(args.begin(), args.end(), var);
       Assert(ita != args.end());
-      Assert(isVariableElim(var, slv));
       Trace("var-elim-quant")
           << "Variable eliminate based on bit-vector inversion : " << var
           << " -> " << slv << std::endl;
+      Assert(!slv.hasSubterm(var));
+      Assert(slv.getType().isSubtypeOf(var.getType()));
       vars.push_back(var);
       subs.push_back(slv);
       args.erase(ita);
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5016bd87f..79b7d9a99 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -83,13 +83,23 @@ void TheoryQuantifiers::finishInit()
 }
 
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
+  if (n.getKind() != FORALL)
+  {
+    return;
+  }
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
-  if( n.getKind()==FORALL ){
-    if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
-      getQuantifiersEngine()->registerQuantifier( n );
-      Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
-    }
+  if (options::cbqi() && !options::recurseCbqi()
+      && TermUtil::hasInstConstAttr(n))
+  {
+    Debug("quantifiers-prereg")
+        << "TheoryQuantifiers::preRegisterTerm() done, unused " << n << endl;
+    return;
   }
+  // Preregister the quantified formula.
+  // This initializes the modules used for handling n in this user context.
+  getQuantifiersEngine()->preRegisterQuantifier(n);
+  Debug("quantifiers-prereg")
+      << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
 }
 
 
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 4f0302bf3..b82dccd73 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -65,9 +65,6 @@ class TheoryQuantifiers : public Theory {
   void assertUniversal( Node n );
   void assertExistential( Node n );
   void computeCareGraph() override;
-
-  using BoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
-
   /** number of instantiations */
   int d_numInstantiations;
   int d_baseDecLevel;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8e6aab06c..97e02f2c0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -76,6 +76,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_term_enum(new quantifiers::TermEnumeration),
       d_conflict_c(c, false),
       // d_quants(u),
+      d_quants_prereg(u),
       d_quants_red(u),
       d_lemmas_produced_c(u),
       d_ierCounter_c(c),
@@ -430,6 +431,31 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
     return;
   }
+  if (d_conflict_c.get())
+  {
+    if (e < Theory::EFFORT_LAST_CALL)
+    {
+      // this can happen in rare cases when quantifiers is the first to realize
+      // there is a quantifier-free conflict, for example, when it discovers
+      // disequal and congruent terms in the master equality engine during
+      // term indexing. In such cases, quantifiers reports a "conflicting lemma"
+      // that is, one that is entailed to be false by the current assignment.
+      // If this lemma is not a SAT conflict, we may get another call to full
+      // effort check and the quantifier-free solvers still haven't realized
+      // there is a conflict. In this case, we return, trusting that theory
+      // combination will do the right thing (split on equalities until there is
+      // a conflict at the quantifier-free level).
+      Trace("quant-engine-debug")
+          << "Conflicting lemma already reported by quantifiers, return."
+          << std::endl;
+      return;
+    }
+    // we reported what we thought was a conflicting lemma, but now we have
+    // gotten a check at LAST_CALL effort, indicating that the lemma we reported
+    // was not conflicting. This should never happen, but in production mode, we
+    // proceed with the check.
+    Assert(false);
+  }
   bool needsCheck = !d_lemmas_waiting.empty();
   QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
   std::vector< QuantifiersModule* > qm;
@@ -456,8 +482,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
   if( needsCheck ){
-    //this will fail if a set of instances is marked as a conflict, but is not
-    Assert( !d_conflict_c.get() );
     //flush previous lemmas (for instance, if was interupted), or other lemmas to process
     flushLemmas();
     if( d_hasAddedLemma ){
@@ -619,6 +643,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
                 setIncomplete = true;
               }
             }
+            if (d_conflict_c.get())
+            {
+              // we reported a conflicting lemma, should return
+              setIncomplete = true;
+            }
             //if we have a chance not to set incomplete
             if( !setIncomplete ){
               //check if we should set the incomplete flag
@@ -734,52 +763,77 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) {
   }
 }
 
-bool QuantifiersEngine::registerQuantifier( Node f ){
+void QuantifiersEngine::registerQuantifierInternal(Node f)
+{
   std::map< Node, bool >::iterator it = d_quants.find( f );
   if( it==d_quants.end() ){
     Trace("quant") << "QuantifiersEngine : Register quantifier ";
     Trace("quant") << " : " << f << std::endl;
+    unsigned prev_lemma_waiting = d_lemmas_waiting.size();
     ++(d_statistics.d_num_quant);
     Assert( f.getKind()==FORALL );
+    // register with utilities
+    for (unsigned i = 0; i < d_util.size(); i++)
+    {
+      d_util[i]->registerQuantifier(f);
+    }
+    // compute attributes
+    d_quant_attr->computeAttributes(f);
 
-    //check whether we should apply a reduction
-    if( reduceQuantifier( f ) ){
-      Trace("quant") << "...reduced." << std::endl;
-      d_quants[f] = false;
-      return false;
-    }else{
-      // register with utilities
-      for (unsigned i = 0; i < d_util.size(); i++)
-      {
-        d_util[i]->registerQuantifier(f);
-      }
-      // compute attributes
-      d_quant_attr->computeAttributes(f);
-
-      for( unsigned i=0; i<d_modules.size(); i++ ){
-        Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
-        d_modules[i]->preRegisterQuantifier( f );
-      }
-      QuantifiersModule * qm = getOwner( f );
-      if( qm!=NULL ){
-        Trace("quant") << "   Owner : " << qm->identify() << std::endl;
-      }
-      //register with each module
-      for( unsigned i=0; i<d_modules.size(); i++ ){
-        Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl;
-        d_modules[i]->registerQuantifier( f );
-      }
-      //TODO: remove this
-      Node ceBody = d_term_util->getInstConstantBody( f );
-      Trace("quant-debug")  << "...finish." << std::endl;
-      d_quants[f] = true;
-      // flush lemmas
-      flushLemmas();
-      return true;
+    for (QuantifiersModule*& mdl : d_modules)
+    {
+      Trace("quant-debug") << "check ownership with " << mdl->identify()
+                           << "..." << std::endl;
+      mdl->checkOwnership(f);
     }
-  }else{
-    return (*it).second;
+    QuantifiersModule* qm = getOwner(f);
+    Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
+                   << std::endl;
+    // register with each module
+    for (QuantifiersModule*& mdl : d_modules)
+    {
+      Trace("quant-debug") << "register with " << mdl->identify() << "..."
+                           << std::endl;
+      mdl->registerQuantifier(f);
+      // since this is context-independent, we should not add any lemmas during
+      // this call
+      Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
+    }
+    // TODO (#2020): remove this
+    Node ceBody = d_term_util->getInstConstantBody(f);
+    Trace("quant-debug") << "...finish." << std::endl;
+    d_quants[f] = true;
+    AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);
+  }
+}
+
+void QuantifiersEngine::preRegisterQuantifier(Node q)
+{
+  NodeSet::const_iterator it = d_quants_prereg.find(q);
+  if (it != d_quants_prereg.end())
+  {
+    return;
+  }
+  Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
+  d_quants_prereg.insert(q);
+  // try to reduce
+  if (reduceQuantifier(q))
+  {
+    // if we can reduce it, nothing left to do
+    return;
+  }
+  // ensure that it is registered
+  registerQuantifierInternal(q);
+  // register with each module
+  for (QuantifiersModule*& mdl : d_modules)
+  {
+    Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
+                         << std::endl;
+    mdl->preRegisterQuantifier(q);
   }
+  // flush the lemmas
+  flushLemmas();
+  Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
 }
 
 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
@@ -790,31 +844,35 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 }
 
 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
+  if (reduceQuantifier(f))
+  {
+    // if we can reduce it, nothing left to do
+    return;
+  }
   if( !pol ){
-    //if not reduced
-    if( !reduceQuantifier( f ) ){
-      //do skolemization
-      Node lem = d_skolemize->process(f);
-      if (!lem.isNull())
+    // do skolemization
+    Node lem = d_skolemize->process(f);
+    if (!lem.isNull())
+    {
+      if (Trace.isOn("quantifiers-sk-debug"))
       {
-        if( Trace.isOn("quantifiers-sk-debug") ){
-          Node slem = Rewriter::rewrite( lem );
-          Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl;
-        }
-        getOutputChannel().lemma( lem, false, true );
+        Node slem = Rewriter::rewrite(lem);
+        Trace("quantifiers-sk-debug")
+            << "Skolemize lemma : " << slem << std::endl;
       }
+      getOutputChannel().lemma(lem, false, true);
     }
-  }else{
-    //assert to modules TODO : also for !pol?
-    //register the quantifier, assert it to each module
-    if( registerQuantifier( f ) ){
-      d_model->assertQuantifier( f );
-      for( unsigned i=0; i<d_modules.size(); i++ ){
-        d_modules[i]->assertNode( f );
-      }
-      addTermToDatabase( d_term_util->getInstConstantBody( f ), true );
-    }
+    return;
+  }
+  // ensure the quantified formula is registered
+  registerQuantifierInternal(f);
+  // assert it to each module
+  d_model->assertQuantifier(f);
+  for (QuantifiersModule*& mdl : d_modules)
+  {
+    mdl->assertNode(f);
   }
+  addTermToDatabase(d_term_util->getInstConstantBody(f), true);
 }
 
 void QuantifiersEngine::propagate( Theory::Effort level ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 456a268da..70a4ede0c 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -173,6 +173,8 @@ private:
  private:
   /** list of all quantifiers seen */
   std::map< Node, bool > d_quants;
+  /** quantifiers pre-registered */
+  NodeSet d_quants_prereg;
   /** quantifiers reduced */
   BoolMap d_quants_red;
   std::map< Node, Node > d_quants_red_lem;
@@ -277,8 +279,12 @@ public:
   void check( Theory::Effort e );
   /** notify that theories were combined */
   void notifyCombineTheories();
-  /** register quantifier */
-  bool registerQuantifier( Node f );
+  /** preRegister quantifier
+   *
+   * This function is called after registerQuantifier for quantified formulas
+   * that are pre-registered to the quantifiers theory.
+   */
+  void preRegisterQuantifier(Node q);
   /** register quantifier */
   void registerPattern( std::vector<Node> & pattern);
   /** assert universal quantifier */
@@ -288,10 +294,19 @@ public:
   /** get next decision request */
   Node getNextDecisionRequest( unsigned& priority );
 private:
-  /** reduceQuantifier, return true if reduced */
-  bool reduceQuantifier( Node q );
-  /** flush lemmas */
-  void flushLemmas();
+ /** (context-indepentent) register quantifier internal
+  *
+  * This is called when a quantified formula q is pre-registered to the
+  * quantifiers theory, and updates the modules in this class with
+  * context-independent information about how to handle q. This includes basic
+  * information such as which module owns q.
+  */
+ void registerQuantifierInternal(Node q);
+ /** reduceQuantifier, return true if reduced */
+ bool reduceQuantifier(Node q);
+ /** flush lemmas */
+ void flushLemmas();
+
 public:
   /** add lemma lem */
   bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index f91a413e3..5024d17ac 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -666,7 +666,14 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
         if (assignable)
         {
           Assert(!evaluable || assignOne);
-          Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
+          // this assertion ensures that if we are assigning to a term of
+          // Boolean type, then the term is either a variable or an APPLY_UF.
+          // Note we only assign to terms of Boolean type if the term occurs in
+          // a singleton equivalence class; otherwise the term would have been
+          // in the equivalence class of true or false and would not need
+          // assigning.
+          Assert(!t.isBoolean() || (*i2).isVar()
+                 || (*i2).getKind() == kind::APPLY_UF);
           Node n;
           if (t.getCardinality().isInfinite())
           {
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 36f0d945e..2ac299177 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -160,6 +160,8 @@ REG0_TESTS = \
 	regress0/bv/bug440.smt \
 	regress0/bv/bug733.smt2 \
 	regress0/bv/bug734.smt2 \
+	regress0/bv/bv-abstr-bug.smt2 \
+	regress0/bv/bv-abstr-bug2.smt2 \
 	regress0/bv/bv-int-collapse1.smt2 \
 	regress0/bv/bv-int-collapse2.smt2 \
 	regress0/bv/bv-options1.smt2 \
@@ -432,6 +434,7 @@ REG0_TESTS = \
 	regress0/fmf/sc_bad_model_1221.smt2 \
 	regress0/fmf/syn002-si-real-int.smt2 \
 	regress0/fmf/tail_rec.smt2 \
+	regress0/fp/simple.smt2 \
 	regress0/fuzz_1.smt \
 	regress0/fuzz_3.smt \
 	regress0/get-value-incremental.smt2 \
@@ -599,7 +602,9 @@ REG0_TESTS = \
 	regress0/quantifiers/floor.smt2 \
 	regress0/quantifiers/is-even-pred.smt2 \
 	regress0/quantifiers/is-int.smt2 \
+	regress0/quantifiers/issue2031-bv-var-elim.smt2 \
 	regress0/quantifiers/issue1805.smt2 \
+	regress0/quantifiers/issue2033-macro-arith.smt2 \
 	regress0/quantifiers/lra-triv-gn.smt2 \
 	regress0/quantifiers/macros-int-real.smt2 \
 	regress0/quantifiers/macros-real-arg.smt2 \
@@ -1082,6 +1087,7 @@ REG1_TESTS = \
 	regress1/fmf/german169.smt2 \
 	regress1/fmf/german73.smt2 \
 	regress1/fmf/issue916-fmf-or.smt2 \
+	regress1/fmf/issue2034-preinit.smt2 \
 	regress1/fmf/jasmin-cdt-crash.smt2 \
 	regress1/fmf/ko-bound-set.cvc \
 	regress1/fmf/loopy_coda.smt2 \
@@ -1228,6 +1234,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 \
@@ -1252,6 +1259,7 @@ REG1_TESTS = \
 	regress1/quantifiers/ext-ex-deq-trigger.smt2 \
 	regress1/quantifiers/extract-nproc.smt2 \
 	regress1/quantifiers/florian-case-ax.smt2 \
+	regress1/quantifiers/fp-cegqi-unsat.smt2 \
 	regress1/quantifiers/gauss_init_0030.fof.smt2 \
 	regress1/quantifiers/horn-simple.smt2 \
 	regress1/quantifiers/inst-max-level-segf.smt2 \
@@ -1293,6 +1301,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 \
@@ -1584,7 +1593,6 @@ REG2_TESTS = \
 	regress2/ooo.tag10.smt2 \
 	regress2/piVC_5581bd.smt2 \
 	regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 \
-	regress2/quantifiers/ForElimination-scala-9.smt2 \
 	regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 \
 	regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 \
 	regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 \
@@ -1953,6 +1961,7 @@ DISABLED_TESTS = \
 	regress2/bug396.smt2 \
 	regress2/nl/dumortier-050317.smt2 \
 	regress2/nl/nt-lemmas-bad.smt2 \
+	regress2/quantifiers/ForElimination-scala-9.smt2 \
 	regress2/quantifiers/small-bug1-fixpoint-3.smt2 \
 	regress2/xs-11-20-5-2-5-3.smt \
 	regress2/xs-11-20-5-2-5-3.smt2
diff --git a/test/regress/README.md b/test/regress/README.md
index f6ff3c68b..d0c9b2b7a 100644
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -108,6 +108,19 @@ string `TERM` to make the regression test robust to the actual term printed
 (e.g. there could be multiple non-linear facts and it is ok if any of them is
 printed).
 
+Sometimes, certain benchmarks only apply to certain CVC4
+configurations. The `REQUIRES` directive can be used to only run
+a given benchmark when a feature is supported. For example:
+
+```
+; REQUIRES: symfpu
+```
+
+This benchmark is only run when symfpu has been configured.
+Multiple `REQUIRES` directives are supported. For a list of
+features that can be listed as a requirement, refer to CVC4's
+`--show-config` output.
+
 Sometimes it is useful to keep the directives separate. You can separate the
 benchmark from the output expectations by putting the benchmark in `<benchmark
 file>.smt` and the directives in `<benchmark file>.smt.expect`, which is looked
diff --git a/test/regress/regress0/bv/bv-abstr-bug.smt2 b/test/regress/regress0/bv/bv-abstr-bug.smt2
new file mode 100644
index 000000000..745996cb7
--- /dev/null
+++ b/test/regress/regress0/bv/bv-abstr-bug.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --bv-abstraction --bitblast=eager --no-check-models
+;
+; BV-abstraction should not be applied
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const c Bool)
+(declare-const d Bool)
+(assert
+ (or
+  (and a b)
+  (and c d)
+ )
+)
+(check-sat)
diff --git a/test/regress/regress0/bv/bv-abstr-bug2.smt2 b/test/regress/regress0/bv/bv-abstr-bug2.smt2
new file mode 100644
index 000000000..939439adf
--- /dev/null
+++ b/test/regress/regress0/bv/bv-abstr-bug2.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --solve-int-as-bv=32 --bitblast=eager
+(set-logic QF_NIA)
+(set-info :status sat)
+(declare-fun _substvar_7_ () Bool)
+(declare-fun _substvar_3_ () Int)
+(assert (or _substvar_7_ (= 0 _substvar_3_)))
+(check-sat)
diff --git a/test/regress/regress0/fp/simple.smt2 b/test/regress/regress0/fp/simple.smt2
new file mode 100644
index 000000000..0b4a11f08
--- /dev/null
+++ b/test/regress/regress0/fp/simple.smt2
@@ -0,0 +1,6 @@
+; REQUIRES: symfpu
+; EXPECT: unsat
+(set-logic QF_FP)    
+(declare-const x Float32)
+(assert (not (= x (fp.neg (fp.neg x)))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/issue2031-bv-var-elim.smt2 b/test/regress/regress0/quantifiers/issue2031-bv-var-elim.smt2
new file mode 100644
index 000000000..0585c5d67
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue2031-bv-var-elim.smt2
@@ -0,0 +1,4 @@
+(set-logic BV)
+(set-info :status unsat)
+(assert (exists ((?y2 (_ BitVec 32))) (exists ((?y3 (_ BitVec 32))) (forall ((?y5 (_ BitVec 32))) (forall ((?y6 (_ BitVec 32))) (not (= (bvadd (bvadd (bvadd (bvadd (bvmul (bvneg (_ bv65 32)) ?y6) (bvmul (bvneg (_ bv93 32)) ?y5)) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)) (_ bv69 32))))))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
new file mode 100644
index 000000000..7993910fd
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: sat
+(set-logic AUFNIRA)
+(set-info :status sat)
+(declare-fun _substvar_4_ () Real)
+(declare-sort S2 0)
+(declare-sort S10 0)
+(declare-fun f22 (S10 S2) Real)
+(assert (forall ((?v0 S10) (?v1 S2)) (= _substvar_4_ (- (f22 ?v0 ?v1)))))
+(check-sat)
diff --git a/test/regress/regress1/fmf/issue2034-preinit.smt2 b/test/regress/regress1/fmf/issue2034-preinit.smt2
new file mode 100644
index 000000000..e80e698fd
--- /dev/null
+++ b/test/regress/regress1/fmf/issue2034-preinit.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unknown
+(set-logic AUFLIRA)
+(set-info :status unknown)
+(declare-fun _substvar_1_ () Int)
+(declare-fun tptp_const_array1 (Int Real) (Array Int Real))
+(assert (forall ((?I_4 Int) (?L_5 Int) (?U_6 Int) (?Val_7 Real)) (=> true (= (select (tptp_const_array1 _substvar_1_ ?Val_7) 0) ?Val_7))))
+(check-sat)
\ No newline at end of file
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/fp-cegqi-unsat.smt2 b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2
new file mode 100644
index 000000000..1ee8e6c11
--- /dev/null
+++ b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2
@@ -0,0 +1,10 @@
+; REQUIRES: symfpu
+(set-info :smt-lib-version 2.6)
+(set-logic FP)
+(set-info :status unsat)
+(declare-fun c_main_~E0~7 () (_ FloatingPoint 11 53))
+(declare-fun c_main_~S~7 () (_ FloatingPoint 11 53))
+(assert (and (= ((_ to_fp 11 53) RNE (_ bv0 32)) c_main_~S~7) (fp.geq c_main_~E0~7 (fp.neg ((_ to_fp 11 53) RNE 1.0))) (fp.leq c_main_~E0~7 ((_ to_fp 11 53) RNE 1.0))))
+(assert (not (and (exists ((main_~E0~7 (_ FloatingPoint 11 53)) (main_~E1~7 (_ FloatingPoint 11 53))) (and (fp.geq main_~E1~7 (fp.neg ((_ to_fp 11 53) RNE 1.0))) (= c_main_~S~7 (fp.sub RNE (fp.add RNE (fp.mul RNE ((_ to_fp 11 53) RNE 0.999) ((_ to_fp 11 53) RNE (_ bv0 32))) main_~E0~7) main_~E1~7)) (fp.geq main_~E0~7 (fp.neg ((_ to_fp 11 53) RNE 1.0))) (fp.leq main_~E0~7 ((_ to_fp 11 53) RNE 1.0)) (fp.leq main_~E1~7 ((_ to_fp 11 53) RNE 1.0)))) (fp.geq c_main_~E0~7 (fp.neg ((_ to_fp 11 53) RNE 1.0))) (fp.leq c_main_~E0~7 ((_ to_fp 11 53) RNE 1.0)))))
+(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)
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 7226e7453..9bd3de9f0 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -23,6 +23,7 @@ EXPECT = 'EXPECT: '
 EXPECT_ERROR = 'EXPECT-ERROR: '
 EXIT = 'EXIT: '
 COMMAND_LINE = 'COMMAND-LINE: '
+REQUIRES = 'REQUIRES: '
 
 
 def run_process(args, cwd, timeout, s_input=None):
@@ -42,17 +43,37 @@ def run_process(args, cwd, timeout, s_input=None):
     out = ''
     err = ''
     exit_status = 124
-    timer = threading.Timer(timeout, lambda p: p.kill(), [proc])
     try:
-        timer.start()
+        if timeout:
+            timer = threading.Timer(timeout, lambda p: p.kill(), [proc])
+            timer.start()
         out, err = proc.communicate(input=s_input)
         exit_status = proc.returncode
     finally:
-        timer.cancel()
+        if timeout:
+            timer.cancel()
 
     return out, err, exit_status
 
 
+def get_cvc4_features(cvc4_binary):
+    """Returns a list of features supported by the CVC4 binary `cvc4_binary`."""
+
+    output, _, _ = run_process([cvc4_binary, '--show-config'], None, None)
+    if isinstance(output, bytes):
+        output = output.decode()
+
+    features = []
+    for line in output.split('\n'):
+        tokens = [t.strip() for t in line.split(':')]
+        if len(tokens) == 2:
+            key, value = tokens
+            if value == 'yes':
+                features.append(key)
+
+    return features
+
+
 def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc4_binary,
                   command_line, benchmark_dir, benchmark_filename, timeout):
     """Runs CVC4 on the file `benchmark_filename` in the directory
@@ -113,6 +134,8 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
     if not os.path.isfile(benchmark_path):
         sys.exit('"{}" does not exist or is not a file'.format(benchmark_path))
 
+    cvc4_features = get_cvc4_features(cvc4_binary)
+
     basic_command_line_args = []
 
     benchmark_basename = os.path.basename(benchmark_path)
@@ -167,6 +190,7 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
     expected_error = ''
     expected_exit_status = None
     command_lines = []
+    requires = []
     for line in metadata_lines:
         # Skip lines that do not start with a comment character.
         if line[0] != comment_char:
@@ -185,6 +209,8 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
             expected_exit_status = int(line[len(EXIT):])
         elif line.startswith(COMMAND_LINE):
             command_lines.append(line[len(COMMAND_LINE):])
+        elif line.startswith(REQUIRES):
+            requires.append(line[len(REQUIRES):].strip())
     expected_output = expected_output.strip()
     expected_error = expected_error.strip()
 
@@ -217,6 +243,12 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
         )
         return
 
+    for req_feature in requires:
+        if req_feature not in cvc4_features:
+            print('1..0 # Skipped regression: {} not supported'.format(
+                req_feature))
+            return
+
     if not command_lines:
         command_lines.append('')
 
@@ -251,8 +283,8 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
                    not cvc4_binary.endswith('pcvc4'):
                     extra_command_line_args += ['--check-unsat-cores']
             if extra_command_line_args:
-                command_line_args_configs.append(
-                    all_args + extra_command_line_args)
+                command_line_args_configs.append(all_args +
+                                                 extra_command_line_args)
 
     # Run CVC4 on the benchmark with the different option sets and check
     # whether the exit status, stdout output, stderr output are as expected.