mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

check that both simplified expressions are concats in simplify_concat_equality()

Browse source 
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.
This commit is contained in:
Murphy Berzish 2015-12-02 22:15:04 -05:00
parent 1a15b3937d
commit f5e94af784
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_str.cpp
View file

@ -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];