mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix intblast is_bounded (#7163)

Browse source
This commit is contained in:
Jakob Rath 2024-03-14 16:48:38 +01:00 • committed by GitHub
parent 0b3bbc2972
commit 5704e8d154
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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

@ -467,7 +467,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;
}); });
} }
@ -536,7 +536,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;