diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-03 10:19:44 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-03 10:19:44 -0600 |
commit | 5b010143cce0cace27e2556e26221f69ae43f688 (patch) | |
tree | 40c67ef477bd2b6fa48b57ad55890d8da088ac17 /src/theory/quantifiers | |
parent | 1cec37904f1d770d7756d5661ff9b86fbca6d7ac (diff) |
Fix invariant template inference for trivially infeasible conjecture (#3693)
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
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(), |