8000 Wrong result "unsat" for Spacer · Issue #7554 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Wrong result "unsat" for Spacer #7554

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact 8000 its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
jena-kling opened this issue Feb 13, 2025 · 3 comments
Closed

Wrong result "unsat" for Spacer #7554

jena-kling opened this issue Feb 13, 2025 · 3 comments
Assignees
@agurfinkel
Labels
qe qel

Comments

@jena-kling
Copy link

Hello guys,

I think I found another bug for Spacer where it erroneously returns unsat. This seems to be connected to inlining of rules :

(set-logic HORN)

(declare-fun inv1 (Int Int Int) Bool)
(declare-fun u_pred (Int) Bool)

(assert (u_pred 0))
(assert (inv1 0 0 8))
(assert (forall ((D (Array Int Int)) (F Int) (H Int))
  (=> (inv1 F 0 8) (inv1 (+ 1 F) H (select (store D F 0) H)))))
(assert (forall ((D Int)) (=> (and (inv1 1 D 8) (u_pred D)) false)))

(check-sat)

Specifically I executed:

$ z3 fp.xform.inline_eager=false test.smt2 
unsat

$ z3 --version
Z3 version 4.13.4 - 64 bit - build hashcode 943d881340fc77496dcfc75d9ba65a617a51475e
@NikolajBjorner
Copy link
Contributor
NikolajBjorner commented Feb 18, 2025 •
edited
Loading

Looks like blame is EMBP for Arrays:

-------- [spacer] spacer::pred_transformer::mk_rf C:\z3\src\muz\spacer\spacer_context.cpp:3970 ---------
Reach fact, before QE:
(and (= inv1_2_0 8)
     (= inv1_0_n (+ 1 inv1_0_0))
     (= inv1_0_0 0)
     (= inv1_1_0 0)
     (= inv1_2_n (select (store aux!1_n inv1_0_0 0) inv1_1_n)))
Vars:

inv1_0_0
inv1_1_0
inv1_2_0
aux!1_n
------------------------------------------------
-------- [spacer] spacer::pred_transformer::mk_rf C:\z3\src\muz\spacer\spacer_context.cpp:3984 ---------
Reach fact, after QE project:
(= inv1_0_n 1)
Vars:

------------------------------------------------

Let us call the state variables x, y, z, x', y', z', with array A.

Then it says x = y = 0, z = 8, x' = x + 1, z' = A[x -> 0][y']
Project everything but x', y', z'.
If x = y' then z' = 0. So, the projection must have either x' -1 != y' or z' = 0
The projection has x' = 1 as expected from x' = x + 1.

Tracing with qe, it narrows to mbp_tg:

-------- [qe] qe::mbproj::impl::spacer_qel C:\z3\src\qe\qe_mbp.cpp:555 ---------
Before projection:
(and (= inv1_2_0 8)
     (= inv1_0_n (+ 1 inv1_0_0))
     (= inv1_0_0 0)
     (= inv1_1_0 0)
     (= inv1_2_n (select (store aux!1_n inv1_0_0 0) inv1_1_n)))
Vars: 
inv1_0_0
inv1_1_0
inv1_2_0
aux!1_n
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_2_0 := 8
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_2_0 := 8
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_0_0 := (+ inv1_0_n (* (- 1) 1))
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_0_0 := (+ (* (- 1) 1) inv1_0_n)
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_1_0 := 0
------------------------------------------------
-------- [qe] mbp::arith_solve_plugin::solve C:\z3\src\qe\mbp\mbp_solve_plugin.cpp:103 ---------
inv1_1_0 := 0
------------------------------------------------
-------- [qe] qe::mbproj::impl::do_qel C:\z3\src\qe\qe_mbp.cpp:532 ---------
After qel:
(and (= 1 inv1_0_n) (= inv1_2_n (select (store aux!1_n 0 0) inv1_1_n)))
Vars: 
aux!1_n
------------------------------------------------
-------- [qe] qe::mbproj::impl::qel_project C:\z3\src\qe\qe_mbp.cpp:551 ---------
After mbp_tg:
(= inv1_0_n 1) models 1
Vars: 
------------------------------------------------
-------- [spacer] spacer::pred_transformer::mk_rf C:\z3\src\muz\spacer\spacer_context.cpp:3984 ---------
Reach fact, after QE project:
(= inv1_0_n 1)
Vars:

@NikolajBjorner
Copy link
Contributor

@hgvk94

@NikolajBjorner
Copy link
Contributor

m_use_mdl is false when mbp_arrays_tg is invoked.
Then the rule for eliminating read-writes is not invoked.

z3/src/qe/mbp/mbp_arrays_tg.cpp

Line 364 in 42f6e13

if (m_use_mdl && is_rd_wr(nt)) {

If you force m_use_mdl = true, we get the right results.

arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
fix Z3Prover#7554
d56b69b 
mbp_qel  uses two iterations of saturation.
The first iteration uses only congruences, not the model.
The second iteration uses the model.
Terms are marked as "seen" during either iteration and will not be reprocessed if they are "seen".
All select terms get marked as "seen" to avoid reproducing Ackerman axioms.
But this conflicts with expanding select-store axioms during
the phase of saturation where use_model is allowed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@agurfinkel agurfinkel

Labels
qe qel
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@NikolajBjorner @agurfinkel @jena-kling
0