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 0e76062768921a32cbb371993a7fce368acf9ea0..f81d2455c1ab4ba727f5d75ba1e98be66083cbbc 100644 (file)
--- 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 3bcdec380498ef72583b88d91b4f3b0060d761ce..cea7b60adfe3f0d293818e64ec865bd3f7fe4bcb 100644 (file)
--- 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 (file)
index 0000000..22fc12e
--- /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)