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

handle exception internally, avoid passing rationals to integer operations

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-28 20:09:59 -08:00
parent 5b175c1bcd
commit fe5d17d515
2 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/sls/sls_arith_base.cpp
View file

@ -586,6 +586,8 @@ namespace sls {
if (mx == 0) if (mx == 0)
continue; continue;
auto valmx = divide(x, val, mx); auto valmx = divide(x, val, mx);
if (p > 1 && !is_int(x))
continue;
auto r = root_of(p, valmx); auto r = root_of(p, valmx);
add_update(x, r - value(x)); add_update(x, r - value(x));
if (p % 2 == 0) if (p % 2 == 0)
@ -1786,7 +1788,9 @@ namespace sls {
// val / mx = x^p // val / mx = x^p
if (mx == 0) if (mx == 0)
continue; continue;
auto valmx = divide(x, val, mx); if (p > 1 && !is_int(x))
continue;
auto valmx = divide(x, val, mx);
auto r = root_of(p, valmx); auto r = root_of(p, valmx);
add_update(x, r - value(x)); add_update(x, r - value(x));
if (p % 2 == 0) if (p % 2 == 0)

8
src/ast/sls/sls_smt_plugin.cpp
View file

@ -101,7 +101,13 @@ namespace sls {
void smt_plugin::run() { void smt_plugin::run() {
if (!m_ddfw) if (!m_ddfw)
return; return;
m_result = m_ddfw->check(0, nullptr); try {
m_result = m_ddfw->check(0, nullptr);
}
catch (std::exception& ex) {
IF_VERBOSE(0, verbose_stream() << "sls-exception " << ex.what() << "\n");
m_result = l_undef;
}
IF_VERBOSE(3, verbose_stream() << "sls-result " << m_result << "\n"); IF_VERBOSE(3, verbose_stream() << "sls-result " << m_result << "\n");
for (auto v : m_shared_bool_vars) { for (auto v : m_shared_bool_vars) {
auto w = m_smt_bool_var2sls_bool_var[v]; auto w = m_smt_bool_var2sls_bool_var[v];