More updates to arithmetic in preparation for central equality engine (#6927)

Makes arithEqSolver more robust to propagations from multiple sources, changes the default relationship to congruence manager based on preliminary results on SMT-LIB.

1 files changed, 12 insertions, 0 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index d5b3b7929..e12d3eb1d 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -968,6 +968,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Trace("smt") << "setting decision mode to " << opts.decision.decisionMode
                  << std::endl;
   }
+
+  // set up of central equality engine
+  if (opts.arith.arithEqSolver)
+  {
+    if (!opts.arith.arithCongManWasSetByUser)
+    {
+      // if we are using the arithmetic equality solver, do not use the
+      // arithmetic congruence manager by default
+      opts.arith.arithCongMan = false;
+    }
+  }
+
   if (options::incrementalSolving())
   {
     // disable modes not supported by incremental