Fix

ajreynol · Dec 19, 2024 · 9914b82 · 9914b82
1 parent 2765368
commit 9914b82
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
@@ -467,7 +467,7 @@ bool InferProofCons::convert(Env& env,
       Trace("strings-ipc-core")
           << "Main equality after subs " << pmainEq << std::endl;
       // now, conclude the proper equality
-      Node mainEqSRew = psb.applyPredElim(pmainEq, pcsr);
+      Node mainEqSRew = psb.applyPredElim(pmainEq, {});
       if (mainEqSRew == conc)
       {
         Trace("strings-ipc-core") << "...success after rewrite!" << std::endl;