Protype e-solver implementationesolverPrototype

31 files changed, 2305 insertions, 30 deletions

diff --git a/.clang-format b/.clang-format
index a4e83f330..23e537b33 100644
--- a/.clang-format
+++ b/.clang-format
@@ -6,7 +6,6 @@ BinPackArguments: false
 BinPackParameters: false
 BreakBeforeBinaryOperators: NonAssignment
 BraceWrapping:
-  AfterCaseLabel: true
   AfterClass: true
   AfterControlStatement: true
   AfterEnum: true
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6c3ed4bbc..3180c780e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -256,9 +256,9 @@ execute_process(COMMAND ${CMAKE_C_COMPILER}
                 -fuse-ld=gold
                 -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION)
 if ("${LD_VERSION}" MATCHES "GNU gold")
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold")
-  string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold")
-  string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold -lpthread")
+  string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold -lpthread")
+  string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold -lpthread")
   message(STATUS "Using GNU gold linker.")
 endif ()
 
@@ -453,6 +453,9 @@ endif()
 if(ENABLE_PROFILING)
   add_definitions(-DCVC4_PROFILING)
   add_check_c_cxx_flag("-pg")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -pg")
+  string(APPEND CMAKE_SHARED_LINKER_FLAGS " -pg")
+  string(APPEND CMAKE_MODULE_LINKER_FLAGS " -pg")
 endif()
 
 if(ENABLE_PROOFS)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0929b6625..58e5927af 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -223,6 +223,12 @@ libcvc4_add_sources(
   smt/dump.h
   smt/dump_manager.cpp
   smt/dump_manager.h
+  smt/e_solver/e_solver.cpp
+  smt/e_solver/e_solver.h
+  smt/e_solver/thread_pool.h
+  smt/e_solver/var_map.h
+  smt/e_solver/worker.cpp
+  smt/e_solver/worker.h
   smt/expand_definitions.cpp
   smt/expand_definitions.h
   smt/listeners.cpp
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index f1386b84d..a41859fe8 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -30,6 +30,12 @@ ${includes}
 
 namespace CVC4 {
 
+namespace smt {
+struct Instantiator;
+struct VarMap;
+struct Worker;
+}
+
 namespace api {
 class Solver;
 }
@@ -45,6 +51,9 @@ class ResourceManager;
 class CVC4_PUBLIC ExprManager {
  private:
   friend api::Solver;
+  friend smt::Instantiator;
+  friend smt::VarMap;
+  friend smt::Worker;
   /** The internal node manager */
   NodeManager* d_nodeManager;
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 59afec4a6..6df13c3b7 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -610,7 +610,7 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
     }
     AlwaysAssert(nameResolutions.find(dtc->getName()) == nameResolutions.end())
         << "cannot construct two datatypes at the same time "
-           "with the same name";
+           "with the same name (" << dtc->getName() << ")";
     nameResolutions.insert(std::make_pair(dtc->getName(), typeNode));
     dtts.push_back(typeNode);
   }
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 19434fa33..ab0ab38b3 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -178,5 +178,4 @@ header = "options/datatypes_options.h"
   long       = "sygus-abort-size=N"
   type       = "int"
   default    = "-1"
-  read_only  = true
   help       = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)"
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 4b98cb84d..f7fdc7758 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -67,7 +67,6 @@ header = "options/quantifiers_options.h"
   long       = "var-elim-quant"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "enable simple variable elimination for quantified formulas"
 
 [[option]]
@@ -76,7 +75,6 @@ header = "options/quantifiers_options.h"
   long       = "var-ineq-elim-quant"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "enable variable elimination based on infinite projection of unbound arithmetic variables"
 
 [[option]]
@@ -112,7 +110,6 @@ header = "options/quantifiers_options.h"
   long       = "cond-var-split-quant"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "split quantified formulas that lead to variable eliminations"
 
 [[option]]
@@ -121,7 +118,6 @@ header = "options/quantifiers_options.h"
   long       = "cond-var-split-agg-quant"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "aggressive split quantified formulas that lead to variable eliminations"
 
 [[option]]
@@ -174,7 +170,6 @@ header = "options/quantifiers_options.h"
   long       = "elim-taut-quant"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "eliminate tautological disjuncts of quantified formulas"
 
 [[option]]
@@ -517,7 +512,6 @@ header = "options/quantifiers_options.h"
   long       = "full-saturate-quant-rd"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "whether to use relevant domain first for enumerative instantiation strategy"
 
 [[option]]
@@ -526,7 +520,6 @@ header = "options/quantifiers_options.h"
   long       = "full-saturate-quant-limit=N"
   type       = "int"
   default    = "-1"
-  read_only  = true
   help       = "maximum number of rounds of enumerative instantiation to apply (-1 means no limit)"
   
 [[option]]
@@ -1116,7 +1109,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-active-gen=MODE"
   type       = "SygusActiveGenMode"
   default    = "AUTO"
-  read_only  = true
   help       = "mode for actively-generated sygus enumerators"
   help_mode  = "Modes for actively-generated sygus enumerators."
 [[option.mode.NONE]]
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index ed056ac9f..a0ae4a6b9 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -802,6 +802,22 @@ header = "options/smt_options.h"
   help       = "support the get-abduct command"
 
 [[option]]
+  name       = "eSolver"
+  category   = "undocumented"
+  long       = "e-solver"
+  type       = "bool"
+  default    = "false"
+  help       = "Use CEGAR solver for quantifiers"
+
+[[option]]
+  name       = "numThreads"
+  category   = "undocumented"
+  long       = "num-threads=N"
+  type       = "int"
+  default    = "1"
+  help       = "Number of threads"
+
+[[option]]
   name       = "checkInterpols"
   category   = "regular"
   long       = "check-interpols"
