mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix bug in ctx-solver-simplify reported @ http://z3.codeplex.com/workitem/51

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-06-27 11:59:40 -05:00
parent 13262a0fc5
commit 619bd91ddb
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -218,7 +218,7 @@ protected:
else if (m.is_bool(arg)) { else if (m.is_bool(arg)) {
res = local_simplify(a, n, id, i); res = local_simplify(a, n, id, i);
TRACE("ctx_solver_simplify_tactic", TRACE("ctx_solver_simplify_tactic",
tout << "Already cached: " << path_r.first << " " << mk_pp(res, m) << "\n";); tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";);
args.push_back(res); args.push_back(res);
} }
else { else {
@ -327,7 +327,7 @@ protected:
tmp = m.mk_eq(result, n); tmp = m.mk_eq(result, n);
m_solver.assert_expr(tmp); m_solver.assert_expr(tmp);
if (!simplify_bool(n2, result)) { if (!simplify_bool(n2, result)) {
result = a; result = a->get_arg(index);
} }
m_solver.pop(1); m_solver.pop(1);
return result; return result;