Set theoryof-mode after theory widening

Fixes #4367. We set the theoryof-mode depending on whether sharing is
enabled or not. However, we were checking whether sharing was enabled
before theory widening, leading to unexpected results. This commit moves
the check after widening the theories.

3 files changed, 25 insertions, 12 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index e06363883..b5d36f134 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -538,18 +538,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     smte.setOption("produce-models", SExpr("true"));
   }
 
-  // Set the options for the theoryOf
-  if (!options::theoryOfMode.wasSetByUser())
-  {
-    if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
-        && !logic.isTheoryEnabled(THEORY_STRINGS)
-        && !logic.isTheoryEnabled(THEORY_SETS))
-    {
-      Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
-      options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
-    }
-  }
-
   /////////////////////////////////////////////////////////////////////////////
   // Theory widening
   //
@@ -607,8 +595,21 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       logic.lock();
     }
   }
+
   /////////////////////////////////////////////////////////////////////////////
 
+  // Set the options for the theoryOf
+  if (!options::theoryOfMode.wasSetByUser())
+  {
+    if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
+        && !logic.isTheoryEnabled(THEORY_STRINGS)
+        && !logic.isTheoryEnabled(THEORY_SETS))
+    {
+      Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
+      options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
+    }
+  }
+
   // by default, symmetry breaker is on only for non-incremental QF_UF
   if (!options::ufSymmetryBreaker.wasSetByUser())
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 38c60e0e3..20985a5f8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -37,6 +37,7 @@ set(regress_0_tests
   regress0/arith/issue3413.smt2
   regress0/arith/issue3480.smt2
   regress0/arith/issue3683.smt2
+  regress0/arith/issue4367.smt2
   regress0/arith/issue4525.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
diff --git a/test/regress/regress0/arith/issue4367.smt2 b/test/regress/regress0/arith/issue4367.smt2
new file mode 100644
index 000000000..abe5b09fd
--- /dev/null
+++ b/test/regress/regress0/arith/issue4367.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --incremental --check-unsat-cores
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic NRA)
+(declare-const r0 Real)
+(assert (! (forall ((q0 Bool) (q1 Real)) (= (* r0 r0) r0 r0)) :named IP_2))
+(assert (! (not (forall ((q2 Real)) (not (<= 55.033442 r0 55.033442 q2)))) :named IP_5))
+(push 1)
+(check-sat)
+(pop 1)
+(check-sat)