diff --git a/src/smt/e_solver/e_solver.cpp b/src/smt/e_solver/e_solver.cpp
new file mode 100644
index 000000000..95d96282e
--- /dev/null
+++ b/src/smt/e_solver/e_solver.cpp
@@ -0,0 +1,1110 @@
+/*********************                                                        */
+/*! \file e_solver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 A CEGAR solver for quantifiers
+ **/
+
+#include "smt/e_solver/e_solver.h"
+
+#include <chrono>
+#include <condition_variable>
+#include <future>
+#include <mutex>
+#include <thread>
+
+#include "expr/node_algorithm.h"
+#include "options/base_options.h"
+#include "options/datatypes_options.h"
+#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "smt/e_solver/thread_pool.h"
+#include "smt/e_solver/worker.h"
+#include "smt/model.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/cegqi/vts_term_cache.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/smt_engine_subsolver.h"
+#include "theory/theory_engine.h"
+#include "util/integer.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+namespace smt {
+
+using namespace CVC4::theory;
+
+struct Instantiator
+{
+  NodeManager* d_mainNm;
+  std::vector<TNode> d_key;
+  unsigned long d_timeout;
+  bool d_assertFunctionModels;
+  TNode d_cube;
+  TNode d_eBody;
+
+  Instantiator(NodeManager* mainNm, const LogicInfo& logic)
+      : d_mainNm(mainNm), d_timeout(1000), d_assertFunctionModels(false)
+  {
+  }
+
+  ~Instantiator() {}
+};
+
+ESolver::ESolver(SmtEngine* parent, SmtEngineState* state)
+    : d_parent(parent),
+      d_state(state),
+      d_eSolverTime("smt::eSolver::time"),
+      d_mainSolverTime("smt::eSolver::mainSolverTime"),
+      d_mainWaitTime("smt::eSolver::mainWaitTime"),
+      d_numMainChecks("smt::eSolver::numMainChecks", 0),
+      d_numAxioms("smt::eSolver::numAxioms", 0),
+      d_numRounds("smt::eSolver::numRounds", 0)
+{
+  Trace("e-solver") << "Using e-solver" << std::endl;
+  smtStatisticsRegistry()->registerStat(&d_eSolverTime);
+  smtStatisticsRegistry()->registerStat(&d_mainSolverTime);
+  smtStatisticsRegistry()->registerStat(&d_mainWaitTime);
+  smtStatisticsRegistry()->registerStat(&d_numMainChecks);
+  smtStatisticsRegistry()->registerStat(&d_numAxioms);
+  smtStatisticsRegistry()->registerStat(&d_numRounds);
+}
+
+ESolver::~ESolver()
+{
+  SmtScope smts(d_parent);
+  smtStatisticsRegistry()->unregisterStat(&d_eSolverTime);
+  smtStatisticsRegistry()->unregisterStat(&d_mainSolverTime);
+  smtStatisticsRegistry()->unregisterStat(&d_mainWaitTime);
+  smtStatisticsRegistry()->unregisterStat(&d_numMainChecks);
+  smtStatisticsRegistry()->unregisterStat(&d_numAxioms);
+  smtStatisticsRegistry()->unregisterStat(&d_numRounds);
+}
+
+Result ESolver::checkSatisfiability(Assertions& asserts)
+{
+  d_state->notifyCheckSat(false);
+
+  NodeManager* nm = NodeManager::currentNM();
+  preprocessing::AssertionPipeline ap = asserts.getAssertionPipeline();
+  std::vector<Node> as(ap.begin(), ap.end());
+  Node f = as.size() == 0
+               ? nm->mkConst(true)
+               : (as.size() == 1 ? as[0] : nm->mkNode(kind::AND, as));
+
+  Trace("e-solver") << "Original input " << f << std::endl;
+  f = collapseQuantifiers(f);
+  Trace("e-solver") << "Preprocessed input " << f << std::endl;
+
+  Result r = isUnsat(f);
+  if (r.isSat() == Result::SAT_UNKNOWN)
+  {
+    Trace("e-solver") << std::endl;
+    Trace("e-solver") << "Could not prove `unsat`, trying to prove `sat`..."
+                      << std::endl;
+    r = isUnsat(f.notNode());
+    if (r.isSat() == Result::UNSAT)
+    {
+      r = Result(Result::SAT);
+    }
+  }
+  d_state->notifyCheckSatResult(false, r);
+  return r;
+}
+
+std::pair<bool, JobOutput> refine(Worker* worker, Instantiator* instantiator)
+{
+  SmtEngine* smt = worker->d_smt.get();
+  NodeManager* nm = worker->getNodeManager();
+  SmtScope smts(smt);
+
+  bool timedOut = false;
+  std::vector<Node> toAssert;
+
+  {
+    Trace("e-solver") << "Worker updating assertions..." << std::endl;
+    std::vector<Node>& abstractAsserts = worker->d_abstractAsserts;
+    {
+      std::unique_lock<std::mutex> lock(worker->d_abstractAssertsBufferMut);
+      worker->d_abstractAssertsBufferCv.wait(lock, [worker] {
+        return worker->d_ready || worker->d_pool->stopped();
+      });
+      if (worker->d_pool->stopped())
+      {
+        Trace("e-solver") << "Thread pool stopped, shutting down" << std::endl;
+
+        lock.unlock();
+        return std::make_pair(true, JobOutput(worker, instantiator, {}, true));
+      }
+      for (const Node& am : worker->d_abstractAssertsBuffer)
+      {
+        Node a = worker->d_vmInterWorker.importNode(am);
+        Trace("e-solver") << "Asserting " << a << " to worker" << std::endl;
+        smt->assertFormula(a);
+        abstractAsserts.emplace_back(a);
+      }
+      {
+        NodeManagerScope nms(worker->d_interNm);
+        worker->d_abstractAssertsBuffer.clear();
+      }
+    }
+
+    smt->push();
+
+    Node cube;
+    {
+      NodeManagerScope nmsInter(worker->d_interNm);
+      Node cubeInter = worker->d_vmMainInter.importNode(instantiator->d_cube);
+      {
+        NodeManagerScope nmsWorker(worker->getNodeManager());
+        cube = worker->d_vmInterWorker.importNode(cubeInter);
+      }
+    }
+
+    Trace("e-solver") << "Asserting cube " << cube << std::endl;
+    smt->assertFormula(cube.notNode());
+
+    Trace("e-solver") << "Instantiator checking assertions... ";
+    Result r = smt->checkSat();
+    Trace("e-solver") << r << std::endl;
+    if (r.isUnknown() && r.whyUnknown() == Result::TIMEOUT)
+    {
+      worker->reinit();
+      return std::make_pair(false, JobOutput(worker, instantiator, {}, false));
+    }
+    else if (r.isSat() == Result::UNSAT
+             || (r.isUnknown() && (r.whyUnknown() == Result::INTERRUPTED)))
+    {
+      // Nothing more to learn from this instantiator
+      Trace("e-solver") << "Instantiator done";
+      smt->pop();
+      return std::make_pair(true, JobOutput(worker, instantiator, {}, true));
+    }
+
+    // Gather SAT assignment
+    std::unordered_set<Node, NodeHashFunction> literals;
+    std::unordered_set<Node, NodeHashFunction> asyms;
+    for (const Node& a : abstractAsserts)
+    {
+      worker->getLiterals(literals, a);
+      expr::getSymbols(a, asyms);
+    }
+    Trace("e-solver") << "SAT assignment = " << literals << std::endl;
+
+    // Gather function models
+    std::unordered_map<Node, Node, NodeHashFunction> cache;
+    std::unordered_map<Node, Node, NodeHashFunction> fmodels;
+    for (const Node& asym : asyms)
+    {
+      Node val = mapConsts(smt->getValue(asym), cache);
+      fmodels[asym] = val;
+    }
+
+    std::vector<Node> axioms;
+    bool useSygus = false;
+    std::vector<Node> ts;
+    for (const TNode& t : instantiator->d_key)
+    {
+      NodeManagerScope nmsInter(worker->d_interNm);
+      Node tInter = worker->d_vmMainInter.importNode(t);
+      {
+        NodeManagerScope nmsWorker(worker->getNodeManager());
+        ts.emplace_back(worker->d_vmInterWorker.importNode(tInter));
+      }
+    }
+    Node eBody;
+    {
+      NodeManagerScope nmsInter(worker->d_interNm);
+      Node eBodyInter = worker->d_vmMainInter.importNode(instantiator->d_eBody);
+      {
+        NodeManagerScope nmsWorker(worker->getNodeManager());
+        eBody = worker->d_vmInterWorker.importNode(eBodyInter);
+      }
+    }
+    Trace("e-solver") << "Body = " << eBody << std::endl;
+
+    std::vector<Node> tvs;
+    for (const Node& t : ts)
+    {
+      if (t.getKind() == kind::APPLY_UF)
+      {
+        Trace("e-solver")
+            << t.getOperator()
+            << " is a function,, using SyGuS for axiom instantiation"
+            << std::endl;
+        useSygus = true;
+        break;
+      }
+
+      Node val = smt->getValue(t);
+      if (val.isNull())
+      {
+        break;
+      }
+      tvs.emplace_back(val);
+    }
+
+    if (useSygus)
+    {
+      std::unique_ptr<SmtEngine> sygusChecker(new SmtEngine(nm));
+      sygusChecker->getOptions().set(options::inputLanguage,
+                                     language::input::LANG_SYGUS_V2);
+      sygusChecker->getOptions().set(options::incrementalSolving, false);
+      // sygusChecker->getOptions().set(options::sygusAbortSize, 2);
+      // sygusChecker->getOptions().set(options::sygusRepairConst, true);
+      sygusChecker->getOptions().set(options::sygusActiveGenMode,
+                                     options::SygusActiveGenMode::ENUM);
+      sygusChecker->setIsInternalSubsolver();
+      sygusChecker->setTimeLimit(instantiator->d_timeout);
+
+      Node f = abstractAsserts.size() == 0
+                   ? nm->mkConst(true)
+                   : (abstractAsserts.size() == 1
+                          ? abstractAsserts[0]
+                          : nm->mkNode(kind::AND, abstractAsserts));
+
+      std::vector<Node> funs;
+      for (const Node& t : ts)
+      {
+        std::stringstream ss;
+        ss << "f" << t.getOperator() << "_";
+        Node fun = nm->mkBoundVar(ss.str(), t.getOperator().getType());
+        funs.emplace_back(fun);
+        Trace("e-solver") << "Synthesizing function " << fun << " with type "
+                          << fun.getType() << std::endl;
+
+        std::vector<Node> vars;
+        Assert(t.getKind() == kind::APPLY_UF);
+        for (const Node& v : t)
+        {
+          Node bv = nm->mkBoundVar("v", v.getType());
+          vars.emplace_back(bv);
+        }
+        sygusChecker->declareSynthFun(fun, false, vars);
+
+        f = f.substitute(TNode(t.getOperator()), TNode(fun));
+        f = f.substitute(t.begin(), t.end(), vars.begin(), vars.end());
+      }
+
+      std::unordered_set<Node, NodeHashFunction> symss;
+      expr::getSymbols(f, symss);
+
+      std::vector<Node> fsyms;
+      std::vector<Node> fsymModels;
+      std::vector<Node> syms;
+      for (const Node& n : symss)
+      {
+        if (std::find(ts.begin(), ts.end(), n) != ts.end())
+        {
+          continue;
+        }
+
+        if (n.getType().isFunction())
+        {
+          fsyms.emplace_back(n);
+          fsymModels.emplace_back(smt->getValue(n));
+        }
+        else if (n.getType().getKind() != kind::SELECTOR_TYPE)
+        {
+          syms.emplace_back(n);
+        }
+      }
+
+      f = f.substitute(
+          fsyms.begin(), fsyms.end(), fsymModels.begin(), fsymModels.end());
+
+      std::vector<Node> svars;
+      for (const Node& sym : syms)
+      {
+        std::stringstream ss;
+        ss << "s" << sym << "_";
+        Node bv = nm->mkBoundVar(ss.str(), sym.getType());
+        svars.emplace_back(bv);
+        sygusChecker->declareSygusVar(bv);
+        Trace("e-solver") << "SyGuS variable " << sym << " -> " << bv << " ("
+                          << sym.getType() << ")" << std::endl;
+      }
+      f = f.substitute(syms.begin(), syms.end(), svars.begin(), svars.end());
+
+      Trace("e-solver") << "f = " << f << std::endl;
+      Trace("e-solver") << "syms = " << syms << std::endl;
+      Trace("e-solver") << "Synthesizing... ";
+      sygusChecker->assertSygusConstraint(f.notNode());
+      Result sr = sygusChecker->checkSynth();
+      Trace("e-solver") << sr << std::endl;
+
+      if (sr.isSat() == Result::UNSAT)
+      {
+        std::map<Node, Node> fmap;
+        sygusChecker->getSynthSolutions(fmap);
+
+        Trace("e-solver") << "Found solution" << std::endl;
+        Node qt = eBody;
+        Assert(funs.size() == ts.size());
+        for (size_t i = 0, size = funs.size(); i < size; i++)
+        {
+          Node t = ts[i];
+          Node fun = funs[i];
+          Node result = fmap[fun];
+          Trace("e-solver") << "  " << fun << ": " << result << std::endl;
+          qt = qt.substitute(TNode(t.getOperator()), TNode(result));
+        }
+
+        Node axiomInst = nm->mkNode(kind::IMPLIES, qt, eBody);
+        Trace("e-solver") << "Adding axiom instance: " << axiomInst
+                          << std::endl;
+        toAssert.emplace_back(axiomInst);
+      }
+      else
+      {
+        Trace("e-solver") << "No solution found for synthesis problem"
+                          << std::endl;
+        instantiator->d_timeout *= 2;
+      }
+    }
+    else
+    {
+      std::vector<Node> bvs;
+      for (size_t i = 0, size = ts.size(); i < size; i++)
+      {
+        Node t = ts[i];
+        std::stringstream ss;
+        ss << "t" << i;
+        bvs.emplace_back(nm->mkBoundVar(ss.str(), t.getType()));
+      }
+      Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, bvs);
+      Node qt = eBody.substitute(ts.begin(), ts.end(), bvs.begin(), bvs.end());
+      Node qbody = nm->mkNode(kind::IMPLIES, qt, eBody);
+
+      TypeNode boolType = nm->booleanType();
+      Node qvar = nm->mkSkolem("qid", boolType);
+      Node ip = nm->mkNode(kind::INST_ATTRIBUTE, qvar);
+      Node ipl = nm->mkNode(kind::INST_PATTERN_LIST, ip);
+
+      qvar.setAttribute(InternalQuantAttribute(), true);
+      smt->setUserAttribute("qid", qvar, {}, "");
+
+      Node axiom = nm->mkNode(kind::FORALL, bvl, qbody, ipl);
+      axioms.emplace_back(axiom);
+      Trace("e-solver") << "Adding axiom... " << axiom << std::endl;
+    }
+
+    smt->push();
+
+    // Assert SAT assignment
+    for (const Node& literal : literals)
+    {
+      smt->assertFormula(literal);
+    }
+
+    // Assert models of function symbols
+    if (instantiator->d_assertFunctionModels)
+    {
+      for (const Node& asym : asyms)
+      {
+        if (asym.getType().isFunction())
+        {
+          Node val = fmodels[asym];
+          std::vector<Node> args(val[0].begin(), val[0].end());
+          Trace("e-solver") << "Asserting function model " << asym << " = "
+                            << val << std::endl;
+          smt->defineFunction(asym, args, val[1]);
+        }
+      }
+    }
+
+    Node qt;
+    for (const Node& axiom : axioms)
+    {
+      Trace("e-solver") << "Testing axiom " << axiom << "... ";
+      smt->push();
+      smt->assertFormula(axiom);
+      smt->setTimeLimit(instantiator->d_timeout);
+      Result ar = smt->checkSat();
+      Trace("e-solver") << ar << std::endl;
+
+      if (ar.isUnknown() && ar.whyUnknown() == Result::TIMEOUT)
+      {
+        timedOut = true;
+      }
+
+      if (ar.isSat() != Result::SAT)
+      {
+        std::vector<Node> qs;
+        smt->getInstantiatedQuantifiedFormulas(qs);
+
+        for (const Node& q : qs)
+        {
+          std::vector<std::vector<Node>> tvecs;
+          smt->getInstantiationTermVectors(q, tvecs);
+          Trace("e-solver") << "Quantifier: " << q << std::endl;
+          for (const std::vector<Node>& tvec : tvecs)
+          {
+            bool skip = false;
+            for (size_t i = 0, size = tvec.size(); i < size; i++)
+            {
+              Node tv = tvec[i];
+              Node t = axiom[0][i];
+              if (tv.getKind() == kind::WITNESS || t.getType() != tv.getType())
+              {
+                skip = true;
+                break;
+              }
+            }
+            if (skip)
+            {
+              continue;
+            }
+
+            Trace("e-solver") << "  Instantiations: " << tvec << std::endl;
+            Node axiomInst = axiom[1].substitute(
+                axiom[0].begin(), axiom[0].end(), tvec.begin(), tvec.end());
+            toAssert.emplace_back(axiomInst);
+            Node lemma = additionalLemmas(axiomInst);
+            if (!lemma.isConst())
+            {
+              toAssert.emplace_back(lemma);
+            }
+          }
+        }
+      }
+      smt->pop();
+    }
+
+    smt->pop();
+    smt->pop();
+  }
+
+  JobOutput jo(worker, instantiator, toAssert, false);
+  toAssert.clear();
+
+  if (timedOut)
+  {
+    Trace("e-solver") << "Instantiator timed out, reinitializing" << std::endl;
+    instantiator->d_assertFunctionModels =
+        !instantiator->d_assertFunctionModels;
+    worker->reinit();
+    instantiator->d_timeout *= 2;
+  }
+
+  return std::make_pair(false, jo);
+}
+
+Result ESolver::isUnsat(Node f)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  SmtEngine* smtCurr = smt::currentSmtEngine();
+
+  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  std::map<std::vector<Node>, std::pair<Node, Node>> eMap;
+  std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
+      termIndex;
+  std::unordered_set<Node, NodeHashFunction> axiomsSent;
+
+  std::mutex abstractAssertsMut;
+  Trace("e-solver") << "Original formula" << std::endl;
+  std::vector<Node> abstractAsserts;
+  Trace("e-solver") << "  " << f << std::endl;
+  abstractAsserts.emplace_back(abstract(f, cache, eMap));
+  Trace("e-solver") << std::endl;
+
+  if (Trace.isOn("e-solver"))
+  {
+    Trace("e-solver") << "Mappings" << std::endl;
+    for (const std::pair<const std::vector<Node>, std::pair<Node, Node>>&
+             mapping : eMap)
+    {
+      Trace("e-solver") << "  " << mapping.first << " -> " << mapping.second
+                        << std::endl;
+    }
+    Trace("e-solver") << std::endl;
+  }
+
+  std::unique_ptr<SmtEngine> mainChecker;
+  theory::initializeSubsolver(mainChecker);
+  mainChecker->getOptions().set(options::produceModels, true);
+  mainChecker->getOptions().set(options::incrementalSolving, true);
+  mainChecker->getOptions().set(options::eSolver, false);
+
+  std::vector<std::unique_ptr<Instantiator>> instantiators;
+  for (size_t i = 0; i < eMap.size(); i++)
+  {
+    Trace("e-solver") << "Creating instantiator (" << i << ")..." << std::endl;
+    instantiators.emplace_back(new Instantiator(nm, smtCurr->getLogicInfo()));
+  }
+
+  {
+    SmtScope smts(mainChecker.get());
+
+    Trace("e-solver") << "Abstract formulas" << std::endl;
+    for (const Node& a : abstractAsserts)
+    {
+      Trace("e-solver") << "  " << a << std::endl;
+      mainChecker->assertFormula(a);
+    }
+  }
+
+  size_t numThreads = eMap.size();
+  if (options::numThreads() >= 1)
+  {
+    numThreads =
+        std::min(numThreads, static_cast<size_t>(options::numThreads()));
+  }
+  bool pinning = (eMap.size() == numThreads);
+  Trace("e-solver") << "Actual number of worker threads used: " << numThreads
+                    << std::endl;
+  Trace("e-solver") << "Pinning: " << pinning << std::endl;
+
+  std::vector<std::unique_ptr<Worker>> workerInfos;
+  for (size_t i = 0; i < numThreads; i++)
+  {
+    workerInfos.emplace_back(new Worker(i, nm, smtCurr->getLogicInfo()));
+  }
+
+  SmtScope smts(mainChecker.get());
+
+  for (std::unique_ptr<Worker>& worker : workerInfos)
+  {
+    for (const Node& a : abstractAsserts)
+    {
+      NodeManagerScope nms(worker->d_interNm);
+      worker->d_abstractAssertsBuffer.emplace_back(
+          worker->d_vmMainInter.importNode(a));
+    }
+  }
+
+  size_t i = 0;
+  std::vector<std::pair<Node, std::pair<Node, Node>>> tVars;
+  for (const std::pair<const std::vector<Node>, std::pair<Node, Node>>&
+           mapping : eMap)
+  {
+    Instantiator* instantiator = instantiators[i].get();
+    Node eBody = mapping.second.second;
+
+    std::unordered_set<Node, NodeHashFunction> fvs;
+    expr::getFreeVariables(eBody, fvs);
+
+    std::vector<Node> args;
+    std::vector<TypeNode> argTypes;
+    for (const Node& fv : fvs)
+    {
+      args.emplace_back(fv);
+      argTypes.emplace_back(fv.getType());
+    }
+
+    std::vector<Node> qtVars;
+    const std::vector<Node>& eVars = mapping.first;
+    for (const Node& eVar : eVars)
+    {
+      Node t;
+      if (args.size() > 0)
+      {
+        TypeNode fnt = nm->mkFunctionType(argTypes, eVar.getType());
+        std::vector<Node> largs = {nm->mkSkolem("t", fnt)};
+        largs.insert(largs.end(), args.begin(), args.end());
+        t = nm->mkNode(kind::APPLY_UF, largs);
+      }
+      else
+      {
+        t = nm->mkSkolem("t", eVar.getType());
+      }
+
+      qtVars.emplace_back(t);
+      tVars.emplace_back(std::make_pair(t, std::make_pair(eVar, eBody)));
+    }
+
+    // Each instantiator negates one e-constant
+    Node cube = eBody;
+    instantiator->d_cube = cube;
+    Trace("e-solver") << "Set cube " << cube << std::endl;
+
+    for (const Node& eVar : eVars)
+    {
+      instantiator->d_key.emplace_back(eVar);
+    }
+    instantiator->d_eBody = eBody;
+    /*
+    {
+      NodeManagerScope nms(instantiator->getNodeManager());
+      Node cube = instantiator->d_vm.importNode(eBody).notNode();
+      Trace("e-solver") << "Asserting cube " << cube << std::endl;
+      instantiator->d_smt->assertFormula(cube);
+
+      // TODO: Ugly/unnecessary work
+      for (const Node& eVar : eVars) {
+        instantiator->d_key.emplace_back(instantiator->d_vm.importNode(eVar));
+      }
+    }
+    */
+    i++;
+  }
+
+  Trace("e-solver") << std::endl;
+
+  ThreadPool<Worker, JobOutput> pool(workerInfos, numThreads, pinning);
+
+  CodeTimer eSolverTimer(d_eSolverTime);
+
+  for (std::unique_ptr<Worker>& worker : workerInfos)
+  {
+    worker->d_smt->setOutOfResourcesCallback(
+        [&pool]() { return pool.stopped(); });
+    worker->d_pool = &pool;
+  }
+
+  for (std::unique_ptr<Instantiator>& instantiator : instantiators)
+  {
+    Instantiator* instantiatorPtr = instantiator.get();
+    pool.scheduleTask([instantiatorPtr](Worker* worker) {
+      return refine(worker, instantiatorPtr);
+    });
+  }
+
+  bool recheck = true;
+  std::vector<Node> toAssert;
+  while (true)
+  {
+    if (recheck)
+    {
+      Result r;
+      Trace("e-solver") << "Check assertions... ";
+      {
+        CodeTimer mainSolverTimer(d_mainSolverTime);
+        d_numMainChecks += 1;
+        // mainChecker->setTimeLimit(timeout);
+        r = mainChecker->checkSat();
+      }
+      Trace("e-solver") << r << std::endl;
+      if (r.isSat() == Result::UNSAT)
+      {
+        pool.stop();
+        for (std::unique_ptr<Worker>& worker : workerInfos)
+        {
+          Trace("e-solver") << "Notifying worker to shut down" << std::endl;
+          worker->d_abstractAssertsBufferCv.notify_one();
+        }
+        return r;
+      } /* else if (r.isUnknown()) {
+        timeout *= 2;
+        recheck = true;
+      } */
+      else
+      {
+        recheck = false;
+      }
+    }
+
+    Trace("e-solver") << "Waiting for next result" << std::endl;
+    std::vector<std::pair<size_t, JobOutput>> resv;
+    {
+      CodeTimer mainSolverTimer(d_mainWaitTime);
+      if (!pool.getResult(resv))
+      {
+        break;
+      }
+    }
+
+    d_numRounds += 1;
+    for (std::pair<size_t, JobOutput>& res : resv)
+    {
+      JobOutput& jo = res.second;
+
+      if (jo.d_toAssert.empty())
+      {
+        Trace("e-solver") << "No axioms" << std::endl;
+      }
+      else
+      {
+        // Assert new axioms and share with instantiators
+        for (const Node& a : jo.d_toAssert)
+        {
+          Node axiomInst = jo.d_worker->d_vmMainInter.exportNode(a);
+          if (axiomsSent.find(axiomInst) != axiomsSent.end())
+          {
+            Trace("e-solver")
+                << "Skipping axiom instance: " << axiomInst << std::endl;
+          }
+          else
+          {
+            Trace("e-solver")
+                << "Asserting axiom instance: " << axiomInst << std::endl;
+            recheck = true;
+            d_numAxioms += jo.d_toAssert.size();
+            mainChecker->assertFormula(axiomInst);
+            abstractAsserts.emplace_back(axiomInst);
+            axiomsSent.insert(axiomInst);
+
+            for (std::unique_ptr<Worker>& worker : workerInfos)
+            {
+              std::unique_lock<std::mutex> lock(
+                  worker->d_abstractAssertsBufferMut);
+              NodeManagerScope nms(worker->d_interNm);
+              worker->d_abstractAssertsBuffer.emplace_back(
+                  worker->d_vmMainInter.importNode(axiomInst));
+            }
+          }
+        }
+      }
+
+      jo.clear();
+
+      {
+        std::unique_lock<std::mutex> lock(
+            jo.d_worker->d_abstractAssertsBufferMut);
+        jo.d_worker->d_ready = true;
+      }
+      jo.d_worker->d_abstractAssertsBufferCv.notify_one();
+
+      if (jo.d_done)
+      {
+        Trace("e-solver") << "Instantiator done, not rescheduling" << std::endl;
+      }
+      else
+      {
+        if (pinning)
+        {
+          pool.notifyNextTask(res.first);
+        }
+        else
+        {
+          // If we are not pinning, we have to reschedule
+          Instantiator* instantiatorPtr = jo.d_instantiator;
+          // Schedule instantiator again
+          pool.scheduleTask([instantiatorPtr](Worker* worker) {
+            return refine(worker, instantiatorPtr);
+          });
+        }
+      }
+    }
+
+    Trace("e-solver") << std::endl;
+  }
+
+  Result r(Result::SAT_UNKNOWN, Result::INCOMPLETE);
+  return r;
+}
+
+Node ESolver::abstract(Node n,
+                       std::unordered_map<Node, Node, NodeHashFunction>& cache,
+                       std::map<std::vector<Node>, std::pair<Node, Node>>& eMap)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> toVisit{n};
+  while (!toVisit.empty())
+  {
+    Node curr = toVisit.back();
+    toVisit.pop_back();
+
+    if (cache.find(curr) != cache.end())
+    {
+      Node result = cache[curr];
+      if (result.isNull())
+      {
+        Node newNode;
+        if (curr.getKind() == kind::FORALL || curr.getKind() == kind::EXISTS)
+        {
+          bool negate = curr.getKind() == kind::FORALL;
+          Node bvl = curr[0];
+          Node newBody = cache[curr[1]];
+
+          std::unordered_set<Node, NodeHashFunction> fvs;
+          expr::getFreeVariables(curr, fvs);
+
+          std::vector<Node> args;
+          std::vector<TypeNode> argTypes;
+          for (const Node& fv : fvs)
+          {
+            args.emplace_back(fv);
+            argTypes.emplace_back(fv.getType());
+          }
+
+          std::vector<Node> es;
+          for (Node var : bvl)
+          {
+            Node e;
+            if (args.size() > 0)
+            {
+              TypeNode fnt = nm->mkFunctionType(argTypes, var.getType());
+              std::vector<Node> largs = {nm->mkSkolem("l", fnt)};
+              largs.insert(largs.end(), args.begin(), args.end());
+              e = nm->mkNode(kind::APPLY_UF, largs);
+            }
+            else
+            {
+              e = nm->mkSkolem("l", var.getType());
+            }
+            es.emplace_back(e);
+            newBody = newBody.substitute(TNode(var), TNode(e));
+            // TODO: Ugly and inefficient
+            for (std::pair<const std::vector<Node>, std::pair<Node, Node>>&
+                     mapping : eMap)
+            {
+              mapping.second = std::make_pair(
+                  mapping.second.first,
+                  mapping.second.second.substitute(TNode(var), TNode(e)));
+            }
+          }
+
+          eMap[es] =
+              std::make_pair(es[0], negate ? newBody.notNode() : newBody);
+          cache[curr] = newBody;
+        }
+        else
+        {
+          NodeBuilder<> nb(curr.getKind());
+          if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+          {
+            nb << cache[curr.getOperator()];
+          }
+          for (const Node& currc : curr)
+          {
+            nb << cache[currc];
+          }
+          cache[curr] = nb;
+        }
+      }
+      continue;
+    }
+    else if (curr.getNumChildren() == 0)
+    {
+      cache[curr] = curr;
+      continue;
+    }
+
+    cache[curr] = Node::null();
+    toVisit.emplace_back(curr);
+    if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      toVisit.push_back(curr.getOperator());
+    }
+    toVisit.insert(toVisit.end(), curr.begin(), curr.end());
+  }
+
+  return cache[n];
+}
+
+Node mapConsts(Node n, std::unordered_map<Node, Node, NodeHashFunction>& cache)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> toVisit{n};
+  while (!toVisit.empty())
+  {
+    Node curr = toVisit.back();
+    toVisit.pop_back();
+
+    if (cache.find(curr) != cache.end())
+    {
+      Node result = cache[curr];
+      if (!result.isNull())
+      {
+        continue;
+      }
+
+      if (curr.getKind() == kind::UNINTERPRETED_CONSTANT)
+      {
+        Node c = nm->mkSkolem("uc", curr.getType());
+        cache[curr] = c;
+      }
+      else if (curr.getNumChildren() == 0)
+      {
+        cache[curr] = curr;
+      }
+      else
+      {
+        NodeBuilder<> nb(curr.getKind());
+        if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+        {
+          nb << cache[curr.getOperator()];
+        }
+        for (const Node& currc : curr)
+        {
+          nb << cache[currc];
+        }
+        cache[curr] = nb;
+      }
+      continue;
+    }
+
+    cache[curr] = Node::null();
+    toVisit.emplace_back(curr);
+    if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      toVisit.push_back(curr.getOperator());
+    }
+    toVisit.insert(toVisit.end(), curr.begin(), curr.end());
+  }
+
+  return cache[n];
+}
+
+void ESolver::apps(Node f, Node n, std::vector<Node>& result)
+{
+  std::unordered_set<Node, NodeHashFunction> visited;
+  std::vector<Node> toVisit{n};
+  while (!toVisit.empty())
+  {
+    Node curr = toVisit.back();
+    toVisit.pop_back();
+
+    if (visited.find(curr) != visited.end())
+    {
+      continue;
+    }
+    visited.insert(curr);
+
+    if (curr.getKind() == kind::APPLY_UF && curr.getOperator() == f)
+    {
+      result.emplace_back(curr);
+    }
+
+    toVisit.emplace_back(curr);
+    if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      toVisit.push_back(curr.getOperator());
+    }
+    toVisit.insert(toVisit.end(), curr.begin(), curr.end());
+  }
+}
+
+bool ESolver::hasTVar(Node t, Node n)
+{
+  std::unordered_set<Node, NodeHashFunction> visited;
+  std::vector<Node> toVisit{n};
+  while (!toVisit.empty())
+  {
+    Node curr = toVisit.back();
+    toVisit.pop_back();
+
+    if (visited.find(curr) != visited.end())
+    {
+      continue;
+    }
+    visited.insert(curr);
+
+    if (curr == t)
+    {
+      return true;
+    }
+
+    toVisit.emplace_back(curr);
+    if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      toVisit.push_back(curr.getOperator());
+    }
+    toVisit.insert(toVisit.end(), curr.begin(), curr.end());
+  }
+
+  return false;
+}
+
+Node additionalLemmas(Node inst)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  VirtualTermSkolemAttribute vtsa;
+  std::unordered_set<Node, NodeHashFunction> visited;
+  std::vector<Node> toVisit{inst};
+  Node lemmas = nm->mkConst(true);
+  while (!toVisit.empty())
+  {
+    Node curr = toVisit.back();
+    toVisit.pop_back();
+
+    if (visited.find(curr) != visited.end())
+    {
+      continue;
+    }
+    visited.insert(curr);
+
+    if (curr.getKind() == kind::SKOLEM)
+    {
+      if (curr.getAttribute(vtsa))
+      {
+        lemmas =
+            nm->mkNode(kind::AND,
+                       lemmas,
+                       nm->mkNode(kind::GT, curr, nm->mkConst(Rational(0))));
+      }
+    }
+
+    toVisit.emplace_back(curr);
+    if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      toVisit.push_back(curr.getOperator());
+    }
+    toVisit.insert(toVisit.end(), curr.begin(), curr.end());
+  }
+  return lemmas;
+}
+
+Node collapseQuantifiers(Node f)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<Node, Node, NodeHashFunction> results;
+  std::vector<Node> toVisit{f};
+  while (!toVisit.empty())
+  {
+    Node curr = toVisit.back();
+    toVisit.pop_back();
+
+    if (results.find(curr) != results.end())
+    {
+      Node result = results[curr];
+      if (result.isNull())
+      {
+        Node newNode;
+        if ((curr.getKind() == kind::FORALL || curr.getKind() == kind::EXISTS)
+            && curr.getKind() == curr[1].getKind())
+        {
+          std::vector<Node> bvs;
+          bvs.insert(bvs.end(), curr[0].begin(), curr[0].end());
+          bvs.insert(bvs.end(), curr[1][0].begin(), curr[1][0].end());
+          results[curr] = nm->mkNode(curr.getKind(),
+                                     nm->mkNode(kind::BOUND_VAR_LIST, bvs),
+                                     curr[1][1]);
+        }
+        else
+        {
+          NodeBuilder<> nb(curr.getKind());
+          if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+          {
+            nb << results[curr.getOperator()];
+          }
+          for (const Node& currc : curr)
+          {
+            nb << results[currc];
+          }
+          results[curr] = nb;
+        }
+      }
+      continue;
+    }
+    else if (curr.getNumChildren() == 0)
+    {
+      results[curr] = curr;
+      continue;
+    }
+
+    results[curr] = Node::null();
+    toVisit.emplace_back(curr);
+    if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      toVisit.push_back(curr.getOperator());
+    }
+    toVisit.insert(toVisit.end(), curr.begin(), curr.end());
+  }
+
+  return results[f];
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/e_solver/e_solver.h b/src/smt/e_solver/e_solver.h
new file mode 100644
index 000000000..874a7f045
--- /dev/null
+++ b/src/smt/e_solver/e_solver.h
@@ -0,0 +1,84 @@
+/*********************                                                        */
+/*! \file e_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 A CEGAR solver for quantifiers
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__E_SOLVER__E_SOLVER_H
+#define CVC4__SMT__E_SOLVER__E_SOLVER_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "smt/assertions.h"
+#include "smt/smt_engine_state.h"
+#include "util/result.h"
+
+namespace CVC4 {
+namespace smt {
+
+class ESolver
+{
+ public:
+  ESolver(SmtEngine* parent, SmtEngineState* state);
+  ~ESolver();
+
+  /** Check satisfiability using the e-solver */
+  Result checkSatisfiability(Assertions& asserts);
+
+ private:
+  /** Check if the formula f is satisfiable */
+  Result isUnsat(Node f);
+
+  /**
+   * Abstract the original formula. This method removes quantifiers and
+   * replaces bound variables with fresh constants that represent abstracted
+   * e-terms.
+   *
+   * @param n Node to abstract
+   * @param cache A cache that maps terms to their abstractions
+   * @param eMap Maps abstracted literals to the e-term bodies
+   * @return The abstracted version of n
+   */
+  Node abstract(Node n,
+                std::unordered_map<Node, Node, NodeHashFunction>& cache,
+                std::map<std::vector<Node>, std::pair<Node, Node>>& eMap);
+
+  void apps(Node f, Node n, std::vector<Node>& result);
+
+  bool hasTVar(Node t, Node n);
+
+  /** The parent SMT engine */
+  SmtEngine* d_parent;
+  SmtEngineState* d_state;
+
+  TimerStat d_eSolverTime;
+  TimerStat d_mainSolverTime;
+  TimerStat d_mainWaitTime;
+  IntStat d_numMainChecks;
+  IntStat d_numAxioms;
+  IntStat d_numRounds;
+};
+
+Node mapConsts(Node n, std::unordered_map<Node, Node, NodeHashFunction>& cache);
+
+/** Combines nested quantifiers */
+Node collapseQuantifiers(Node f);
+Node additionalLemmas(Node inst);
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__E_SOLVER_H */
diff --git a/src/smt/e_solver/thread_pool.h b/src/smt/e_solver/thread_pool.h
new file mode 100644
index 000000000..04e8b25b3
--- /dev/null
+++ b/src/smt/e_solver/thread_pool.h
@@ -0,0 +1,194 @@
+/*********************                                                        */
+/*! \file thread_pool.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 An implementation of a thread pool
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__E_SOLVER__THREAD_POOL_H
+#define CVC4__SMT__E_SOLVER__THREAD_POOL_H
+
+#include <condition_variable>
+#include <future>
+#include <mutex>
+#include <queue>
+#include <thread>
+#include <unordered_map>
+
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "smt/assertions.h"
+#include "smt/smt_engine_state.h"
+#include "util/result.h"
+
+namespace CVC4 {
+namespace smt {
+
+template <class W, class R>
+class ThreadPool
+{
+ public:
+  ThreadPool(std::vector<std::unique_ptr<W>>& workerInfos,
+             ssize_t threads,
+             bool pinning)
+      : d_workerInfos(workerInfos),
+        d_stop(false),
+        d_pinning(pinning),
+        d_process(-1)
+  {
+    for (ssize_t i = 0; i < threads; ++i)
+    {
+      d_workers.emplace_back([this, i, &workerInfos] {
+        std::function<std::pair<bool, R>(W*)> task;
+        bool fetchTask = true;
+        for (;;)
+        {
+          if (fetchTask)
+          {
+            std::unique_lock<std::mutex> lock(this->d_queueMutex);
+            this->d_cv.wait(lock, [this] {
+              return this->d_stop || !this->d_tasks.empty();
+            });
+            if (this->d_stop)
+            {
+              Trace("e-solver") << "Shutting down thread" << std::endl;
+              break;
+            }
+            task = std::move(this->d_tasks.front());
+            this->d_tasks.pop();
+
+            if (this->d_pinning)
+            {
+              // If we are using pinning, we just execute the same task over and
+              // over again
+              fetchTask = false;
+            }
+          }
+          else
+          {
+            std::unique_lock<std::mutex> lock(this->d_queueMutex);
+            this->d_cv.wait(lock, [this, i] {
+              return this->d_stop || this->d_process == i;
+            });
+            this->d_process = -1;
+            if (this->d_stop)
+            {
+              break;
+            }
+          }
+
+          std::pair<bool, R> res = task(workerInfos[i].get());
+          if (this->d_pinning && res.first)
+          {
+            // Exit if this thread has no more work to do and pinning is
+            // enabled
+            break;
+          }
+          else
+          {
+            std::unique_lock<std::mutex> lock(this->d_resultsMut);
+            d_results.emplace(std::make_pair(i, res.second));
+            // Clear object while holding the lock to make sure that the
+            // NodeManager is not used simultaneously to delete the result and
+            // to copy the result to the main thread.
+            res.second.clear();
+          }
+          d_cvResults.notify_one();
+        }
+      });
+    }
+  }
+
+  ~ThreadPool()
+  {
+    Trace("e-solver") << "Shutting down thread pool" << std::endl;
+    {
+      std::unique_lock<std::mutex> lock(d_queueMutex);
+      d_stop = true;
+    }
+    d_cv.notify_all();
+    for (std::thread& worker : d_workers)
+    {
+      worker.join();
+    }
+    Trace("e-solver") << "Joined all threads" << std::endl;
+  }
+
+  void stop()
+  {
+    std::unique_lock<std::mutex> lock(d_queueMutex);
+    d_stop = true;
+  }
+
+  bool stopped() { return d_stop; }
+
+  void scheduleTask(std::function<std::pair<bool, R>(W*)>&& f)
+  {
+    {
+      std::unique_lock<std::mutex> lock(d_queueMutex);
+      if (d_stop) throw std::runtime_error("enqueue on stopped ThreadPool");
+      d_tasks.emplace(f);
+    }
+    d_cv.notify_one();
+  }
+
+  void notifyNextTask(size_t hint)
+  {
+    {
+      std::unique_lock<std::mutex> lock(d_queueMutex);
+      d_process = hint;
+    }
+    d_cv.notify_all();
+  }
+
+  bool getResult(std::vector<std::pair<size_t, R>>& out)
+  {
+    {
+      std::unique_lock<std::mutex> lock(this->d_resultsMut);
+      this->d_cvResults.wait(
+          lock, [this] { return this->d_stop || !this->d_results.empty(); });
+      if (this->d_stop)
+      {
+        return false;
+      }
+      Trace("e-solver") << "Number of results " << d_results.size()
+                        << std::endl;
+      while (!d_results.empty())
+      {
+        out.emplace_back(d_results.front());
+        d_results.pop();
+      }
+    }
+    return true;
+  }
+
+ private:
+  std::vector<std::thread> d_workers;
+  std::vector<std::unique_ptr<W>>& d_workerInfos;
+  std::queue<std::function<std::pair<bool, R>(W*)>> d_tasks;
+  std::queue<std::pair<size_t, R>> d_results;
+
+  std::mutex d_queueMutex;
+  std::condition_variable d_cv;
+
+  std::mutex d_resultsMut;
+  std::condition_variable d_cvResults;
+
+  bool d_stop;
+  bool d_pinning;
+  ssize_t d_process;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/e_solver/var_map.h b/src/smt/e_solver/var_map.h
new file mode 100644
index 000000000..bc494d05e
--- /dev/null
+++ b/src/smt/e_solver/var_map.h
@@ -0,0 +1,471 @@
+/*********************                                                        */
+/*! \file var_map.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Mapping of variables between two NodeManagers
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__E_SOLVER__VAR_MAP_H
+#define CVC4__SMT__E_SOLVER__VAR_MAP_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+
+namespace CVC4 {
+namespace smt {
+
+class VarMap
+{
+ public:
+  VarMap(NodeManager* nm1, NodeManager* nm2) : d_nm1(nm1), d_nm2(nm2) {}
+  ~VarMap()
+  {
+    {
+      NodeManagerScope nms(d_nm1);
+      for (std::pair<const TypeNode, TypeNode>& kv : d_revTypeMap)
+      {
+        d_revTypeMap[kv.first] = TypeNode::null();
+      }
+    }
+    {
+      NodeManagerScope nms(d_nm2);
+      for (std::pair<const TypeNode, TypeNode>& kv : d_typeMap)
+      {
+        d_typeMap[kv.first] = TypeNode::null();
+      }
+    }
+    {
+      NodeManagerScope nms(d_nm1);
+      d_map.clear();
+      d_typeMap.clear();
+      d_keepAliveFrom.clear();
+    }
+    {
+      NodeManagerScope nms(d_nm2);
+      d_revMap.clear();
+      d_revTypeMap.clear();
+      d_keepAliveTo.clear();
+    }
+  }
+
+  Node importNode(TNode n)
+  {
+    return exportNodeInternal(d_nm1,
+                              d_nm2,
+                              n,
+                              d_map,
+                              d_revMap,
+                              d_typeMap,
+                              d_revTypeMap,
+                              d_keepAliveTo);
+  }
+
+  Node exportNode(TNode n)
+  {
+    return exportNodeInternal(d_nm2,
+                              d_nm1,
+                              n,
+                              d_revMap,
+                              d_map,
+                              d_revTypeMap,
+                              d_typeMap,
+                              d_keepAliveFrom);
+  }
+
+  Node exportNodeInternal(
+      NodeManager* from,
+      NodeManager* to,
+      TNode n,
+      std::unordered_map<TNode, TNode, TNodeHashFunction>& nodeMap,
+      std::unordered_map<TNode, TNode, TNodeHashFunction>& revNodeMap,
+      std::unordered_map<TypeNode, TypeNode, TypeNodeHashFunction>& typeNodeMap,
+      std::unordered_map<TypeNode, TypeNode, TypeNodeHashFunction>&
+          revTypeNodeMap,
+      std::vector<Node>& keepAlive)
+  {
+    NodeManagerScope nmsTo(to);
+    std::unordered_map<TNode, Node, TNodeHashFunction> result;
+    std::vector<TNode> toVisit{n};
+
+    while (!toVisit.empty())
+    {
+      TNode curr = toVisit.back();
+      toVisit.pop_back();
+
+      if (result.find(curr) != result.end())
+      {
+        if (!result[curr].isNull())
+        {
+          continue;
+        }
+
+        if (nodeMap.find(curr) != nodeMap.end())
+        {
+          result[curr] = nodeMap[curr];
+        }
+        else if (curr.getNumChildren() == 0)
+        {
+          if (curr.getKind() == kind::SKOLEM
+              || curr.getKind() == kind::VARIABLE)
+          {
+            TypeNode tn;
+            TypeNode ctn;
+            {
+              NodeManagerScope nmsFrom(from);
+              ctn = curr.getType();
+            }
+            {
+              NodeManagerScope nmsFrom(to);
+              tn = exportTypeNode(from, to, ctn, typeNodeMap, revTypeNodeMap);
+            }
+            std::stringstream ss;
+            {
+              NodeManagerScope nmsFrom(from);
+              ss << "_" << curr;
+            }
+            Node sk = to->mkSkolem(ss.str(), tn);
+            result[curr] = sk;
+            nodeMap[curr] = sk;
+            revNodeMap[sk] = curr;
+
+            keepAlive.emplace_back(sk);
+          }
+          else if (curr.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+          {
+            Node sk = to->mkBooleanTermVariable();
+            result[curr] = sk;
+            nodeMap[curr] = sk;
+            revNodeMap[sk] = curr;
+
+            keepAlive.emplace_back(sk);
+          }
+          else if (curr.getKind() == kind::BOUND_VARIABLE)
+          {
+            TypeNode tn;
+            TypeNode ctn;
+            {
+              NodeManagerScope nmsFrom(from);
+              ctn = curr.getType();
+            }
+            {
+              NodeManagerScope nmsFrom(to);
+              tn = exportTypeNode(from, to, ctn, typeNodeMap, revTypeNodeMap);
+            }
+            std::stringstream ss;
+            {
+              NodeManagerScope nmsFrom(from);
+              ss << "_" << curr;
+            }
+            Node sk = to->mkBoundVar(ss.str(), tn);
+            result[curr] = sk;
+            nodeMap[curr] = sk;
+            revNodeMap[sk] = curr;
+
+            keepAlive.emplace_back(sk);
+          }
+          else if (curr.isConst())
+          {
+            switch (curr.getKind())
+            {
+              case kind::UNINTERPRETED_CONSTANT:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::UninterpretedConstant>());
+                break;
+              case kind::ABSTRACT_VALUE:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::AbstractValue>());
+                break;
+              case kind::BUILTIN:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::Kind>());
+                break;
+              case kind::TYPE_CONSTANT:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::TypeConstant>());
+                break;
+              case kind::CONST_BOOLEAN:
+                result[curr] = to->mkConst(curr.getConst<bool>());
+                break;
+              case kind::DIVISIBLE_OP:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::Divisible>());
+                break;
+              case kind::CONST_RATIONAL:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::Rational>());
+                break;
+              case kind::IAND_OP:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::IntAnd>());
+                break;
+              case kind::BITVECTOR_TYPE:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::BitVectorSize>());
+                break;
+              case kind::CONST_BITVECTOR:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::BitVector>());
+                break;
+              case kind::BITVECTOR_BITOF_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::BitVectorBitOf>());
+                break;
+              case kind::BITVECTOR_EXTRACT_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::BitVectorExtract>());
+                break;
+              case kind::BITVECTOR_REPEAT_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::BitVectorRepeat>());
+                break;
+              case kind::BITVECTOR_ROTATE_LEFT_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::BitVectorRotateLeft>());
+                break;
+              case kind::BITVECTOR_ROTATE_RIGHT_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::BitVectorRotateRight>());
+                break;
+              case kind::BITVECTOR_SIGN_EXTEND_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::BitVectorSignExtend>());
+                break;
+              case kind::BITVECTOR_ZERO_EXTEND_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::BitVectorZeroExtend>());
+                break;
+              case kind::INT_TO_BITVECTOR_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::IntToBitVector>());
+                break;
+              case kind::CONST_FLOATINGPOINT:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::FloatingPoint>());
+                break;
+              case kind::CONST_ROUNDINGMODE:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::RoundingMode>());
+                break;
+              case kind::FLOATINGPOINT_TYPE:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::FloatingPointSize>());
+                break;
+              case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
+                result[curr] = to->mkConst(
+                    curr.getConst<::CVC4::FloatingPointToFPIEEEBitVector>());
+                break;
+              case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
+                result[curr] = to->mkConst(
+                    curr.getConst<::CVC4::FloatingPointToFPFloatingPoint>());
+                break;
+              case kind::FLOATINGPOINT_TO_FP_REAL_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::FloatingPointToFPReal>());
+                break;
+              case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
+                result[curr] = to->mkConst(
+                    curr.getConst<::CVC4::FloatingPointToFPSignedBitVector>());
+                break;
+              case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<
+                                ::CVC4::FloatingPointToFPUnsignedBitVector>());
+                break;
+              case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
+                result[curr] = to->mkConst(
+                    curr.getConst<::CVC4::FloatingPointToFPGeneric>());
+                break;
+              case kind::FLOATINGPOINT_TO_UBV_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::FloatingPointToUBV>());
+                break;
+              case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
+                result[curr] = to->mkConst(
+                    curr.getConst<::CVC4::FloatingPointToUBVTotal>());
+                break;
+              case kind::FLOATINGPOINT_TO_SBV_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::FloatingPointToSBV>());
+                break;
+              case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
+                result[curr] = to->mkConst(
+                    curr.getConst<::CVC4::FloatingPointToSBVTotal>());
+                break;
+              case kind::STORE_ALL:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::ArrayStoreAll>());
+                break;
+              case kind::DATATYPE_TYPE:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::DatatypeIndexConstant>());
+                break;
+              case kind::ASCRIPTION_TYPE:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::AscriptionType>());
+                break;
+              case kind::TUPLE_UPDATE_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::TupleUpdate>());
+                break;
+              case kind::RECORD_UPDATE_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::RecordUpdate>());
+                break;
+              case kind::EMPTYSET:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::EmptySet>());
+                break;
+              case kind::SINGLETON_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::SingletonOp>());
+                break;
+              case kind::EMPTYBAG:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::EmptyBag>());
+                break;
+              case kind::MK_BAG_OP:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::MakeBagOp>());
+                break;
+              case kind::CONST_STRING:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::String>());
+                break;
+              case kind::CONST_SEQUENCE:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::Sequence>());
+                break;
+              case kind::REGEXP_REPEAT_OP:
+                result[curr] =
+                    to->mkConst(curr.getConst<::CVC4::RegExpRepeat>());
+                break;
+              case kind::REGEXP_LOOP_OP:
+                result[curr] = to->mkConst(curr.getConst<::CVC4::RegExpLoop>());
+                break;
+
+              default: Unhandled() << "not implemented: " << curr.getKind();
+            }
+          }
+        }
+        else
+        {
+          NodeManagerScope nms(to);
+          NodeBuilder<> nb(curr.getKind());
+          if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+          {
+            nb << result[curr.getOperator()];
+          }
+          for (const TNode& currc : curr)
+          {
+            nb << result[currc];
+          }
+          result[curr] = nb;
+        }
+
+        continue;
+      }
+
+      {
+        NodeManagerScope nms(to);
+        result[curr] = Node::null();
+      }
+      toVisit.emplace_back(curr);
+      if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        // XXX: This is a very ugly hack to get the operator as a TNode
+        toVisit.emplace_back(curr[-1]);  //.getOperator());
+      }
+      toVisit.insert(toVisit.end(), curr.begin(), curr.end());
+    }
+
+    return result[n];
+  }
+
+  TypeNode exportTypeNode(
+      NodeManager* from,
+      NodeManager* to,
+      TypeNode tn,
+      std::unordered_map<TypeNode, TypeNode, TypeNodeHashFunction>& typeNodeMap,
+      std::unordered_map<TypeNode, TypeNode, TypeNodeHashFunction>&
+          revTypeNodeMap)
+  {
+    if (theory::kindToTheoryId(tn.getKind()) == theory::THEORY_DATATYPES)
+    {
+      Unimplemented() << "Cannot export datatypes";
+    }
+    if (tn.getMetaKind() == kind::metakind::PARAMETERIZED
+        && tn.getKind() != kind::SORT_TYPE)
+    {
+      Unimplemented() << "Cannot export parametrized types";
+    }
+    if (tn.getKind() == kind::TYPE_CONSTANT)
+    {
+      return to->mkTypeConst(tn.getConst<TypeConstant>());
+    }
+    else if (tn.getKind() == kind::BITVECTOR_TYPE)
+    {
+      return to->mkBitVectorType(tn.getConst<BitVectorSize>());
+    }
+    else if (tn.getKind() == kind::FLOATINGPOINT_TYPE)
+    {
+      return to->mkFloatingPointType(tn.getConst<FloatingPointSize>());
+    }
+    else if (tn.getKind() == kind::FLOATINGPOINT_TYPE)
+    {
+      return to->mkFloatingPointType(tn.getConst<FloatingPointSize>());
+    }
+    else if (tn.getKind() == kind::FUNCTION_TYPE)
+    {
+      TypeNode range = exportTypeNode(
+          from, to, tn.getRangeType(), typeNodeMap, revTypeNodeMap);
+      std::vector<TypeNode> args;
+      for (const TypeNode& tnn : tn.getArgTypes())
+      {
+        args.emplace_back(
+            exportTypeNode(from, to, tnn, typeNodeMap, revTypeNodeMap));
+      }
+      NodeManagerScope nms(to);
+      TypeNode res = to->mkFunctionType(args, range);
+      return res;
+    }
+    else if (tn.getNumChildren() == 0)
+    {
+      if (tn.getKind() == kind::SORT_TYPE)
+      {
+        if (typeNodeMap.find(tn) == typeNodeMap.end())
+        {
+          std::stringstream ss;
+          {
+            NodeManagerScope nms(from);
+            ss << "_";
+            ss << tn;
+          }
+          NodeManagerScope nms(to);
+          TypeNode sort = to->mkSort(ss.str());
+          typeNodeMap[tn] = sort;
+          revTypeNodeMap[sort] = tn;
+        }
+        return typeNodeMap[tn];
+      }
+      Unimplemented() << "Cannot export 0-arity " << tn;
+    }
+    Unimplemented() << "Cannot export " << tn;
+  }
+
+ private:
+  NodeManager* d_nm1;
+  NodeManager* d_nm2;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> d_map;
+  std::unordered_map<TNode, TNode, TNodeHashFunction> d_revMap;
+  std::unordered_map<TypeNode, TypeNode, TypeNodeHashFunction> d_typeMap;
+  std::unordered_map<TypeNode, TypeNode, TypeNodeHashFunction> d_revTypeMap;
+  std::vector<Node> d_keepAliveTo;
+  std::vector<Node> d_keepAliveFrom;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/e_solver/worker.cpp b/src/smt/e_solver/worker.cpp
new file mode 100644
index 000000000..49eedbda5
--- /dev/null
+++ b/src/smt/e_solver/worker.cpp
@@ -0,0 +1,68 @@
+/*********************                                                        */
+/*! \file worker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 A CEGAR solver for quantifiers
+ **/
+
+#include "smt/e_solver/worker.h"
+
+namespace CVC4 {
+namespace smt {
+
+JobOutput::JobOutput()
+    : d_worker(nullptr), d_instantiator(nullptr), d_toAssert({}), d_done(true)
+{
+}
+
+JobOutput::JobOutput(Worker* worker,
+                     Instantiator* instantiator,
+                     const std::vector<Node>& toAssert,
+                     bool done)
+    : d_worker(worker), d_instantiator(instantiator), d_done(done)
+{
+  std::unique_lock<std::mutex> lock(d_worker->d_abstractAssertsBufferMut);
+  d_worker->d_ready = false;
+
+  NodeManagerScope nms(d_worker->d_interNm);
+  for (const Node& n : toAssert)
+  {
+    d_toAssert.emplace_back(d_worker->d_vmInterWorker.exportNode(n));
+  }
+}
+
+JobOutput::JobOutput(const JobOutput& other)
+    : d_worker(other.d_worker), d_instantiator(other.d_instantiator)
+{
+  NodeManagerScope nms(d_worker->d_interNm);
+  d_toAssert = other.d_toAssert;
+  d_done = other.d_done;
+}
+
+JobOutput& JobOutput::operator=(const JobOutput& other)
+{
+  d_worker = other.d_worker;
+  d_instantiator = other.d_instantiator;
+  NodeManagerScope nms(d_worker->d_interNm);
+  d_toAssert = other.d_toAssert;
+  d_done = other.d_done;
+  return *this;
+}
+
+void JobOutput::clear()
+{
+  NodeManagerScope nms(d_worker->d_interNm);
+  d_toAssert.clear();
+}
+
+JobOutput::~JobOutput() { clear(); }
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/e_solver/worker.h b/src/smt/e_solver/worker.h
new file mode 100644
index 000000000..b748a1d93
--- /dev/null
+++ b/src/smt/e_solver/worker.h
@@ -0,0 +1,165 @@
+/*********************                                                        */
+/*! \file worker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 A CEGAR solver for quantifiers
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__E_SOLVER__WORKER_H
+#define CVC4__SMT__E_SOLVER__WORKER_H
+
+#include <unordered_map>
+
+#include "expr/expr_manager.h"
+#include "expr/node.h"
+#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "smt/e_solver/thread_pool.h"
+#include "smt/e_solver/var_map.h"
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+namespace smt {
+
+struct Worker;
+
+struct JobOutput
+{
+  Worker* d_worker;
+  Instantiator* d_instantiator;
+  std::vector<Node> d_toAssert;
+  bool d_done;
+
+  JobOutput();
+
+  JobOutput(Worker* worker,
+            Instantiator* instantiator,
+            const std::vector<Node>& toAssert,
+            bool done);
+  JobOutput(const JobOutput& other);
+  JobOutput& operator=(const JobOutput& other);
+
+  void clear();
+
+  ~JobOutput();
+};
+
+struct Worker
+{
+  Worker(size_t id, NodeManager* mainNm, const LogicInfo& logic)
+      : d_pool(nullptr),
+        d_id(id),
+        d_mainNm(mainNm),
+        d_logic(logic),
+        d_em(new ExprManager()),
+        d_interEm(new ExprManager()),
+        d_interNm(d_interEm->getNodeManager()),
+        d_smt(new SmtEngine(d_em->getNodeManager())),
+        d_vmMainInter(d_mainNm, d_interNm),
+        d_vmInterWorker(d_interNm, d_em->getNodeManager()),
+        d_timeout(1000),
+        d_ready(true)
+  {
+    initSolver();
+  }
+
+  ~Worker()
+  {
+    {
+      NodeManagerScope nms(d_interNm);
+      d_abstractAssertsBuffer.clear();
+    }
+
+    NodeManagerScope nms(getNodeManager());
+    d_abstractAsserts.clear();
+  }
+
+  void initSolver()
+  {
+    d_smt->setIsInternalSubsolver();
+    d_smt->setLogic(d_logic);
+    d_smt->getOptions().set(options::produceModels, true);
+    d_smt->getOptions().set(options::fullSaturateQuant, true);
+  }
+
+  NodeManager* getNodeManager() { return d_em->getNodeManager(); }
+
+  void getLiterals(std::unordered_set<Node, NodeHashFunction>& literals, Node n)
+  {
+    std::unordered_set<Node, NodeHashFunction> visited;
+    std::vector<Node> toVisit{n};
+    while (!toVisit.empty())
+    {
+      Node curr = toVisit.back();
+      toVisit.pop_back();
+
+      if (visited.find(curr) != visited.end())
+      {
+        continue;
+      }
+      visited.insert(curr);
+
+      if (curr.getType().isBoolean()
+          && (curr.getNumChildren() == 0 || !curr[0].getType().isBoolean()))
+      {
+        Trace("e-solver-debug") << "Get value of " << curr << std::endl;
+        Node val = d_smt->getValue(curr);
+        literals.insert(val.getConst<bool>() ? curr : curr.notNode());
+        continue;
+      }
+
+      toVisit.emplace_back(curr);
+      if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        toVisit.push_back(curr.getOperator());
+      }
+      toVisit.insert(toVisit.end(), curr.begin(), curr.end());
+    }
+  }
+
+  void reinit()
+  {
+    // d_timeout *= 2;
+    d_smt.reset(new SmtEngine(getNodeManager()));
+    initSolver();
+
+    for (const Node& a : d_abstractAsserts)
+    {
+      d_smt->assertFormula(a);
+    }
+
+    d_smt->setOutOfResourcesCallback(
+        [this]() { return this->d_pool->stopped(); });
+  }
+
+  ThreadPool<Worker, JobOutput>* d_pool;
+  size_t d_id;
+  NodeManager* d_mainNm;
+  LogicInfo d_logic;
+  std::unique_ptr<ExprManager> d_em;
+  std::unique_ptr<ExprManager> d_interEm;
+  NodeManager* d_interNm;
+  std::unique_ptr<SmtEngine> d_smt;
+  std::vector<Node> d_abstractAsserts;
+  std::mutex d_abstractAssertsBufferMut;
+  std::condition_variable d_abstractAssertsBufferCv;
+  std::vector<Node> d_abstractAssertsBuffer;
+  VarMap d_vmMainInter;
+  VarMap d_vmInterWorker;
+  unsigned long d_timeout;
+  bool d_ready;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 26f5745ca..f1ca7b204 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -214,6 +214,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
 
+  if (options::eSolver())
+  {
+    logic = logic.getUnlockedCopy();
+    logic.enableTheory(THEORY_UF);
+    logic.lock();
+  }
+
   // --ite-simp is an experimental option designed for QF_LIA/nec. This
   // technique is experimental. This benchmark set also requires removing ITEs
   // during preprocessing, before repeating simplification. Hence, we enable
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 09d54d6d8..ffdefda45 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -38,6 +38,7 @@
 #include "smt/check_models.h"
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
+#include "smt/e_solver/e_solver.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
 #include "smt/logic_request.h"
@@ -289,6 +290,11 @@ void SmtEngine::finishInit()
     d_interpolSolver.reset(new InterpolationSolver(this));
   }
 
+  if (options::eSolver())
+  {
+    d_eSolver.reset(new ESolver(this, d_state.get()));
+  }
+
   d_pp->finishInit();
 
   AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
@@ -344,6 +350,7 @@ SmtEngine::~SmtEngine()
     d_model.reset(nullptr);
 
     d_sygusSolver.reset(nullptr);
+    d_eSolver.reset(nullptr);
 
     d_smtSolver.reset(nullptr);
 
@@ -965,8 +972,19 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
                  << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
                  << assumptions << ")" << endl;
     // check the satisfiability with the solver object
-    Result r = d_smtSolver->checkSatisfiability(
-        *d_asserts.get(), assumptions, inUnsatCore, isEntailmentCheck);
+    Result r;
+
+    if (d_eSolver == nullptr)
+    {
+      r = d_smtSolver->checkSatisfiability(
+          *d_asserts.get(), assumptions, inUnsatCore, isEntailmentCheck);
+    }
+    else
+    {
+      AlwaysAssert(assumptions.size() == 0);
+      AlwaysAssert(!isEntailmentCheck);
+      r = d_eSolver->checkSatisfiability(*d_asserts.get());
+    }
 
     Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
                  << "(" << assumptions << ") => " << r << endl;
@@ -1856,6 +1874,11 @@ void SmtEngine::setTimeLimit(unsigned long milis)
   d_resourceManager->setTimeLimit(milis);
 }
 
+void SmtEngine::setOutOfResourcesCallback(std::function<bool()>&& f)
+{
+  d_resourceManager->setCallback(std::move(f));
+}
+
 unsigned long SmtEngine::getResourceUsage() const {
   return d_resourceManager->getResourceUsage();
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eb8eb6ca0..593f80f41 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -104,6 +104,7 @@ class CheckModels;
 class SmtSolver;
 class SygusSolver;
 class AbductionSolver;
+class ESolver;
 class InterpolationSolver;
 class QuantElimSolver;
 /**
@@ -794,6 +795,8 @@ class CVC4_PUBLIC SmtEngine
    */
   void setTimeLimit(unsigned long millis);
 
+  void setOutOfResourcesCallback(std::function<bool()>&& f);
+
   /**
    * Get the current resource usage count for this SmtEngine.  This
    * function can be used to ascertain reasonable values to pass as
@@ -1122,6 +1125,7 @@ class CVC4_PUBLIC SmtEngine
 
   /** The solver for abduction queries */
   std::unique_ptr<smt::AbductionSolver> d_abductSolver;
+  std::unique_ptr<smt::ESolver> d_eSolver;
   /** The solver for interpolation queries */
   std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
   /** The solver for quantifier elimination queries */
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 3bbe15b8c..85def07b5 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -176,10 +176,10 @@ bool Instantiate::addInstantiation(
     // this assertion is critical to soundness
     if (bad_inst)
     {
-      Trace("inst") << "***& Bad Instantiate " << q << " with " << std::endl;
+      std::cout << "***& Bad Instantiate " << q << " with " << std::endl;
       for (unsigned j = 0; j < terms.size(); j++)
       {
-        Trace("inst") << "   " << terms[j] << std::endl;
+        std::cout << "   " << terms[j] << std::endl;
       }
       Assert(false);
     }
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index fef3fdc67..1367cc033 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -37,7 +37,7 @@ namespace CVC4 {
 namespace theory {
 
 /** Default value for the uninterpreted sorts is the UF theory */
-TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
+thread_local TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
 
 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
   switch(level){
diff --git a/src/theory/theory.h b/src/theory/theory.h
index fa26ab65e..941d7525d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -267,7 +267,7 @@ class Theory {
   /**
    * The theory that owns the uninterpreted sort.
    */
-  static TheoryId s_uninterpretedSortOwner;
+  static thread_local TheoryId s_uninterpretedSortOwner;
 
   void printFacts(std::ostream& os) const;
   void debugPrintFacts() const;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index bd03a4d03..1ea4fee2d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -32,6 +32,7 @@
 #include "options/quantifiers_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"
+#include "proof/unsat_core.h"
 #include "smt/dump.h"
 #include "smt/logic_exception.h"
 #include "smt/term_formula_removal.h"
@@ -46,6 +47,7 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/relevance_manager.h"
 #include "theory/rewriter.h"
+#include "theory/smt_engine_subsolver.h"
 #include "theory/theory.h"
 #include "theory/theory_engine_proof_generator.h"
 #include "theory/theory_id.h"
@@ -560,6 +562,96 @@ void TheoryEngine::check(Theory::Effort effort) {
           // quantifiers engine must check at last call effort
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
         }
+        /*
+
+        // TODO: inefficient
+        Node confl;
+        std::vector<Node> ts;
+        theory::eq::EqualityEngine* ee = d_tc->getCoreEqualityEngine();
+        {
+          eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
+          while (!eqcs_i.isFinished())
+          {
+            Node eqc = (*eqcs_i);
+            eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
+            while (!eqc_i.isFinished())
+            {
+              Node n = *eqc_i;
+              smt::IsTAttribute ta;
+              if (n.getAttribute(ta)) {
+                ts.emplace_back(n);
+
+                eq::EqClassIterator eqc_i2 = eq::EqClassIterator(eqc, ee);
+                while (!eqc_i2.isFinished())
+                {
+                  Node n2 = *eqc_i2;
+                  if (n != n2) {
+                    confl = n.eqNode(n2);
+                    break;
+                  }
+                  ++eqc_i2;
+                }
+              }
+              ++eqc_i;
+            }
+            ++eqcs_i;
+          }
+        }
+        std::cout << "ts = " << ts << std::endl;
+
+        std::vector<Node> eqs;
+        std::vector<Node> neqs;
+        eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
+        while (!eqcs_i.isFinished())
+        {
+          Node eqc = (*eqcs_i);
+          eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
+          while (!eqc_i.isFinished())
+          {
+            Node n = *eqc_i;
+            smt::IsTAttribute ta;
+            if (n.getType().isBoolean() && ee->getRepresentative(n).isConst()) {
+              eqs.emplace_back(ee->getRepresentative(n).getConst<bool>() ? n : n.notNode());
+            } else {
+              eqs.emplace_back(n.eqNode(ee->getRepresentative(n)));
+            }
+            if (!n.getAttribute(ta)) {
+              for (const Node& t : ts) {
+                if (t.getType().isComparableTo(n.getType())) {
+                  neqs.emplace_back(n.eqNode(t).notNode());
+                }
+              }
+            }
+            ++eqc_i;
+          }
+          ++eqcs_i;
+        }
+
+        NodeManager* nm = NodeManager::currentNM();
+        std::unique_ptr<SmtEngine> deqChecker;
+        theory::initializeSubsolver(deqChecker);
+        deqChecker->getOptions().set(options::unsatCores, true);
+        for (const Node& eq : eqs) {
+          deqChecker->assertFormula(eq);
+        }
+        Node disneqs = nm->mkNode(kind::OR, neqs).notNode();
+        deqChecker->assertFormula(disneqs);
+        Result r = deqChecker->checkSat();
+        if (r.isSat() == Result::UNSAT)
+        {
+          std::vector<Node> uc;
+          for (const Node& c : deqChecker->getUnsatCore()) {
+            if (c != disneqs) {
+              uc.emplace_back(c.notNode());
+            }
+          }
+          lemma(TrustNode::mkTrustLemma(nm->mkNode(kind::OR, uc)), LemmaProperty::NONE);
+        }
+
+        std::cout << "eqs = " << eqs << std::endl;
+        std::cout << "neqs = " << neqs << std::endl;
+        */
+
       }
       if (!d_inConflict && !needCheck())
       {
@@ -1140,6 +1232,10 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   return d_sharedSolver->getEqualityStatus(a, b);
 }
 
+theory::eq::EqualityEngine* TheoryEngine::getEqualityEngine() {
+  return d_tc->getCoreEqualityEngine();
+}
+
 Node TheoryEngine::getModelValue(TNode var) {
   if (var.isConst())
   {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 1a9447681..15be73144 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -625,6 +625,8 @@ class TheoryEngine {
    */
   theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  theory::eq::EqualityEngine* getEqualityEngine();
+
   /**
    * Returns the value that a theory that owns the type of var currently
    * has (or null if none);
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 3be99021b..38ad09b22 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -24,6 +24,7 @@
 #include <sys/time.h>
 
 #include <chrono>
+#include <functional>
 #include <memory>
 
 #include "base/exception.h"
@@ -114,6 +115,11 @@ class CVC4_PUBLIC ResourceManager
   /** Can not be moved. */
   ResourceManager& operator=(ResourceManager&&) = delete;
 
+  void setCallback(std::function<bool()>&& f) { 
+    d_on = true;
+    d_callback = f;
+  }
+
   /** Checks whether any limit is active. */
   bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
   /** Checks whether any cumulative limit is active. */
@@ -126,7 +132,7 @@ class CVC4_PUBLIC ResourceManager
   /** Checks whether time has been exhausted. */
   bool outOfTime() const;
   /** Checks whether any limit has been exhausted. */
-  bool out() const { return d_on && (outOfResources() || outOfTime()); }
+  bool out() const { return d_on && (d_callback() || outOfResources() || outOfTime()); }
 
   /** Retrieves amount of resources used overall. */
   uint64_t getResourceUsage() const;
@@ -207,6 +213,7 @@ class CVC4_PUBLIC ResourceManager
 
   Options& d_options;
 
+  std::function<bool()> d_callback = [](){ return false; };
 }; /* class ResourceManager */
 
 }  // namespace CVC4
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3bdaad2ad..a509e60c1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -536,6 +536,17 @@ set(regress_0_tests
   regress0/eqrange1.smt2
   regress0/eqrange2.smt2
   regress0/eqrange3.smt2
+  regress0/e_solver/byron.smt2
+  regress0/e_solver/ex6.smt2
+  regress0/e_solver/min_7.smt2
+  regress0/e_solver/min_perf.smt2
+  regress0/e_solver/min_perf2.smt2
+  regress0/e_solver/min_perf3.smt2
+  regress0/e_solver/min_perf4.smt2
+  regress0/e_solver/min_perf5.min.smt2
+  regress0/e_solver/min_perf5.smt2
+  regress0/e_solver/min_perf6.smt2
+  regress0/e_solver/real.smt2
   regress0/expect/scrub.01.smtv1.smt2
   regress0/expect/scrub.03.smt2
   regress0/expect/scrub.06.cvc
diff --git a/test/regress/regress0/quantifiers/ari056.smt2 b/test/regress/regress0/quantifiers/ari056.smt2
index aee3cd970..3dd03cc83 100644
--- a/test/regress/regress0/quantifiers/ari056.smt2
+++ b/test/regress/regress0/quantifiers/ari056.smt2
@@ -2,5 +2,6 @@
 ; EXPECT: unsat
 (set-logic UFNIRA)
 (set-info :status unsat)
-(assert (forall ((X Int)) (= X 12) ))
+(declare-const y Int)
+(assert (and (= y 1) (forall ((X Int)) (= X 12) )))
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/ex6.smt2 b/test/regress/regress0/quantifiers/ex6.smt2
index 7285e1c4f..958f79659 100644
--- a/test/regress/regress0/quantifiers/ex6.smt2
+++ b/test/regress/regress0/quantifiers/ex6.smt2
@@ -6,6 +6,9 @@
 (declare-fun a () U)
 (declare-fun S (U) U)
 (declare-fun G (U U) Bool)
-(assert (and (forall ((x U)) (G (S x) x)) (forall ((x U) (y U) (z U)) (=> (and (G x y) (G y z)) (G x z))) (not (G (S (S a)) a))))
+(assert (and
+  (forall ((x U)) (G (S x) x))
+  (forall ((x U) (y U) (z U)) (=> (and (G x y) (G y z)) (G x z)))
+  (not (G (S (S a)) a))))
 (check-sat)
 (exit)
diff --git a/test/regress/regress0/quantifiers/mix-simp.smt2 b/test/regress/regress0/quantifiers/mix-simp.smt2
index b7142c6e9..8ec9afe73 100644
--- a/test/regress/regress0/quantifiers/mix-simp.smt2
+++ b/test/regress/regress0/quantifiers/mix-simp.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic LIRA)
+(set-logic UFLIRA)
 (set-info :status sat)
 (assert (forall ((x Real)) (exists ((y Int)) (and (>= y x) (< y (+ x 1))))))
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/nested-delta.smt2 b/test/regress/regress0/quantifiers/nested-delta.smt2
index 137a5eee3..7321dd2ae 100644
--- a/test/regress/regress0/quantifiers/nested-delta.smt2
+++ b/test/regress/regress0/quantifiers/nested-delta.smt2
@@ -1,4 +1,4 @@
-(set-logic LRA)
+(set-logic UFLRA)
 (set-info :status sat)
-(assert (forall ((x Real)) (or (exists ((y Real)) (and (< y 0) (< y x))) (<= x 0))))
+(assert (forall ((x Real)) (exists ((y Real)) (< y x))))
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2
index 2bdc2d994..8b5554c95 100644
--- a/test/regress/regress0/quantifiers/qbv-simp.smt2
+++ b/test/regress/regress0/quantifiers/qbv-simp.smt2
@@ -2,10 +2,15 @@
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
+; (assert
+;    (forall
+;     ((A (_ BitVec 8)) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8)))
+;       (or (and (= A B) (= C D)) (and (= A C) (= B D)))))
+
 (assert
    (forall
-    ((A (_ BitVec 8)) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8)))
-      (or (and (= A B) (= C D)) (and (= A C) (= B D)))))
+    ((A (_ BitVec 8)) (B (_ BitVec 8)))
+      (= A B)))
 
 (check-sat)
 
diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2
index b851d2e19..a2d771be1 100644
--- a/test/regress/regress1/quantifiers/horn-simple.smt2
+++ b/test/regress/regress1/quantifiers/horn-simple.smt2
@@ -6,7 +6,7 @@
 
 (assert (forall ((x Int)) (=> (= x 0) (I x))))
 
-(assert (forall ((x Int)) (=> (and (I x) (< x 6)) (I (+ x 1)))))
+(assert (forall ((x Int)) (=> (and (>= x 0) (I x) (< x 6)) (I (+ x 1)))))
 
 (assert (forall ((x Int)) (=> (I x) (<= x 10))))
 
diff --git a/test/regress/regress1/quantifiers/issue4849-nqe.smt2 b/test/regress/regress1/quantifiers/issue4849-nqe.smt2
index dd7a22e39..487c11291 100644
--- a/test/regress/regress1/quantifiers/issue4849-nqe.smt2
+++ b/test/regress/regress1/quantifiers/issue4849-nqe.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --cegqi-nested-qe -q
 ; EXPECT: sat
 (set-logic LIA)
-(set-option :cegqi-nested-qe true)
+; (set-option :cegqi-nested-qe true)
 (set-info :status sat)
 (assert (forall ((a Int)) (exists ((b Int)) (= (ite (= a 0) 0 1) (ite (= b 0) 0 1)))))
 (check-sat)