From a567cce685dd385da2fd7b983b0eb5ebe6064a0a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Nov 2015 10:13:27 -0800 Subject: [PATCH] fix(library/blast/simplify_actions): compilation error due to recent changes in the simplifier API --- src/library/blast/simplify_actions.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/blast/simplify_actions.cpp b/src/library/blast/simplify_actions.cpp index 909965ea75..dcc72de394 100644 --- a/src/library/blast/simplify_actions.cpp +++ b/src/library/blast/simplify_actions.cpp @@ -43,7 +43,7 @@ action_result simplify_target_action() { bool iff = use_iff(target); name rname = iff ? get_iff_name() : get_eq_name(); auto r = simplify(rname, target, s.get_simp_rule_sets()); - if (r.is_none()) + if (!r.has_proof()) return action_result::failed(); // did nothing s.push_proof_step(new simplify_target_proof_step_cell(iff, r.get_proof())); s.set_target(r.get_new());