Make strings emp inference an unhandled inference for proofs (#6575)

The strings inference id STRINGS_INFER_EMP is a rare inference that currently leads to a segfault when proof reconstruction is tried for it. This PR makes it unhandled.

This was caught by a new regression on the soon-to-be-merged jh-new branch.

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index bc02dcbb69a76462df4a5e3c5a893096d09d1d11..8ee29f71230d865ab08e456ffc2dde16ecadebf6 100644 (file)
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -136,7 +136,6 @@ void InferProofCons::convert(InferenceId infer,
     break;
     // ========================== rewrite pred
     case InferenceId::STRINGS_EXTF_EQ_REW:
-    case InferenceId::STRINGS_INFER_EMP:
     {
       // the last child is the predicate we are operating on, move to front
       Node src = ps.d_children[ps.d_children.size() - 1];
@@ -680,7 +679,9 @@ void InferProofCons::convert(InferenceId infer,
     }
     break;
     // ========================== unit injectivity
-    case InferenceId::STRINGS_UNIT_INJ: { ps.d_rule = PfRule::STRING_SEQ_UNIT_INJ;
+    case InferenceId::STRINGS_UNIT_INJ:
+    {
+      ps.d_rule = PfRule::STRING_SEQ_UNIT_INJ;
     }
     break;
     // ========================== prefix conflict
@@ -848,6 +849,7 @@ void InferProofCons::convert(InferenceId infer,
     case InferenceId::STRINGS_CARDINALITY:
     case InferenceId::STRINGS_I_CYCLE_E:
     case InferenceId::STRINGS_I_CYCLE:
+    case InferenceId::STRINGS_INFER_EMP:
     case InferenceId::STRINGS_RE_DELTA:
     case InferenceId::STRINGS_RE_DELTA_CONF:
     case InferenceId::STRINGS_RE_DERIVE: