diff options
-rw-r--r-- | src/proof/arith_proof.cpp | 5 | ||||
-rw-r--r-- | src/proof/arith_proof.h | 2 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 2 |
3 files changed, 8 insertions, 1 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index f1d7c0e43..ee7bf5f99 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -1341,4 +1341,9 @@ bool LFSCArithProof::printsAsBool(const Node& n) return n.getType().isBoolean() and (n.isVar() or n.isConst()); } +TypeNode LFSCArithProof::equalityType(const Expr& left, const Expr& right) +{ + return TypeNode::fromType(!left.getType().isInteger() ? left.getType() : right.getType()); +} + } /* CVC4 namespace */ diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 44e99cb76..587569b1a 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -208,6 +208,8 @@ public: * Return whether this node, when serialized to LFSC, has sort `Bool`. Otherwise, the sort is `formula`. */ bool printsAsBool(const Node& n) override; + + TypeNode equalityType(const Expr& left, const Expr& right) override; }; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index b516c250f..88a53062a 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -971,7 +971,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, } else { - printBoundTerm(term[2], os, map); + printBoundTerm(term[2], os, map, armType); } os << ")"; return; |