Merge branch 'master' into fixSetInfoNamefixSetInfoName

24 files changed, 454 insertions, 439 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 40aa1a5af..6a21566e0 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -77,6 +77,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/bv_intro_pow2.h \
 	preprocessing/passes/extended_rewriter_pass.cpp \
 	preprocessing/passes/extended_rewriter_pass.h \
+	preprocessing/passes/global_negate.cpp \
+	preprocessing/passes/global_negate.h \
 	preprocessing/passes/int_to_bv.cpp \
 	preprocessing/passes/int_to_bv.h \
 	preprocessing/passes/ite_removal.cpp \
@@ -462,8 +464,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/fmf/model_engine.h \
 	theory/quantifiers/fun_def_process.cpp \
 	theory/quantifiers/fun_def_process.h \
-	theory/quantifiers/global_negate.cpp \
-	theory/quantifiers/global_negate.h \
 	theory/quantifiers/instantiate.cpp \
 	theory/quantifiers/instantiate.h \
 	theory/quantifiers/inst_match.cpp \
diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index 73a2be9ff..e0c34127a 100644
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -77,15 +77,6 @@ header = "options/uf_options.h"
   help       = "mode of operation for uf strong solver."
 
 [[option]]
-  name       = "ufssCliqueSplits"
-  category   = "regular"
-  long       = "uf-ss-clique-splits"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "use cliques instead of splitting on demand to shrink model"
-
-[[option]]
   name       = "ufssFairness"
   category   = "regular"
   long       = "uf-ss-fair"
diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp
index 12c1c5c21..26785f15b 100644
--- a/src/preprocessing/passes/bv_ackermann.cpp
+++ b/src/preprocessing/passes/bv_ackermann.cpp
@@ -23,12 +23,9 @@
 
 #include "preprocessing/passes/bv_ackermann.h"
 
-#include "expr/node.h"
 #include "options/bv_options.h"
 #include "theory/bv/theory_bv_utils.h"
 
-#include <unordered_set>
-
 using namespace CVC4;
 using namespace CVC4::theory;
 
@@ -41,55 +38,142 @@ namespace passes {
 namespace
 {
 
-void storeFunction(
-    TNode func,
-    TNode term,
-    FunctionToArgsMap& fun_to_args,
-    SubstitutionMap& fun_to_skolem)
+void addLemmaForPair(TNode args1,
+                     TNode args2,
+                     const TNode func,
+                     AssertionPipeline* assertionsToPreprocess,
+                     NodeManager* nm)
 {
-  if (fun_to_args.find(func) == fun_to_args.end())
+  Node args_eq;
+
+  if (args1.getKind() == kind::APPLY_UF)
   {
-    fun_to_args.insert(make_pair(func, NodeSet()));
+    Assert(args1.getOperator() == func);
+    Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func);
+    Assert(args1.getNumChildren() == args2.getNumChildren());
+
+    std::vector<Node> eqs(args1.getNumChildren());
+
+    for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
+    {
+      eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
+    }
+    args_eq = bv::utils::mkAnd(eqs);
   }
-  NodeSet& set = fun_to_args[func];
-  if (set.find(term) == set.end())
+  else
   {
-    set.insert(term);
-    TypeNode tn = term.getType();
-    Node skolem = NodeManager::currentNM()->mkSkolem(
-        "BVSKOLEM$$",
-        tn,
-        "is a variable created by the ackermannization "
-        "preprocessing pass for theory BV");
-    fun_to_skolem.addSubstitution(term, skolem);
+    Assert(args1.getKind() == kind::SELECT && args1[0] == func);
+    Assert(args2.getKind() == kind::SELECT && args2[0] == func);
+    Assert(args1.getNumChildren() == 2);
+    Assert(args2.getNumChildren() == 2);
+    args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]);
   }
+  Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
+  Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
+  assertionsToPreprocess->push_back(lemma);
 }
 
-void collectFunctionSymbols(
-    TNode term,
-    FunctionToArgsMap& fun_to_args,
-    SubstitutionMap& fun_to_skolem,
-    std::unordered_set<TNode, TNodeHashFunction>& seen)
+void storeFunctionAndAddLemmas(TNode func,
+                               TNode term,
+                               FunctionToArgsMap& fun_to_args,
+                               SubstitutionMap& fun_to_skolem,
+                               AssertionPipeline* assertions,
+                               NodeManager* nm,
+                               std::vector<TNode>* vec)
 {
-  if (seen.find(term) != seen.end()) return;
-  if (term.getKind() == kind::APPLY_UF)
-  {
-    storeFunction(term.getOperator(), term, fun_to_args, fun_to_skolem);
-  }
-  else if (term.getKind() == kind::SELECT)
+  if (fun_to_args.find(func) == fun_to_args.end())
   {
-    storeFunction(term[0], term, fun_to_args, fun_to_skolem);
+    fun_to_args.insert(make_pair(func, TNodeSet()));
   }
-  else
+  TNodeSet& set = fun_to_args[func];
+  if (set.find(term) == set.end())
   {
-    AlwaysAssert(term.getKind() != kind::STORE,
-                 "Cannot use eager bitblasting on QF_ABV formula with stores");
+    TypeNode tn = term.getType();
+    Node skolem = nm->mkSkolem("BVSKOLEM$$",
+                               tn,
+                               "is a variable created by the ackermannization "
+                               "preprocessing pass for theory BV");
+    for (const auto& t : set)
+    {
+      addLemmaForPair(t, term, func, assertions, nm);
+    }
+    fun_to_skolem.addSubstitution(term, skolem);
+    set.insert(term);
+    /* Add the arguments of term (newest element in set) to the vector, so that
+     * collectFunctionsAndLemmas will process them as well.
+     * This is only needed if the set has at least two elements
+     * (otherwise, no lemma is generated).
+     * Therefore, we defer this for term in case it is the first element in the
+     * set*/
+    if (set.size() == 2)
+    {
+      for (TNode elem : set)
+      {
+        vec->insert(vec->end(), elem.begin(), elem.end());
+      }
+    }
+    else if (set.size() > 2)
+    {
+      vec->insert(vec->end(), term.begin(), term.end());
+    }
   }
-  for (const TNode& n : term)
+}
+
+/* We only add top-level applications of functions.
+ * For example: when we see "f(g(x))", we do not add g as a function and x as a
+ * parameter.
+ * Instead, we only include f as a function and g(x) as a parameter.
+ * However, if we see g(x) later on as a top-level application, we will add it
+ * as well.
+ * Another example: for the formula f(g(x))=f(g(y)),
+ * we first only add f as a function and g(x),g(y) as arguments.
+ * storeFunctionAndAddLemmas will then add the constraint g(x)=g(y) ->
+ * f(g(x))=f(g(y)).
+ * Now that we see g(x) and g(y), we explicitly add them as well. */
+void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
+                               SubstitutionMap& fun_to_skolem,
+                               std::vector<TNode>* vec,
+                               AssertionPipeline* assertions)
+{
+  TNodeSet seen;
+  NodeManager* nm = NodeManager::currentNM();
+  TNode term;
+  while (!vec->empty())
   {
-    collectFunctionSymbols(n, fun_to_args, fun_to_skolem, seen);
+    term = vec->back();
+    vec->pop_back();
+    if (seen.find(term) == seen.end())
+    {
+      TNode func;
+      if (term.getKind() == kind::APPLY_UF)
+      {
+        storeFunctionAndAddLemmas(term.getOperator(),
+                                  term,
+                                  fun_to_args,
+                                  fun_to_skolem,
+                                  assertions,
+                                  nm,
+                                  vec);
+      }
+      else if (term.getKind() == kind::SELECT)
+      {
+        storeFunctionAndAddLemmas(
+            term[0], term, fun_to_args, fun_to_skolem, assertions, nm, vec);
+      }
+      else
+      {
+        AlwaysAssert(
+            term.getKind() != kind::STORE,
+            "Cannot use eager bitblasting on QF_ABV formula with stores");
+        /* add children to the vector, so that they are processed later */
+        for (TNode n : term)
+        {
+          vec->push_back(n);
+        }
+      }
+      seen.insert(term);
+    }
   }
-  seen.insert(term);
 }
 
 }  // namespace
