Remove preregister instantiation heuristic (#5713)

This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.

1 files changed, 0 insertions, 5 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index bbbe73cb1..8b0986db6 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1086,10 +1086,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       options::macrosQuant.set(false);
     }
-    if (!options::cegqiPreRegInst.wasSetByUser())
-    {
-      options::cegqiPreRegInst.set(true);
-    }
     // use tangent planes by default, since we want to put effort into
     // the verification step for sygus queries with non-linear arithmetic
     if (!options::nlExtTangentPlanes.wasSetByUser())
@@ -1135,7 +1131,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       // cannot do nested quantifier elimination in incremental mode
       options::cegqiNestedQE.set(false);
-      options::cegqiPreRegInst.set(false);
     }
     if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
     {