From 7b1aee48dda022f85b8cc5898be8f5c51f3375c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 May 2020 10:40:09 -0700 Subject: [PATCH] fix #4203 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_utvpi_def.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index ec5a19e35..ee22b50f0 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -970,7 +970,7 @@ namespace smt { if (eps_r.is_pos()) { rational num_r = -b.get_rational(); SASSERT(num_r.is_pos()); - rational new_delta = num_r/4*eps_r; + rational new_delta = num_r/(4*eps_r); if (new_delta < m_delta) { m_delta = new_delta; }