@@ -108,57 +192,15 @@ PreprocessingPassResult BVAckermann::applyInternal(
   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
   AlwaysAssert(!options::incrementalSolving());
 
-  std::unordered_set<TNode, TNodeHashFunction> seen;
-
+  /* collect all function applications and generate consistency lemmas
+   * accordingly */
+  std::vector<TNode> to_process;
   for (const Node& a : assertionsToPreprocess->ref())
   {
-    collectFunctionSymbols(a, d_funcToArgs, d_funcToSkolem, seen);
-  }
-
-  NodeManager* nm = NodeManager::currentNM();
-  for (const auto& p : d_funcToArgs)
-  {
-    TNode func = p.first;
-    const NodeSet& args = p.second;
-    NodeSet::const_iterator it1 = args.begin();
-    for (; it1 != args.end(); ++it1)
-    {
-      for (NodeSet::const_iterator it2 = it1; it2 != args.end(); ++it2)
-      {
-        TNode args1 = *it1;
-        TNode args2 = *it2;
-        Node args_eq;
-
-        if (args1.getKind() == kind::APPLY_UF)
-        {
-          AlwaysAssert(args1.getKind() == kind::APPLY_UF
-                       && args1.getOperator() == func);
-          AlwaysAssert(args2.getKind() == kind::APPLY_UF
-                       && args2.getOperator() == func);
-          AlwaysAssert(args1.getNumChildren() == args2.getNumChildren());
-
-          std::vector<Node> eqs(args1.getNumChildren());
-
-          for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
-          {
-            eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
-          }
-          args_eq = bv::utils::mkAnd(eqs);
-        }
-        else
-        {
-          AlwaysAssert(args1.getKind() == kind::SELECT && args1[0] == func);
-          AlwaysAssert(args2.getKind() == kind::SELECT && args2[0] == func);
-          AlwaysAssert(args1.getNumChildren() == 2);
-          AlwaysAssert(args2.getNumChildren() == 2);
-          args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]);
-        }
-        Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
-        Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
-        assertionsToPreprocess->push_back(lemma);
-      }
-    }
+    to_process.push_back(a);
   }
+  collectFunctionsAndLemmas(
+      d_funcToArgs, d_funcToSkolem, &to_process, assertionsToPreprocess);
 
   /* replace applications of UF by skolems */
   // FIXME for model building, github issue #1901
diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h
index 197e92178..5f799ffe4 100644
--- a/src/preprocessing/passes/bv_ackermann.h
+++ b/src/preprocessing/passes/bv_ackermann.h
@@ -26,16 +26,18 @@
 #ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
 #define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
 
+#include <unordered_map>
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 
-#include <unordered_map>
-
 namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
-typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgsMap;
+using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
+using FunctionToArgsMap =
+    std::unordered_map<TNode, TNodeSet, TNodeHashFunction>;
 
 class BVAckermann : public PreprocessingPass
 {
diff --git a/src/theory/quantifiers/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 0670b5c5b..ddebf961f 100644
--- a/src/theory/quantifiers/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -12,21 +12,22 @@
  ** \brief Implementation of global_negate
  **/
 
-#include "theory/quantifiers/global_negate.h"
+#include "preprocessing/passes/global_negate.h"
+#include <vector>
+#include "expr/node.h"
 #include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
+using namespace CVC4::theory;
 
 namespace CVC4 {
-namespace theory {
-namespace quantifiers {
+namespace preprocessing {
+namespace passes {
 
-void GlobalNegate::simplify(std::vector<Node>& assertions)
+Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm)
 {
-  NodeManager* nm = NodeManager::currentNM();
   Assert(!assertions.empty());
-
   Trace("cbqi-gn") << "Global negate : " << std::endl;
   // collect free variables in all assertions
   std::vector<Node> free_vars;
@@ -90,21 +91,26 @@ void GlobalNegate::simplify(std::vector<Node>& assertions)
   Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
   body = Rewriter::rewrite(body);
   Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl;
+  return body;
+}
 
-  Node truen = nm->mkConst(true);
-  for (unsigned i = 0, size = assertions.size(); i < size; i++)
+GlobalNegate::GlobalNegate(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "global-negate"){};
+
+PreprocessingPassResult GlobalNegate::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node simplifiedNode = simplify(assertionsToPreprocess->ref(), nm);
+  Node trueNode = nm->mkConst(true);
+  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {
-    if (i == 0)
-    {
-      assertions[i] = body;
-    }
-    else
-    {
-      assertions[i] = truen;
-    }
+    assertionsToPreprocess->replace(i, trueNode);
   }
+  assertionsToPreprocess->push_back(simplifiedNode);
+  return PreprocessingPassResult::NO_CONFLICT;
 }
 
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
new file mode 100644
index 000000000..0330aa10e
--- /dev/null
+++ b/src/preprocessing/passes/global_negate.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file global_negate.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief the global_negate preprocessing pass
+  * Updates a set of assertions to the negation of
+ * these assertions. In detail, if assertions is:
+ *    F1, ..., Fn
+ * then we update this vector to:
+ *    forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true
+ * where x1...xm are the free variables of F1...Fn.
+ * When this is done, d_globalNegation flag is marked, so that the solver checks
+ *for unsat instead of sat.
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+#define __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class GlobalNegate : public PreprocessingPass
+{
+ public:
+  GlobalNegate(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  Node simplify(std::vector<Node>& assertions, NodeManager* nm);
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f1a59a580..5e7d52676 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -79,6 +79,7 @@
 #include "preprocessing/passes/bv_intro_pow2.h"
 #include "preprocessing/passes/bv_to_bool.h"
 #include "preprocessing/passes/extended_rewriter_pass.h"
+#include "preprocessing/passes/global_negate.h"
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/ite_removal.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
@@ -115,7 +116,6 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/logic_info.h"
 #include "theory/quantifiers/fun_def_process.h"
-#include "theory/quantifiers/global_negate.h"
 #include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/single_inv_partition.h"
@@ -2659,6 +2659,8 @@ void SmtEnginePrivate::finishInit()
       new BVToBool(d_preprocessingPassContext.get()));
   std::unique_ptr<ExtRewPre> extRewPre(
       new ExtRewPre(d_preprocessingPassContext.get()));
+  std::unique_ptr<GlobalNegate> globalNegate(
+      new GlobalNegate(d_preprocessingPassContext.get()));
   std::unique_ptr<IntToBV> intToBV(
       new IntToBV(d_preprocessingPassContext.get()));
   std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
@@ -2700,6 +2702,8 @@ void SmtEnginePrivate::finishInit()
                                            std::move(bvIntroPow2));
   d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool));
   d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre));
