From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 3 Feb 2020 16:19:44 +0000 (-0600)
Subject: Fix invariant template inference for trivially infeasible conjecture (#3693)
X-Git-Tag: cvc5-1.0.0~3693
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b010143cce0cace27e2556e26221f69ae43f688;p=cvc5.git

Fix invariant template inference for trivially infeasible conjecture (#3693)
---

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 0e7606276..f81d2455c 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -163,7 +163,12 @@ void CegSingleInv::initialize(Node q)
   std::vector<Node> sivars;
   d_sip->getSingleInvocationVariables(sivars);
   Node invariant = d_sip->getFunctionInvocationFor(prog);
-  Assert(!invariant.isNull());
+  if (invariant.isNull())
+  {
+    // the conjecture did not have an instance of the invariant
+    // (e.g. it is trivially true/false).
+    return;
+  }
   invariant = invariant.substitute(sivars.begin(),
                                    sivars.end(),
                                    prog_templ_vars.begin(),
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3bcdec380..cea7b60ad 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -948,6 +948,7 @@ set(regress_0_tests
   regress0/sygus/no-syntax-test.sy
   regress0/sygus/parity-AIG-d0.sy
   regress0/sygus/parse-bv-let.sy
+  regress0/sygus/pbe-pred-contra.sy
   regress0/sygus/pLTL-sygus-syntax-err.sy
   regress0/sygus/real-si-all.sy
   regress0/sygus/sygus-no-wf.sy
diff --git a/test/regress/regress0/sygus/pbe-pred-contra.sy b/test/regress/regress0/sygus/pbe-pred-contra.sy
new file mode 100644
index 000000000..22fc12e60
--- /dev/null
+++ b/test/regress/regress0/sygus/pbe-pred-contra.sy
@@ -0,0 +1,7 @@
+; COMMAND_LINE: --cegqi-si=none --sygus-out=status
+; EXPECT: unknown
+(set-logic LIA)
+(synth-fun P ((x Int)) Bool)
+(constraint (P 54))
+(constraint (not (P 54)))
+(check-synth)