From cbf99fdd92c483e70e3b73feb9d368d4bf632a24 Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Mon, 10 Feb 2020 18:32:20 -0800
Subject: [PATCH] Implement LFSCArithProof::equalityType. (#3740)

Also, missed an armType use.
---
 src/proof/arith_proof.cpp  | 5 +++++
 src/proof/arith_proof.h    | 2 ++
 src/proof/theory_proof.cpp | 2 +-
 3 files changed, 8 insertions(+), 1 deletion(-)

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;
-- 
2.30.2