+  d_preprocessingPassRegistry.registerPass("global-negate",
+                                           std::move(globalNegate));
   d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
   d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
                                            std::move(quantifiersPreprocess));
@@ -4084,8 +4088,7 @@ void SmtEnginePrivate::processAssertions() {
   if (options::globalNegate())
   {
     // global negation of the formula
-    quantifiers::GlobalNegate gn;
-    gn.simplify(d_assertions.ref());
+    d_preprocessingPassRegistry.getPass("global-negate")->apply(&d_assertions);
     d_smt.d_globalNegation = !d_smt.d_globalNegation;
   }
 
diff --git a/src/theory/quantifiers/global_negate.h b/src/theory/quantifiers/global_negate.h
deleted file mode 100644
index f5d92c478..000000000
--- a/src/theory/quantifiers/global_negate.h
+++ /dev/null
@@ -1,53 +0,0 @@
-/*********************                                                        */
-/*! \file global_negate.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief global_negate
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H
-#define __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H
-
-#include <vector>
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-/** GlobalNegate
- *
- * This class updates a set of assertions to be equivalent to the negation of
- * these assertions. In detail, if assertions is:
- *    F1, ..., Fn
- * then we update this vector to:
- *    forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true
- * where x1...xm are the free variables of F1...Fn.
- */
-class GlobalNegate
-{
- public:
-  GlobalNegate() {}
-  ~GlobalNegate() {}
-  /** simplify assertions
-   *
-   * Replaces assertions with a set of assertions that is equivalent to its
-   * negation.
-   */
-  void simplify(std::vector<Node>& assertions);
-};
-
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H */
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 091c3b673..a16e03420 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -101,10 +101,6 @@ void InstMatch::clear() {
 }
 
 Node InstMatch::get(int i) const { return d_vals[i]; }
-void InstMatch::getInst(std::vector<Node>& inst) const
-{
-  inst.insert(inst.end(), d_vals.begin(), d_vals.end());
-}
 
 void InstMatch::setValue( int i, TNode n ) {
   d_vals[i] = n;
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 86138feb3..5695d1294 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -80,8 +80,6 @@ public:
   }
   /** get the i^th term in the instantiation */
   Node get(int i) const;
-  /** append the terms of this instantiation to inst */
-  void getInst(std::vector<Node>& inst) const;
   /** set/overwrites the i^th field in the instantiation with n */
   void setValue( int i, TNode n );
   /** set the i^th term in the instantiation to n
diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp
index b9e4d0650..a05388d17 100644
--- a/src/theory/quantifiers/quant_relevance.cpp
+++ b/src/theory/quantifiers/quant_relevance.cpp
@@ -28,21 +28,6 @@ void QuantRelevance::registerQuantifier(Node f)
   std::vector<Node> syms;
   computeSymbols(f[1], syms);
   d_syms[f].insert(d_syms[f].begin(), syms.begin(), syms.end());
-  // set initial relevance
-  int minRelevance = -1;
-  for (int i = 0; i < (int)syms.size(); i++)
-  {
-    d_syms_quants[syms[i]].push_back(f);
-    int r = getRelevance(syms[i]);
-    if (r != -1 && (minRelevance == -1 || r < minRelevance))
-    {
-      minRelevance = r;
-    }
-  }
-  if (minRelevance != -1)
-  {
-    setRelevance(f, minRelevance + 1);
-  }
 }
 
 /** compute symbols */
@@ -65,33 +50,6 @@ void QuantRelevance::computeSymbols(Node n, std::vector<Node>& syms)
   }
 }
 
-/** set relevance */
-void QuantRelevance::setRelevance(Node s, int r)
-{
-  if (d_computeRel)
-  {
-    int rOld = getRelevance(s);
-    if (rOld == -1 || r < rOld)
-    {
-      d_relevance[s] = r;
-      if (s.getKind() == FORALL)
-      {
-        for (int i = 0; i < (int)d_syms[s].size(); i++)
-        {
-          setRelevance(d_syms[s][i], r);
-        }
-      }
-      else
-      {
-        for (int i = 0; i < (int)d_syms_quants[s].size(); i++)
-        {
-          setRelevance(d_syms_quants[s][i], r + 1);
-        }
-      }
-    }
-  }
-}
-
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h
index 75ae32318..21017e783 100644
--- a/src/theory/quantifiers/quant_relevance.h
+++ b/src/theory/quantifiers/quant_relevance.h
@@ -39,7 +39,7 @@ class QuantRelevance : public QuantifiersUtil
    * if this is false, then all calls to getRelevance
    * return -1.
    */
-  QuantRelevance(bool cr) : d_computeRel(cr) {}
+  QuantRelevance() {}
   ~QuantRelevance() {}
   /** reset */
   bool reset(Theory::Effort e) override { return true; }
@@ -47,13 +47,6 @@ class QuantRelevance : public QuantifiersUtil
   void registerQuantifier(Node q) override;
   /** identify */
   std::string identify() const override { return "QuantRelevance"; }
