From f5e94af784b19e021e367c688d295298abf214b8 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 2 Dec 2015 22:15:04 -0500 Subject: [PATCH] check that both simplified expressions are concats in simplify_concat_equality() this seems to fix all the crashes but the solver takes forever to solve a really simple instance with easy model generation, so I think something is still wrong probably next I will go through and change std::map to obj_map, etc. --- src/smt/theory_str.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 62100cfcd..f6187c7c1 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -922,10 +922,6 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { expr * new_nn2 = simplify_concat(nn2); app * a_new_nn1 = to_app(new_nn1); app * a_new_nn2 = to_app(new_nn2); - 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); - expr * v2_arg1 = a_new_nn2->get_arg(1); TRACE("t_str_detail", tout << "new_nn1 = " << mk_ismt2_pp(new_nn1, m) << std::endl << "new_nn2 = " << mk_ismt2_pp(new_nn2, m) << std::endl;); @@ -960,6 +956,13 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { 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); + expr * v2_arg1 = a_new_nn2->get_arg(1); + if (!in_same_eqc(new_nn1, new_nn2) && (nn1 != new_nn1 || nn2 != new_nn2)) { int ii4 = 0; expr* item[3];