mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

port forbidden intervals

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-08 12:04:19 -08:00
parent 4bcd2e038f
commit c41477aadb
13 changed files with 1122 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/polysat_solver.cpp
View file

@ -28,6 +28,7 @@ The result of polysat::core::check is one of:
#include "sat/smt/polysat_solver.h"
#include "sat/smt/euf_solver.h"
#include "sat/smt/polysat_ule.h"
#include "sat/smt/polysat_umul_ovfl.h"
namespace polysat {
@ -221,8 +222,8 @@ namespace polysat {
return expr_ref(bv.mk_ule(l, h), m);
}
case ckind_t::umul_ovfl_t: {
auto l = pdd2expr(sc.to_umul_ovfl().lhs());
auto r = pdd2expr(sc.to_umul_ovfl().rhs());
auto l = pdd2expr(sc.to_umul_ovfl().p());
auto r = pdd2expr(sc.to_umul_ovfl().q());
return expr_ref(bv.mk_bvumul_ovfl(l, r), m);
}
case ckind_t::smul_fl_t: