mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-20 02:00:22 +00:00
Code Activity

check for internalized in solve_for

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-08-17 16:50:28 -07:00
parent 4082e4e56a
commit ff74af7eaa
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_lra.cpp
View file

@ -1296,10 +1296,14 @@ public:
// q = 0 or p = (p mod q) + q * (p div q)
// q = 0 or (p mod q) >= 0
// q = 0 or (p mod q) < abs(q)
// q >= 0 or (p mod q) = (p mod -q)
mk_axiom(eqz, eq);
mk_axiom(eqz, mod_ge_0);
mk_axiom(eqz, mod_lt_q);
// if (!a.is_uminus(q))
// mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q)))));
m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p));
if (a.is_zero(p)) {
@ -3732,6 +3736,8 @@ public:
unsigned_vector vars;
unsigned j = 0;
for (auto [e, t, g] : solutions) {
if (!ctx().e_internalized(e))
continue;
auto n = get_enode(e);
if (!n) {
solutions[j++] = { e, t, g };