Always ensure literal when requiring phase via inference manager (#8292)

Also to be safe, ensures we clear pending in quantifiers engine.

Fixes cvc5/cvc5-projects#484.

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1241988838f1ca3c5a2a6510f05da7401154c42b..dd510a861eabf25017ba74326e3b8ab0c92ac92c 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -507,6 +507,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     //output debug stats
     d_qim.getInstantiate()->debugPrintModel();
   }
+  d_qim.clearPending();
 }
 
 void QuantifiersEngine::notifyCombineTheories() {

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index b4add920ae27e496b8e39517dc76d3ab675ce1a2..97019d101a26eeff688b80ab35a36c69ae5f4731 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -609,7 +609,8 @@ DecisionManager* TheoryInferenceManager::getDecisionManager()
 
 void TheoryInferenceManager::requirePhase(TNode n, bool pol)
 {
-  return d_out.requirePhase(n, pol);
+  Node en = d_theoryState.getValuation().ensureLiteral(n);
+  return d_out.requirePhase(en, pol);
 }
 
 void TheoryInferenceManager::spendResource(Resource r)

diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt
index e110ec07521816fe802c39f2abb4335ad471e613..c250a0598664358036d3c4dcb2feb9022bbbf183 100644 (file)
--- a/test/api/cpp/CMakeLists.txt
+++ b/test/api/cpp/CMakeLists.txt
@@ -60,3 +60,4 @@ cvc5_add_api_test(proj-issue377)
 cvc5_add_api_test(proj-issue395)
 cvc5_add_api_test(proj-issue399)
 cvc5_add_api_test(proj-issue445)
+cvc5_add_api_test(proj-issue484)

diff --git a/test/api/cpp/proj-issue484.cpp b/test/api/cpp/proj-issue484.cpp
new file mode 100644 (file)
index 0000000..10db4c8
--- /dev/null
+++ b/test/api/cpp/proj-issue484.cpp
@@ -0,0 +1,36 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Test for project issue #445
+ *
+ */
+
+#include <cassert>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  Sort s1 = slv.getIntegerSort();
+  Term t1 = slv.mkVar(s1, "_x0");
+  Term t3 = slv.mkInteger("8072314426184292007005683562403");
+  Term t7 = slv.mkTerm(Kind::ADD, {t1, t1, t1, t3});
+  Term t8 = slv.mkTerm(slv.mkOp(Kind::DIVISIBLE, 2319436191), {t7});
+  Term vl = slv.mkTerm(Kind::VARIABLE_LIST, {t1});
+  Term t10 = slv.mkTerm(Kind::FORALL, {vl, t8});
+  slv.checkSatAssuming({t10});
+  slv.assertFormula({t10});
+  slv.checkSat();
+}