diff options
Diffstat (limited to 'src/proof/theory_proof.cpp')
| -rw-r--r-- | src/proof/theory_proof.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 473152647..e70cd60b9 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -354,7 +354,8 @@ void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, Node n1 = it->first; Node n2 = it->second; - Assert(theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); + Assert(n1.toExpr() == utils::mkFalse() || + theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); std::ostringstream rewriteRule; rewriteRule << ".lrr" << d_assertionToRewrite.size(); |