From b9bbfbdbb7bcf67a9489eab3c8ef535b6d324825 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Jan 2015 12:05:12 +0530 Subject: [PATCH] fix interval dependencies bug. Codeplex issue 163 Signed-off-by: Nikolaj Bjorner --- src/duality/duality_rpfp.cpp | 2 +- src/smt/old_interval.cpp | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index cdc8fb3b2..304e41168 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -3147,7 +3147,7 @@ namespace Duality { } if(node->Annotation.IsEmpty() || eq(node->Annotation.Formula,prev_annot) || (repeated_case_count > 0 && !axioms_added) || (repeated_case_count >= 10)){ - looks_bad: + //looks_bad: if(!axioms_added){ // add the axioms in the off chance they are useful const std::vector &theory = ls->get_axioms(); diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index ffc3331be..9dd8e0955 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -295,6 +295,8 @@ interval & interval::operator*=(interval const & other) { } if (other.is_zero()) { *this = other; + m_lower_dep = m_manager.mk_join(m_lower_dep, m_upper_dep); + m_upper_dep = m_lower_dep; return *this; }