mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2022-07-21 13:00:36 +02:00
parent e168d8a2eb
commit 4a3fe8ab82
4 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/test/fixplex.cpp
View file

@ -5,6 +5,7 @@
#include "ast/reg_decl_plugins.h"
#include "smt/smt_kernel.h"
#include "smt/params/smt_params.h"
#include <iostream>
namespace polysat {

1
src/test/mod_interval.cpp
View file

@ -1,4 +1,5 @@
#include "math/interval/mod_interval_def.h"
#include <iostream>
static void test_interval1() {
mod_interval<uint64_t> i1(1, 2);

12
src/test/polysat.cpp
View file

@ -970,7 +970,7 @@ namespace polysat {
// quot_rem(2, 5) should have single solution (0, 2),
// but with the usual axioms we also get (3, 3).
s.add_eq(b * quot + rem - a);
s.add_noovfl(b, quot);
s.add_umul_noovfl(b, quot);
s.add_ult(rem, b);
// To force a solution that's different from the correct one.
s.add_diseq(quot - 0);
@ -1001,7 +1001,7 @@ namespace polysat {
// quot = udiv(a*123, 123)
s.add_eq(quot * y + rem - x);
s.add_diseq(a - quot);
s.add_noovfl(quot, y);
s.add_umul_noovfl(quot, y);
s.add_ult(rem, x);
s.check();
s.expect_sat();
@ -1017,11 +1017,11 @@ namespace polysat {
auto first = s.var(s.add_var(bw));
s.add_eq(q*idx + r, UINT_MAX);
s.add_ult(r, idx);
s.add_noovfl(q, idx);
s.add_umul_noovfl(q, idx);
s.add_ult(first, second);
s.add_diseq(idx, 0);
s.add_ule(second - first, q);
s.add_noovfl(second - first, idx);
s.add_umul_noovfl(second - first, idx);
s.check();
}
@ -1368,9 +1368,9 @@ namespace polysat {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
if (is_not)
s.add_ovfl(pa, pb);
s.add_umul_ovfl(pa, pb);
else
s.add_noovfl(pa, pb);
s.add_umul_noovfl(pa, pb);
}
else {
std::cout << "SKIP: " << mk_pp(fm, m) << "\n";