From feef85c129aca77b1f160851681a61042c9f5a66 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 20 Sep 2016 15:37:29 -0400 Subject: [PATCH] override scope check in theory_str::solve_concat_eq_str fixes indexof2-009.smt2 --- src/smt/theory_str.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index b2e0e70ba..798e16e7c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -5973,24 +5973,40 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { bool entry1InScope; if (entry1 == varForBreakConcat.end()) { + TRACE("t_str_detail", tout << "key1 no entry" << std::endl;); entry1InScope = false; } else { + // OVERRIDE. + entry1InScope = true; + TRACE("t_str_detail", tout << "key1 entry" << std::endl;); + /* if (internal_variable_set.find((entry1->second)[0]) == internal_variable_set.end()) { + TRACE("t_str_detail", tout << "key1 entry not in scope" << std::endl;); entry1InScope = false; } else { + TRACE("t_str_detail", tout << "key1 entry in scope" << std::endl;); entry1InScope = true; } + */ } bool entry2InScope; if (entry2 == varForBreakConcat.end()) { + TRACE("t_str_detail", tout << "key2 no entry" << std::endl;); entry2InScope = false; } else { + // OVERRIDE. + entry2InScope = true; + TRACE("t_str_detail", tout << "key2 entry" << std::endl;); + /* if (internal_variable_set.find((entry2->second)[0]) == internal_variable_set.end()) { + TRACE("t_str_detail", tout << "key2 entry not in scope" << std::endl;); entry2InScope = false; } else { + TRACE("t_str_detail", tout << "key2 entry in scope" << std::endl;); entry2InScope = true; } + */ } TRACE("t_str_detail", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl