Mark quantifier instantiations as needs justify (#5684)

This avoids a solution soundness issue when disabling all NL strategies and using --nl-rlv=always.

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index da9fdd02289550e940bb3b4bff40c2a57acb5531..3e625218ced550c4afa8c76d4766c834ca7d707c 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -994,14 +994,16 @@ void QuantifiersEngine::flushLemmas(){
       const Node& lemw = d_lemmas_waiting[i];
       Trace("qe-lemma") << "Lemma : " << lemw << std::endl;
       itp = d_lemmasWaitingPg.find(lemw);
+      LemmaProperty p =
+          LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY;
       if (itp != d_lemmasWaitingPg.end())
       {
         TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second);
-        out.trustedLemma(tlemw, LemmaProperty::PREPROCESS);
+        out.trustedLemma(tlemw, p);
       }
       else
       {
-        out.lemma(lemw, LemmaProperty::PREPROCESS);
+        out.lemma(lemw, p);
       }
     }
     d_lemmas_waiting.clear();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b32e0799df1eca18fbaad53d7c5f2369a92b2835..01903202ca8490fde87709e381542469cb2ec8fd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -809,6 +809,7 @@ set(regress_0_tests
   regress0/quantifiers/bug291.smt2
   regress0/quantifiers/bug749-rounding.smt2
   regress0/quantifiers/cbqi-lia-dt-simp.smt2
+  regress0/quantifiers/cegqi-needs-justify.smt2
   regress0/quantifiers/cegqi-nl-simp.cvc
   regress0/quantifiers/cegqi-nl-sq.smt2
   regress0/quantifiers/cegqi-par-dt-simple.smt2

diff --git a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
new file mode 100644 (file)
index 0000000..9b7f7a8
--- /dev/null
+++ b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --nl-rlv=always
+; EXPECT: unsat
+(set-logic NRA)
+(set-info :status unsat)
+(declare-fun c () Real)
+(declare-fun t () Real)
+(assert (forall ((s Real)) (and (> t 0) (= 0 (* t c)) (or (< s c) (> s 1.0)))))
+; previously answered "sat" with --no-nl-ext --nl-rlv=always
+(check-sat)