Propagate expected types through UF arguments (#3717)

1 files changed, 15 insertions, 12 deletions

diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 3c4c7d381..214198756 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -628,32 +628,35 @@ void LFSCUFProof::printOwnedTermAsType(Expr term,
                                        const ProofLetMap& map,
                                        TypeNode expectedType)
 {
-  Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl;
+  Node node = Node::fromExpr(term);
+  Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << node << std::endl;
 
-  Assert(theory::Theory::theoryOf(term) == theory::THEORY_UF);
+  Assert(theory::Theory::theoryOf(node) == theory::THEORY_UF);
 
-  if (term.getKind() == kind::VARIABLE ||
-      term.getKind() == kind::SKOLEM ||
-      term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
-    os << term;
+  if (node.getKind() == kind::VARIABLE ||
+      node.getKind() == kind::SKOLEM ||
+      node.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
+    os << node;
     return;
   }
 
-  Assert(term.getKind() == kind::APPLY_UF);
+  Assert(node.getKind() == kind::APPLY_UF);
 
-  if(term.getType().isBoolean()) {
+  if(node.getType().isBoolean()) {
     os << "(p_app ";
   }
-  Expr func = term.getOperator();
+  Node func = node.getOperator();
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
     os << "(apply _ _ ";
   }
   os << func << " ";
-  for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+  Assert(func.getType().isFunction());
+  std::vector<TypeNode> argsTypes = node.getOperator().getType().getArgTypes();
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
 
-    bool convertToBool = (term[i].getType().isBoolean() && !d_proofEngine->printsAsBool(term[i]));
+    bool convertToBool = (node[i].getType().isBoolean() && !d_proofEngine->printsAsBool(node[i]));
     if (convertToBool) os << "(f_to_b ";
-    d_proofEngine->printBoundTerm(term[i], os, map);
+    d_proofEngine->printBoundTerm(term[i], os, map, argsTypes[i]);
     if (convertToBool) os << ")";
     os << ")";
   }