-  /** set relevance of symbol s to r */
-  void setRelevance(Node s, int r);
-  /** get relevance of symbol s */
-  int getRelevance(Node s)
-  {
-    return d_relevance.find(s) == d_relevance.end() ? -1 : d_relevance[s];
-  }
   /** get number of quantifiers for symbol s */
   unsigned getNumQuantifiersForSymbol(Node s)
   {
@@ -61,8 +54,6 @@ class QuantRelevance : public QuantifiersUtil
   }
 
  private:
-  /** for computing relevance */
-  bool d_computeRel;
   /** map from quantifiers to symbols they contain */
   std::map<Node, std::vector<Node> > d_syms;
   /** map from symbols to quantifiers */
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index d0f156811..d1217d01d 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -42,27 +42,6 @@ void SygusUnif::initializeCandidate(
   d_strategy[f].initialize(qe, f, enums);
 }
 
-bool SygusUnif::constructSolution(std::vector<Node>& sols,
-                                  std::vector<Node>& lemmas)
-{
-  // initialize a call to construct solution
-  initializeConstructSol();
-  for (const Node& f : d_candidates)
-  {
-    // initialize a call to construct solution for function f
-    initializeConstructSolFor(f);
-    // call the virtual construct solution method
-    Node e = d_strategy[f].getRootEnumerator();
-    Node sol = constructSol(f, e, role_equal, 1, lemmas);
-    if (sol.isNull())
-    {
-      return false;
-    }
-    sols.push_back(sol);
-  }
-  return true;
-}
-
 Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved)
 {
   Assert(!solved.empty());
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index dd6922351..614a29d1c 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -85,7 +85,7 @@ class SygusUnif
    * channel by the caller.
    */
   virtual bool constructSolution(std::vector<Node>& sols,
-                                 std::vector<Node>& lemmas);
+                                 std::vector<Node>& lemmas) = 0;
 
  protected:
   /** reference to quantifier engine */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8c43e98ff..a5cd95d29 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -135,7 +135,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
   if( options::relevantTriggers() ){
-    d_quant_rel = new quantifiers::QuantRelevance(false);
+    d_quant_rel = new quantifiers::QuantRelevance;
     d_util.push_back(d_quant_rel);
   }else{
     d_quant_rel = NULL;
@@ -563,9 +563,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
 
     if( e==Theory::EFFORT_LAST_CALL ){
-      //if effort is last call, try to minimize model first
-      //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
-      //if( ufss && !ufss->minimize() ){ return; }
       ++(d_statistics.d_instantiation_rounds_lc);
     }else if( e==Theory::EFFORT_FULL ){
       ++(d_statistics.d_instantiation_rounds);
@@ -908,18 +905,6 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
       {
         d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
       }
-
-      // added contains also the Node that just have been asserted in this
-      // branch
-      if (d_quant_rel)
-      {
-        for (std::set<Node>::iterator i = added.begin(), end = added.end();
-             i != end;
-             i++)
-        {
-          d_quant_rel->setRelevance( i->getOperator(), 0 );
-        }
-      }
     }
   }
 }
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 65f7238c9..4efa6c2ce 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -23,7 +23,6 @@
 #include "theory/theory_model.h"
 
 //#define ONE_SPLIT_REGION
-//#define DISABLE_QUICK_CLIQUE_CHECKS
 //#define COMBINE_REGIONS_SMALL_INTO_LARGE
 //#define LAZY_REL_EQC
 
@@ -379,21 +378,6 @@ bool Region::check( Theory::Effort level, int cardinality,
   return false;
 }
 
-bool Region::getCandidateClique( int cardinality, std::vector< Node >& clique )
-{
-  if( d_testCliqueSize>=unsigned(cardinality+1) ){
-    //test clique is a clique
-    for( NodeBoolMap::iterator it = d_testClique.begin();
-         it != d_testClique.end(); ++it ){
-      if( (*it).second ){
-        clique.push_back( (*it).first );
-      }
-    }
-    return true;
-  }
-  return false;
-}
-
 void Region::getNumExternalDisequalities(
     std::map< Node, int >& num_ext_disequalities ){
   for( Region::iterator it = begin(); it != end(); ++it ){
@@ -713,25 +697,16 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
           //see if we have any recommended splits from large regions
           for( int i=0; i<(int)d_regions_index; i++ ){
             if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){
-              //just add the clique lemma
-              if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){
-                std::vector< Node > clique;
-                if( d_regions[i]->getCandidateClique( d_cardinality, clique ) ){
-                  //add clique lemma
-                  addCliqueLemma( clique, out );
-                  return;
-                }
-              }else{
-                int sp = addSplit( d_regions[i], out );
-                if( sp==1 ){
-                  addedLemma = true;
+
+              int sp = addSplit( d_regions[i], out );
+              if( sp==1 ){
+                addedLemma = true;
 #ifdef ONE_SPLIT_REGION
-                  break;
+                break;
 #endif
-                }else if( sp==-1 ){
-                  check( level, out );
-                  return;
-                }
+              }else if( sp==-1 ){
+                check( level, out );
+                return;
               }
             }
           }
@@ -815,67 +790,6 @@ Node SortModel::getNextDecisionRequest(){
   return Node::null();
 }
 
-bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){
-  if( options::ufssTotality() ){
-    //do nothing
-  }else{
-    if( m ){
-#if 0
-      // ensure that the constructed model is minimal
-      // if the model has terms that the strong solver does not know about
-      if( (int)rs->d_type_reps[ d_type ].size()>d_cardinality ){
-        eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->getEqualityEngine() );
-        while( !eqcs_i.isFinished() ){
-          Node eqc = (*eqcs_i);
-          if( eqc.getType()==d_type ){
-            //we must ensure that this equivalence class has been accounted for
-            if( d_regions_map.find( eqc )==d_regions_map.end() ){
-              //split on unaccounted for term and cardinality lemma term (as default)
-              Node splitEq = eqc.eqNode( d_cardinality_term );
-              splitEq = Rewriter::rewrite( splitEq );
-              Trace("uf-ss-minimize") << "Last chance minimize : " << splitEq << std::endl;
-              out->split( splitEq );
-              //tell the sat solver to explore the equals branch first
-              out->requirePhase( splitEq, true );
-              ++( d_thss->d_statistics.d_split_lemmas );
-              return false;
-            }
-          }
-          ++eqcs_i;
-        }
-        Assert( false );
-      }
-#endif
-    }else{
-      Trace("uf-ss-debug")  << "Minimize the UF model..." << std::endl;
-      //internal minimize, ensure that model forms a clique:
-      // if two equivalence classes are neither equal nor disequal, add a split
-      int validRegionIndex = -1;
-      for( int i=0; i<(int)d_regions_index; i++ ){
-        if( d_regions[i]->valid() ){
-          if( validRegionIndex!=-1 ){
-            combineRegions( validRegionIndex, i );
-            if( addSplit( d_regions[validRegionIndex], out )!=0 ){
-              Trace("uf-ss-debug") << "Minimize model : combined regions, found split. " << std::endl;
-              return false;
-            }
-          }else{
-            validRegionIndex = i;
-          }
-        }
-      }
-      Assert( validRegionIndex!=-1 );
-      if( addSplit( d_regions[validRegionIndex], out )!=0 ){
-        Trace("uf-ss-debug") << "Minimize model : found split. " << std::endl;
-        return false;
-      }
-      Trace("uf-ss-debug") << "Minimize success. " << std::endl;
-    }
-  }
-  return true;
-}
-
-
 int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
   int ni = d_regions_map[n];
   int counter = 0;
