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

ctx_simplify: fix bug in simplification of or exprs

Browse source 
this triggered when the or covers the whole space -> true
This commit is contained in:
Nuno Lopes 2016-02-23 10:37:01 +00:00
parent 12458b1a84
commit 64888b6b19
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))) {