From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 16 Dec 2020 21:07:55 +0000 (-0600)
Subject: Mark quantifier instantiations as needs justify (#5684)
X-Git-Tag: cvc5-1.0.0~2433
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d5de3d822b978be11c98da5f026ab5f2ca9d0a83;p=cvc5.git

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 da9fdd022..3e625218c 100644
--- 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 b32e0799d..01903202c 100644
--- 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
index 000000000..9b7f7a847
--- /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)