diff options
Diffstat (limited to 'src/proof/arith_proof.cpp')
| -rw-r--r-- | src/proof/arith_proof.cpp | 5 |
1 files changed, 5 insertions, 0 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 */ |