Merge branch 'master' into privateGetprivateGet

1 files changed, 18 insertions, 2 deletions

diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp
index 72db06060..33004e81f 100644
--- a/src/proof/lfsc/lfsc_post_processor.cpp
+++ b/src/proof/lfsc/lfsc_post_processor.cpp
@@ -16,6 +16,7 @@
 
 #include "options/proof_options.h"
 #include "proof/lazy_proof.h"
+#include "proof/lfsc/lfsc_printer.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
@@ -158,6 +159,8 @@ bool LfscProofPostprocessCallback::update(Node res,
     {
       Assert(res.getKind() == EQUAL);
       Assert(res[0].getOperator() == res[1].getOperator());
+      Trace("lfsc-pp-cong") << "Processing congruence for " << res << " "
+                            << res[0].getKind() << std::endl;
       // different for closures
       if (res[0].isClosure())
       {
@@ -210,6 +213,8 @@ bool LfscProofPostprocessCallback::update(Node res,
       // REFL step. Notice this may be for interpreted or uninterpreted
       // function symbols.
       Node op = d_tproc.getOperatorOfTerm(res[0]);
+      Trace("lfsc-pp-cong") << "Processing cong for op " << op << " "
+                            << op.getType() << std::endl;
       Assert(!op.isNull());
       // initial base step is REFL
       Node opEq = op.eqNode(op);
@@ -245,9 +250,20 @@ bool LfscProofPostprocessCallback::update(Node res,
         for (size_t i = 0; i < nchildren; i++)
         {
           size_t ii = (nchildren - 1) - i;
+          Node uop = op;
+          // special case: each bv concat in the chain has a different type,
+          // so remake the operator here.
+          if (k == kind::BITVECTOR_CONCAT)
+          {
+            // we get the operator of the next argument concatenated with the
+            // current accumulated remainder.
+            Node currApp =
+                nm->mkNode(kind::BITVECTOR_CONCAT, children[ii][0], currEq[0]);
+            uop = d_tproc.getOperatorOfTerm(currApp);
+          }
           Node argAppEq =
-              nm->mkNode(HO_APPLY, op, children[ii][0])
-                  .eqNode(nm->mkNode(HO_APPLY, op, children[ii][1]));
+              nm->mkNode(HO_APPLY, uop, children[ii][0])
+                  .eqNode(nm->mkNode(HO_APPLY, uop, children[ii][1]));
           addLfscRule(cdp, argAppEq, {opEq, children[ii]}, LfscRule::CONG, {});
           // now, congruence to the current equality
           Node nextEq;