mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 04:31:24 +00:00
Code Activity

add case for exclude 0

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-10 17:19:10 -08:00
parent 17f4e8033f
commit 86de8bd5b1
2 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/sat/smt/polysat/viable.cpp
View file

@ -746,10 +746,17 @@ namespace polysat {
if (new_lo == new_hi) { if (new_lo == new_hi) {
IF_VERBOSE(0, verbose_stream() << "Check: always true " << "x*" << ne->coeff << " not in " << ne->interval << " " << new_hi << "\n"); if (lo < hi) {
// empty m_alloc.push_back(ne);
m_alloc.push_back(ne); return find_t::multiple;
return find_t::multiple; }
else {
SASSERT(hi < lo);
// exclude 0
IF_VERBOSE(0, display_one(verbose_stream() << "Exclude 0: ", v, ne) << "\n");
SASSERT(new_lo == 0);
new_hi = 1;
}
} }
ne->coeff = 1; ne->coeff = 1;

2
src/sat/smt/polysat_internalize.cpp
View file

@ -678,7 +678,7 @@ namespace polysat {
// e = hi lo // e = hi lo
// hi = 0 <=> e < 2^|lo| // hi = 0 <=> e < 2^|lo|
void solver::axioms_for_concat(app* e) { void solver::axioms_for_concat(app* e) {
if (e->get_num_args() == 2) { if (e->get_num_args() == 2) {
expr* hi = e->get_arg(0); expr* hi = e->get_arg(0);
auto sz_e = bv.get_bv_size(e); auto sz_e = bv.get_bv_size(e);