From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 Apr 2021 02:18:13 +0000 (-0500)
Subject: Enable strings exp by default for strings specific logics (#6424)
X-Git-Tag: cvc5-1.0.0~1844
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cea1ad700bc4cff0d9fcfb0f14c8908e24bbc8c2;p=cvc5.git

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 117fbbd4b..047dbfea6 100644
--- 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 841cd4ab9..da220be18 100644
--- 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])
     {