@@ -950,21 +864,6 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
         }
       }
     }else{
-      /*
-      if( options::ufssModelInference() ){
-        //check if we are at decision level 0
-        if( d_th->d_valuation.getAssertionLevel()==0 ){
-          Trace("uf-ss-mi") << "We have proved that no models of size " << c << " for type " << d_type << " exist." << std::endl;
-          Trace("uf-ss-mi") << "  # Clique lemmas : " << d_cliques[c].size() << std::endl;
-          if( d_cliques[c].size()==1 ){
-            if( d_totality_terms[c+1].empty() ){
-              Trace("uf-ss-mi") << "*** Establish model" << std::endl;
-              //d_totality_terms[c+1].insert( d_totality_terms[c].begin(), d_cliques[c][0].begin(), d_cliques[c][0].end() );
-            }
-          }
-        }
-      }
-      */
       //see if we need to request a new cardinality
       if( !d_hasCard ){
         bool needsCard = true;
@@ -1248,12 +1147,6 @@ void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out
   while( clique.size()>size_t(d_cardinality+1) ){
     clique.pop_back();
   }
-  //debugging information
-  if( Trace.isOn("uf-ss-cliques") ){
-    std::vector< Node > clique_vec;
-    clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
-    addClique( d_cardinality, clique_vec );
-  }
   // add as lemma
   std::vector<Node> eqs;
   for (unsigned i = 0, size = clique.size(); i < size; i++)
@@ -1323,25 +1216,14 @@ void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
   }
 }
 
-void SortModel::addClique( int c, std::vector< Node >& clique ) {
-  //if( d_clique_trie[c].add( clique ) ){
-  //  d_cliques[ c ].push_back( clique );
-  //}
-}
-
-
 /** apply totality */
 bool SortModel::applyTotality( int cardinality ){
   return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
-  // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
 }
 
 /** get totality lemma terms */
 Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){
   return d_totality_terms[0][i];
-  //}else{
-  //  return d_totality_terms[cardinality][i];
-  //}
 }
 
 void SortModel::simpleCheckCardinality() {
@@ -1909,8 +1791,6 @@ SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
   }
 }
 
-void StrongSolverTheoryUF::notifyRestart(){}
-
 /** get cardinality for sort */
 int StrongSolverTheoryUF::getCardinality( Node n ) {
   SortModel* c = getSortModel( n );
@@ -1929,18 +1809,6 @@ int StrongSolverTheoryUF::getCardinality( TypeNode tn ) {
   return -1;
 }
 
-bool StrongSolverTheoryUF::minimize( TheoryModel* m ){
-  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-    if( !it->second->minimize( d_out, m ) ){
-      return false;
-    }
-  }
-  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-    Trace("uf-ss-minimize") << "Cardinality( " << it->first << " ) : " << it->second->getCardinality() << std::endl;
-  }
-  return true;
-}
-
 //print debug
 void StrongSolverTheoryUF::debugPrint( const char* c ){
   //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine );
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 5108e7ba1..2e219da04 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -200,8 +200,6 @@ public:
       void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities );
       /** check for cliques */
       bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
-      /** get candidate clique */
-      bool getCandidateClique( int cardinality, std::vector< Node >& clique );
       //print debug
       void debugPrint( const char* c, bool incClique = false );
 
@@ -260,26 +258,6 @@ public:
     void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out );
     /** add totality axiom */
     void addTotalityAxiom( Node n, int cardinality, OutputChannel* out );
-
-    class NodeTrie {
-    public:
-      bool add( std::vector< Node >& n, unsigned i = 0 ){
-        Assert( i<n.size() );
-        if( i==(n.size()-1) ){
-          bool ret = d_children.find( n[i] )==d_children.end();
-          d_children[n[i]].d_children.clear();
-          return ret;
-        }else{
-          return d_children[n[i]].add( n, i+1 );
-        }
-      }
-    private:
-      std::map< Node, NodeTrie > d_children;
-    }; /* class NodeTrie */
-
-    std::map< int, NodeTrie > d_clique_trie;
-    void addClique( int c, std::vector< Node >& clique );
-
     /** Are we in conflict */
     context::CDO<bool> d_conflict;
     /** cardinality */
@@ -338,8 +316,6 @@ public:
     void propagate( Theory::Effort level, OutputChannel* out );
     /** get next decision request */
     Node getNextDecisionRequest();
-    /** minimize */
-    bool minimize( OutputChannel* out, TheoryModel* m );
     /** assert cardinality */
     void assertCardinality( OutputChannel* out, int c, bool val );
     /** is in conflict */
@@ -393,8 +369,6 @@ public:
   Node getNextDecisionRequest( unsigned& priority );
   /** preregister a term */
   void preRegisterTerm( TNode n );
-  /** notify restart */
-  void notifyRestart();
   /** identify */
   std::string identify() const { return std::string("StrongSolverTheoryUF"); }
   //print debug
@@ -407,8 +381,6 @@ public:
   int getCardinality( Node n );
   /** get cardinality for type */
   int getCardinality( TypeNode tn );
-  /** minimize */
-  bool minimize( TheoryModel* m = NULL );
   /** has eqc */
   bool hasEqc(Node a);
 
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index a4d318067..ea3a70362 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -155,6 +155,8 @@ REG0_TESTS = \
 	regress0/bug605.cvc \
 	regress0/bug639.smt2 \
 	regress0/buggy-ite.smt2 \
+	regress0/bv/ackermann1.smt2 \
+	regress0/bv/ackermann2.smt2 \
 	regress0/bv/bool-to-bv.smt2 \
 	regress0/bv/bug260a.smt \
 	regress0/bv/bug260b.smt \
@@ -1280,6 +1282,7 @@ REG1_TESTS = \
 	regress1/quantifiers/constfunc.cvc \
 	regress1/quantifiers/dump-inst.smt2 \
 	regress1/quantifiers/dump-inst-i.smt2 \
