Enable strings exp by default for strings specific logics (#6424)

One of the main motivations for this PR is to simplify our process for doing SMT-LIB wide runs.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 117fbbd4b6efc3a7e06cf217fba993e2732d35d1..047dbfea608ab44e5c4b912f98934d5229351691 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -284,6 +284,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // Set default options associated with strings-exp. We also set these options
   // if we are using eager string preprocessing, which may introduce quantified
   // formulas at preprocess time.
+  if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS))
+  {
+    // If the user explicitly set a logic that includes strings, but is not
+    // the generic "ALL" logic, then enable stringsExp.
+    options::stringExp.set(true);
+  }
   if (options::stringExp() || !options::stringLazyPreproc())
   {
     // We require quantifiers since extended functions reduce using them.

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 841cd4ab9b785c3f07b26e62f1acc354a0a2b622..da220be18f9bbdbddbc782aee2a3ec1ac3bb56dd 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -332,6 +332,11 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
        i++)
   {
     Node q = fm->getAssertedQuantifier(i);
+    registerQuantifiedFormula(q);
+    if (!isHandled(q))
+    {
+      continue;
+    }
     // make sure all types are set
     for (const Node& v : q[0])
     {