From 2c91f388dfa02fa74c933af9d7249a61a276942e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sat, 6 Aug 2016 15:35:47 -0400 Subject: [PATCH] add defensive double-non-concat check in theory_str::simplify_concat_equality() --- src/smt/theory_str.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 296041a39..ac897ee7d 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -2317,10 +2317,13 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { simplify_parent(new_nn1, new_nn2); } return; + } else if (!n1IsConcat && !n2IsConcat) { + // normally this should never happen, because group_terms_by_eqc() should have pre-simplified + // as much as possible. however, we make a defensive check here just in case + TRACE("t_str_detail", tout << "WARNING: nn1_new and nn2_new both simplify to non-concat terms" << std::endl;); + return; } - // TODO what happens if BOTH of these are simplified into non-concat terms? - expr * v1_arg0 = a_new_nn1->get_arg(0); expr * v1_arg1 = a_new_nn1->get_arg(1); expr * v2_arg0 = a_new_nn2->get_arg(0);