+	regress1/quantifiers/dump-inst-proof.smt2 \
 	regress1/quantifiers/ext-ex-deq-trigger.smt2 \
 	regress1/quantifiers/extract-nproc.smt2 \
 	regress1/quantifiers/florian-case-ax.smt2 \
@@ -1293,6 +1296,7 @@ REG1_TESTS = \
 	regress1/quantifiers/isaplanner-goal20.smt2 \
 	regress1/quantifiers/is-even.smt2 \
 	regress1/quantifiers/javafe.ast.StmtVec.009.smt2 \
+	regress1/quantifiers/lra-vts-inf.smt2 \
 	regress1/quantifiers/mix-coeff.smt2 \
 	regress1/quantifiers/model_6_1_bv.smt2 \
 	regress1/quantifiers/mutualrec2.cvc \
@@ -1321,6 +1325,8 @@ REG1_TESTS = \
 	regress1/quantifiers/qbv-test-urem-rewrite.smt2 \
 	regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \
 	regress1/quantifiers/qcft-smtlib3dbc51.smt2 \
+	regress1/quantifiers/qe.smt2 \
+	regress1/quantifiers/qe-partial.smt2 \
 	regress1/quantifiers/quant-wf-int-ind.smt2 \
 	regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \
 	regress1/quantifiers/repair-const-nterm.smt2 \
diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2
new file mode 100644
index 000000000..9b96b38c4
--- /dev/null
+++ b/test/regress/regress0/bv/ackermann1.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_UFBV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v0 () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4))
+(declare-fun g ((_ BitVec 4)) (_ BitVec 4))
+
+(assert (= (f (f v0)) (g (f v0))))
+
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
new file mode 100644
index 000000000..eeca505fe
--- /dev/null
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_UFBV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v0 () (_ BitVec 4))
+(declare-fun v1 () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4))
+(declare-fun g ((_ BitVec 4)) (_ BitVec 4))
+(declare-fun h ((_ BitVec 4)) (_ BitVec 4))
+
+(assert (not (= (f (g (h v0))) (f (g (h v1))))))
+(assert (= v0 v1))
+
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
new file mode 100644
index 000000000..c4eedc16f
--- /dev/null
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -0,0 +1,26 @@
+; COMMAND-LINE: --dump-instantiations --proof
+; EXPECT: unsat
+; EXPECT: (instantiation (forall ((x Int)) (or (P x) (Q x)) )
+; EXPECT:   ( 2 )
+; EXPECT: )
+; EXPECT: (instantiation (forall ((x Int)) (or (not (S x)) (not (Q x))) )
+; EXPECT:   ( 2 )
+; EXPECT: )
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun P (Int) Bool)
+(declare-fun Q (Int) Bool)
+(declare-fun R (Int) Bool)
+(declare-fun S (Int) Bool)
+(declare-fun W (Int) Bool)
+(declare-fun U (Int) Bool)
+(assert (forall ((x Int)) (or (P x) (Q x))))
+(assert (forall ((x Int)) (or (R x) (W x))))
+(assert (forall ((x Int)) (or (S x) (U x))))
+(assert (forall ((x Int)) (or (not (S x)) (not (Q x)))))
+(assert (and (not (R 0)) (not (R 10)) (not (S 1)) (not (P 2))))
+(assert (S 2))
+; This tests that --proof minimizes the instantiations printed out.
+; This regression should require only the 2 instantiations above, but
+; may try more.
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/lra-vts-inf.smt2 b/test/regress/regress1/quantifiers/lra-vts-inf.smt2
new file mode 100644
index 000000000..22d6455fb
--- /dev/null
+++ b/test/regress/regress1/quantifiers/lra-vts-inf.smt2
@@ -0,0 +1,144 @@
+; COMMAND-LINE: --cbqi-use-inf-int --cbqi-use-inf-real
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic LRA)
+(set-info :source |
+   Monniaux, David; Quantifier Elimination by Lazy Model Enumeration, CAV 2010
+|)
+(set-info :category "random")
+; ./Mjollnir_examples/B5/formula_171.m
+(set-info :status unsat)
+(assert
+ (forall ((|v17:0| Real) )(forall ((|v16:1| Real) )(forall ((|v15:2| Real) )(forall ((|v14:3| Real) )(forall ((|v13:4| Real) )(forall ((|v12:5| Real) )(exists ((|v11:6| Real) )(exists ((|v10:7| Real) )(exists ((|v9:8| Real) )(exists ((|v8:9| Real) )(exists ((|v7:10| Real) )(exists ((|v6:11| Real) )(forall ((|v5:12| Real) )(forall ((|v4:13| Real) )(forall ((|v3:14| Real) )(forall ((|v2:15| Real) )(forall ((|v1:16| Real) )(forall ((|v0:17| Real) )(let ((?x104 10))
+(let ((?x10 8))
+(let ((?x457 (* ?x10 |v0:17|)))
+(let ((?x538 (+ (+ (* (- 7) |v5:12|) (* 14 |v10:7|)) (* (- 19) |v15:2|))))
+(let ((?x49 19))
+(let ((?x27 (- 15)))
+(let ((?x310 (* ?x27 |v10:7|)))
+(let ((?x532 (+ (+ (+ (* 7 |v12:5|) (* (- 20) |v4:13|)) ?x310) (* 20 |v16:1|))))
+(let ((?x59 (- 16)))
+(let ((?x85 (- 13)))
+(let ((?x187 (* ?x85 |v3:14|)))
+(let ((?x524 (+ (+ (* (- 20) |v5:12|) (* 4 |v13:4|)) (* (- 10) |v2:15|))))
+(let ((?x266 18))
+(let ((?x170 (- 14)))
+(let ((?x308 (* ?x170 |v16:1|)))
+(let ((?x520 (+ (+ (+ (* (- 19) |v2:15|) (* 13 |v7:10|)) ?x308) (* (- 12) |v1:16|))))
+(let (($x542 (and (and (<= ?x520 ?x266) (<= (+ ?x524 ?x187) ?x59)) (and (<= ?x532 ?x49) (<= (+ ?x538 ?x457) ?x104)))))
+(let ((?x158 (- 11)))
+(let ((?x79 6))
+(let ((?x290 (* ?x79 |v3:14|)))
+(let ((?x512 (+ (+ (+ (* (- 8) |v9:8|) (* (- 9) |v0:17|)) ?x290) (* (- 18) |v8:9|))))
+(let ((?x504 (+ (+ (* (- 18) |v12:5|) (* (- 18) |v10:7|)) (* 15 |v5:12|))))
+(let ((?x14 (- 18)))
+(let ((?x100 7))
+(let ((?x471 (* ?x100 |v6:11|)))
+(let (($x499 (<= (+ (+ (+ (* (- 8) |v6:11|) (* ?x100 |v2:15|)) |v17:0|) ?x471) ?x14)))
+(let ((?x177 (- 3)))
+(let ((?x490 (+ (+ (* (- 19) |v14:3|) (* (- 8) |v13:4|)) (* ?x158 |v16:1|))))
+(let (($x515 (and (or (<= (+ ?x490 (* (- 7) |v10:7|)) ?x177) $x499) (or (<= (+ ?x504 (* ?x79 |v0:17|)) ?x266) (<= ?x512 ?x158)))))
+(let ((?x479 (+ (+ (* 13 |v4:13|) (* (- 17) |v4:13|)) (* 11 |v3:14|))))
+(let ((?x110 3))
+(let ((?x33 (* ?x14 |v9:8|)))
+(let (($x474 (<= (+ (+ (+ (* ?x110 |v0:17|) (* 16 |v7:10|)) ?x471) ?x33) ?x110)))
+(let ((?x233 1))
+(let ((?x464 (+ (+ (* ?x158 |v17:0|) (* 4 |v4:13|)) (* (- 5) |v8:9|))))
+(let ((?x24 12))
+(let ((?x458 (+ (+ (+ (* (- 12) |v5:12|) (* 14 |v16:1|)) |v3:14|) ?x457)))
+(let (($x484 (or (and (<= ?x458 ?x24) (<= (+ ?x464 (* (- 12) |v4:13|)) ?x233)) (and $x474 (<= (+ ?x479 (* (- 4) |v12:5|)) ?x59)))))
+(let ((?x447 (+ (+ (* (- 20) |v14:3|) (* (- 19) |v16:1|)) (* 2 |v2:15|))))
+(let ((?x439 (+ (+ (* ?x10 |v13:4|) (* 4 |v13:4|)) (* (- 7) |v11:6|))))
+(let (($x451 (or (<= (+ ?x439 (* (- 5) |v7:10|)) ?x24) (<= (+ ?x447 (* ?x170 |v14:3|)) ?x110))))
+(let ((?x62 (- 17)))
+(let ((?x430 (+ (+ (* (- 1) |v11:6|) (* 5 |v14:3|)) (* ?x104 |v17:0|))))
+(let ((?x190 11))
+(let ((?x424 (+ (+ (+ (* ?x190 |v5:12|) (* (- 10) |v5:12|)) (* ?x27 |v14:3|)) (* 2 |v12:5|))))
+(let (($x485 (or (and (and (<= ?x424 ?x190) (<= (+ ?x430 (* ?x24 |v16:1|)) ?x62)) $x451) $x484)))
+(let ((?x164 4))
+(let ((?x415 (+ (+ (* ?x104 |v15:2|) (* (- 6) |v7:10|)) (* 17 |v1:16|))))
+(let ((?x407 (+ (+ (+ (* ?x59 |v11:6|) (* ?x10 |v14:3|)) (* ?x10 |v7:10|)) (* (- 6) |v8:9|))))
+(let ((?x52 16))
+(let ((?x395 (+ (+ (* (- 5) |v12:5|) (* ?x104 |v15:2|)) (* (- 7) |v1:16|))))
+(let ((?x121 (- 8)))
+(let ((?x389 (+ (+ (+ (* (- 9) |v13:4|) (* ?x110 |v0:17|)) (* ?x59 |v17:0|)) (* ?x190 |v4:13|))))
+(let ((?x346 (* ?x27 |v16:1|)))
+(let ((?x381 (+ (+ (+ (* ?x158 |v12:5|) (* ?x121 |v16:1|)) (* 5 |v0:17|)) ?x346)))
+(let (($x410 (and (or (<= ?x381 ?x104) (<= ?x389 ?x121)) (or (<= (+ ?x395 (* 9 |v9:8|)) ?x52) (<= ?x407 ?x110)))))
+(let ((?x370 (+ (+ (* (- 2) |v14:3|) (* (- 1) |v15:2|)) (* ?x85 |v6:11|))))
+(let ((?x97 (- 2)))
+(let ((?x361 (+ (+ (* ?x27 |v15:2|) (* (- 20) |v4:13|)) (* 20 |v9:8|))))
+(let (($x374 (or (<= (+ ?x361 (* (- 9) |v7:10|)) ?x97) (<= (+ ?x370 (* (- 19) |v17:0|)) ?x52))))
+(let ((?x195 20))
+(let ((?x354 (+ (+ (+ (* ?x49 |v11:6|) (* ?x59 |v2:15|)) (* 17 |v8:9|)) |v17:0|)))
+(let ((?x347 (+ (+ (+ (* (- 7) |v7:10|) (* ?x104 |v10:7|)) (* ?x104 |v6:11|)) ?x346)))
+(let (($x419 (or (and (or (or (<= ?x347 ?x100) (<= ?x354 ?x195)) $x374) $x410) (<= (+ ?x415 (* ?x27 |v1:16|)) ?x164))))
+(let ((?x151 (- 20)))
+(let ((?x333 (* ?x151 |v5:12|)))
+(let (($x335 (<= (+ (+ (+ (* ?x104 |v9:8|) (* ?x151 |v3:14|)) (* ?x110 |v13:4|)) ?x333) ?x151)))
+(let ((?x327 (+ (+ (+ (* ?x158 |v5:12|) (* ?x266 |v14:3|)) (* (- 12) |v14:3|)) (* 5 |v1:16|))))
+(let ((?x314 (* ?x14 |v13:4|)))
+(let (($x319 (<= (+ (+ (+ (* (- 19) |v4:13|) ?x314) (* ?x62 |v15:2|)) ?x314) ?x164)))
+(let ((?x311 (+ (+ (+ (* (- 19) |v6:11|) (* 17 |v0:17|)) ?x308) ?x310)))
+(let ((?x302 (+ (+ (+ (* ?x121 |v9:8|) (* ?x97 |v3:14|)) (* ?x59 |v11:6|)) (* ?x158 |v9:8|))))
+(let ((?x135 (- 10)))
+(let ((?x293 (+ (+ (+ (* ?x27 |v14:3|) (* ?x190 |v7:10|)) ?x290) (* (- 5) |v3:14|))))
+(let ((?x88 (- 5)))
+(let (($x288 (<= (+ (+ (+ (* ?x177 |v1:16|) (* ?x135 |v4:13|)) (* ?x135 |v7:10|)) |v14:3|) ?x88)))
+(let (($x338 (and (and (and $x288 (<= ?x293 ?x135)) (<= ?x302 ?x59)) (and (or (<= ?x311 ?x158) $x319) (or (<= ?x327 ?x233) $x335)))))
+(let ((?x278 (+ (+ (+ (* ?x27 |v12:5|) (* ?x85 |v9:8|)) (* ?x49 |v5:12|)) (* ?x49 |v15:2|))))
+(let ((?x270 (+ (+ (+ (* ?x10 |v14:3|) (* 17 |v6:11|)) (* ?x266 |v7:10|)) (* ?x24 |v9:8|))))
+(let ((?x41 (- 4)))
+(let ((?x259 (+ (+ (+ (* ?x100 |v8:9|) (* ?x177 |v6:11|)) (* 2 |v4:13|)) (* 13 |v12:5|))))
+(let ((?x249 (+ (+ (* 13 |v1:16|) (* ?x151 |v3:14|)) (* 17 |v15:2|))))
+(let (($x281 (and (and (<= (+ ?x249 (* ?x62 |v1:16|)) ?x110) (<= ?x259 ?x41)) (and (<= ?x270 ?x104) (<= ?x278 ?x24)))))
+(let ((?x228 15))
+(let ((?x241 (+ (+ (+ (* ?x88 |v5:12|) (* ?x49 |v10:7|)) (* ?x27 |v14:3|)) (* 17 |v7:10|))))
+(let ((?x232 (+ (+ (+ (* ?x24 |v17:0|) (* ?x135 |v4:13|)) (* ?x228 |v17:0|)) (* ?x88 |v1:16|))))
+(let ((?x117 (- 19)))
+(let ((?x220 (* ?x117 |v2:15|)))
+(let (($x222 (<= (+ (+ (+ (* ?x121 |v17:0|) (* ?x190 |v5:12|)) (* ?x190 |v7:10|)) ?x220) ?x104)))
+(let ((?x114 (- 1)))
+(let ((?x115 (* ?x114 |v1:16|)))
+(let ((?x212 (+ (+ (* 0 |v15:2|) (* 5 |v8:9|)) (* ?x110 |v10:7|))))
+(let (($x244 (and (and (<= (+ ?x212 ?x115) ?x10) $x222) (and (<= ?x232 ?x233) (<= ?x241 ?x228)))))
+(let ((?x128 2))
+(let ((?x202 (+ (+ (+ (* ?x195 |v10:7|) (* ?x121 |v10:7|)) (* ?x135 |v4:13|)) (* 17 |v12:5|))))
+(let (($x193 (<= (+ (+ (+ (* ?x151 |v12:5|) (* ?x114 |v4:13|)) ?x187) (* ?x190 |v12:5|)) ?x110)))
+(let ((?x181 (+ (+ (+ (* ?x110 |v6:11|) (* ?x164 |v15:2|)) (* ?x177 |v11:6|)) (* ?x10 |v9:8|))))
+(let (($x173 (<= (+ (+ (+ (* ?x164 |v10:7|) |v9:8|) (* ?x104 |v5:12|)) (* ?x170 |v6:11|)) ?x24)))
+(let ((?x161 14))
+(let ((?x160 (+ (+ (+ (* ?x151 |v8:9|) (* ?x128 |v16:1|)) (* ?x14 |v12:5|)) (* ?x158 |v0:17|))))
+(let (($x206 (and (<= ?x160 ?x161) (or (or $x173 (<= ?x181 ?x158)) (and $x193 (<= ?x202 ?x128))))))
+(let ((?x144 (+ (+ (+ (* ?x135 |v1:16|) (* ?x14 |v4:13|)) (* ?x10 |v12:5|)) (* 0 |v17:0|))))
+(let ((?x132 (+ (+ (+ (* ?x121 |v8:9|) (* 5 |v17:0|)) (* ?x128 |v13:4|)) (* 13 |v13:4|))))
+(let (($x118 (<= (+ (+ (+ (* ?x104 |v15:2|) (* ?x41 |v7:10|)) (* ?x110 |v6:11|)) ?x115) ?x117)))
+(let ((?x98 (* ?x97 |v14:3|)))
+(let ((?x99 (+ (+ (+ (* ?x85 |v17:0|) (* ?x88 |v15:2|)) (* 0 |v1:16|)) ?x98)))
+(let ((?x78 (+ (+ (+ (* ?x14 |v7:10|) (* (- 7) |v0:17|)) |v3:14|) (* (- 12) |v17:0|))))
+(let ((?x61 (+ (+ (+ (* ?x49 |v8:9|) (* ?x52 |v10:7|)) (* ?x24 |v1:16|)) (* ?x59 |v1:16|))))
+(let ((?x36 13))
+(let (($x44 (<= (+ (+ (+ (* ?x10 |v11:6|) ?x33) (* ?x36 |v15:2|)) (* ?x41 |v2:15|)) ?x36)))
+(let ((?x26 (+ (+ (+ (* ?x10 |v16:1|) (* ?x14 |v5:12|)) (* 17 |v10:7|)) (* ?x24 |v13:4|))))
+(let (($x148 (or (and (and (<= ?x26 ?x27) $x44) (and (<= ?x61 ?x62) (<= ?x78 ?x79))) (or (and (<= ?x99 ?x100) $x118) (and (<= ?x132 ?x41) (<= ?x144 ?x104))))))
+(or (and (and $x148 $x206) (and (or $x244 $x281) $x338)) (and $x419 (or $x485 (and $x515 $x542)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/quantifiers/qe-partial.smt2 b/test/regress/regress1/quantifiers/qe-partial.smt2
new file mode 100644
index 000000000..6f414fb2c
--- /dev/null
+++ b/test/regress/regress1/quantifiers/qe-partial.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE:
+; SCRUBBER: sed -e 's/(not (>= (+ .* (\* (- 1) .*)) 1))$/(not (>= (+ TERMA (\* (- 1) TERMB)) 1))/'
+; EXPECT: (not (>= (+ TERMA (* (- 1) TERMB)) 1))
+(set-logic LIA)
+(set-info :status unsat)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(get-qe-disjunct (exists ((x Int)) (and (<= a x) (or (<= x b) (<= x c)))))
diff --git a/test/regress/regress1/quantifiers/qe.smt2 b/test/regress/regress1/quantifiers/qe.smt2
new file mode 100644
index 000000000..673ece05b
--- /dev/null
+++ b/test/regress/regress1/quantifiers/qe.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE:
+; EXPECT: (not (>= (+ a (* (- 1) b)) 1))
+(set-logic LIA)
+(set-info :status unsat)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(get-qe (exists ((x Int)) (and (<= a x) (<= x b))))