mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Code Activity

add trace message to indicate which free variables are giving us trouble

Browse source 
I think I'm onto the issue though
This commit is contained in:
Murphy Berzish 2015-12-02 23:35:26 -05:00
parent f5e94af784
commit e010e7c0d6
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_str.cpp
View file

@ -532,6 +532,8 @@ void theory_str::instantiate_concat_axiom(enode * cat) {
ast_manager & m = get_manager();
TRACE("t_str_detail", tout << "instantiating concat axiom for " << mk_ismt2_pp(a_cat, m) << std::endl;);
// build LHS
expr_ref len_xy(m);
// TODO should we use str_util for these and other expressions?
@ -560,7 +562,6 @@ void theory_str::instantiate_concat_axiom(enode * cat) {
// finally assert equality between the two subexpressions
app * eq = m.mk_eq(len_xy, len_x_plus_len_y);
SASSERT(eq);
TRACE("t_str", tout << mk_ismt2_pp(eq, m) << std::endl;);
assert_axiom(eq);
}
@ -3443,6 +3444,13 @@ final_check_status theory_str::final_check_eh() {
return FC_DONE;
}
CTRACE("t_str", needToAssignFreeVars,
tout << "Need to assign values to the following free variables:" << std::endl;
for (std::set<expr*>::iterator itx = free_variables.begin(); itx != free_variables.end(); ++itx) {
tout << mk_ismt2_pp(*itx, m) << std::endl;
}
);
// -----------------------------------------------------------
// variables in freeVar are those not bounded by Concats
// classify variables in freeVarMap: