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

fix semantics of check-int64 div operation to align with smtlib semantics

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-29 04:29:38 -08:00
parent 30d72f79ac
commit ab43d2dcf1
2 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/sls/sls_context.cpp
View file

@ -25,6 +25,7 @@ Author:
#include "ast/sls/sls_seq_plugin.h" #include "ast/sls/sls_seq_plugin.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/for_each_expr.h"
#include "smt/params/smt_params_helper.hpp" #include "smt/params/smt_params_helper.hpp"
namespace sls { namespace sls {
@ -208,6 +209,10 @@ namespace sls {
if (bad_model) { if (bad_model) {
IF_VERBOSE(0, verbose_stream() << lit << " " << a->get_id() << " " << mk_bounded_pp(a, m) << " " << eval_a << "\n"); IF_VERBOSE(0, verbose_stream() << lit << " " << a->get_id() << " " << mk_bounded_pp(a, m) << " " << eval_a << "\n");
TRACE("sls", s.display(tout << lit << " " << a->get_id() << " " << mk_bounded_pp(a, m) << " " << eval_a << "\n");
for (expr* t : subterms::all(expr_ref(a, m)))
tout << "#" << t->get_id() << ": " << mk_bounded_pp(t, m) << " := " << ev(t) << "\n";
);
throw default_exception("failed to create a well-formed model"); throw default_exception("failed to create a well-formed model");
} }
} }

10
src/util/checked_int64.h
View file

@ -300,6 +300,16 @@ template<bool CHECK>
inline checked_int64<CHECK> div(checked_int64<CHECK> const& a, checked_int64<CHECK> const& b) { inline checked_int64<CHECK> div(checked_int64<CHECK> const& a, checked_int64<CHECK> const& b) {
checked_int64<CHECK> result(a); checked_int64<CHECK> result(a);
result /= b; result /= b;
if (a < 0) {
checked_int64<CHECK> r(a);
r %= b;
if (r != 0) {
if (b < 0)
result += 1;
else
result -= 1;
}
}
return result; return result;
} }