mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-02-23 18:42:01 -08:00
parent d5383e2387 64888b6b19
commit 4e7a867cd9
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/tactic/core/ctx_simplify_tactic.cpp
View file

@ -374,7 +374,7 @@ struct ctx_simplify_tactic::imp {
if (new_arg != arg)
modified = true;
if (i < num_args - 1 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR))
new_arg = m.mk_false();
new_arg = OR ? m.mk_true() : m.mk_false();
if ((OR && m.is_false(new_arg)) ||
(!OR && m.is_true(new_arg))) {
@ -403,7 +403,7 @@ struct ctx_simplify_tactic::imp {
if (new_arg != arg)
modified = true;
if (i > 0 && !m.is_true(new_arg) && !m.is_false(new_arg) && !assert_expr(new_arg, OR))
new_arg = m.mk_false();
new_arg = OR ? m.mk_true() : m.mk_false();
if ((OR && m.is_false(new_arg)) ||
(!OR && m.is_true(new_arg))) {