From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 19 May 2021 21:33:06 +0000 (-0500)
Subject: Make strings emp inference an unhandled inference for proofs (#6575)
X-Git-Tag: cvc5-1.0.0~1734
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=081f3676865215c88d057b7d5d832e24e3c263bb;p=cvc5.git

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 bc02dcbb6..8ee29f712 100644
--- 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: