From 64888b6b1956500f3261cbf8e154433cec156407 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 23 Feb 2016 10:37:01 +0000 Subject: [PATCH] ctx_simplify: fix bug in simplification of or exprs this triggered when the or covers the whole space -> true --- src/tactic/core/ctx_simplify_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 6d557a3ac..e07f7417d 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -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))) {