mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 21:20:52 +00:00
Code Activity

fix blast rule for overflow

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-05 08:16:34 -08:00
parent 10d56d9af9
commit 187a6b17dd
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/polysat/saturation.cpp
View file

@ -226,15 +226,14 @@ namespace polysat {
void saturation::try_umul_blast(umul_ovfl const& sc) { void saturation::try_umul_blast(umul_ovfl const& sc) {
auto x = sc.p(); auto x = sc.p();
auto y = sc.q(); auto y = sc.q();
if (!x.is_val()) rational vx, vy;
if (!c.try_eval(x, vx))
return; return;
if (!y.is_val()) if (!c.try_eval(y, vy))
return; return;
auto N = x.manager().power_of_2(); auto N = x.manager().power_of_2();
auto d = c.get_dependency(sc.id()); auto d = c.get_dependency(sc.id());
auto vx = x.val();
auto vy = y.val();
auto bx = vx.get_num_bits(); auto bx = vx.get_num_bits();
auto by = vy.get_num_bits(); auto by = vy.get_num_bits();
if (bx > by) { if (bx > by) {