From 187a6b17ddad36d9959722b616ba7857f667d643 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Feb 2024 08:16:34 -0800 Subject: [PATCH] fix blast rule for overflow Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/saturation.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp index ce81a39aa..103da2e55 100644 --- a/src/sat/smt/polysat/saturation.cpp +++ b/src/sat/smt/polysat/saturation.cpp @@ -226,15 +226,14 @@ namespace polysat { void saturation::try_umul_blast(umul_ovfl const& sc) { auto x = sc.p(); auto y = sc.q(); - if (!x.is_val()) + rational vx, vy; + if (!c.try_eval(x, vx)) return; - if (!y.is_val()) + if (!c.try_eval(y, vy)) return; auto N = x.manager().power_of_2(); auto d = c.get_dependency(sc.id()); - auto vx = x.val(); - auto vy = y.val(); auto bx = vx.get_num_bits(); auto by = vy.get_num_bits(); if (bx > by) {