mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-30 01:48:45 +00:00
Code Activity

fix intblast is_bounded

Browse source
This commit is contained in:
Jakob Rath 2024-03-13 12:37:37 +01:00
parent d07d57c240
commit 8a16631fd1
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/intblast_solver.cpp
View file

@ -523,7 +523,7 @@ namespace intblast {
bool solver::is_bounded(expr* x, rational const& N) { bool solver::is_bounded(expr* x, rational const& N) {
return any_of(m_vars, [&](expr* v) { return any_of(m_vars, [&](expr* v) {
return is_translated(v) && translated(v) == x && bv.get_bv_size(v) <= N; return is_translated(v) && translated(v) == x && bv_size(v) <= N;
}); });
} }
@ -592,7 +592,7 @@ namespace intblast {
* Perform simplifications that are claimed sound when the bit-vector interpretations of * Perform simplifications that are claimed sound when the bit-vector interpretations of
* mod/div always guard the mod and dividend to be non-zero. * mod/div always guard the mod and dividend to be non-zero.
* Potentially shady area is for arithmetic expressions created by int2bv. * Potentially shady area is for arithmetic expressions created by int2bv.
* They will be guarded by a modulus which dose not disappear. * They will be guarded by a modulus which does not disappear.
*/ */
expr* solver::amod(expr* bv_expr, expr* x, rational const& N) { expr* solver::amod(expr* bv_expr, expr* x, rational const& N) {
rational v; rational v;