From 081f3676865215c88d057b7d5d832e24e3c263bb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 May 2021 16:33:06 -0500 Subject: [PATCH] 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. --- src/theory/strings/infer_proof_cons.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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: -- 2.30.2