8000 Spacer: New bug after previous fix? · Issue #7566 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Spacer: New bug after previous fix? #7566

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintaine 8000 rs 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 24, 2025 · 1 comment
Closed

Spacer: New bug after previous fix? #7566

jena-kling opened this issue Feb 24, 2025 · 1 comment
Assignees
@agurfinkel
Labels
qel

Comments

@jena-kling
Copy link

Hello

thanks a lot for fixing my previous bug reports. I think one fix however introduced a new issue:
For the following CHC-instance z3 returns erroneously sat:

(set-logic HORN)
(declare-datatypes ((item 0)) (((item (data Int)))))
(declare-datatypes ((HeapObject 0)) (((O_item (getitem item)) (defObj))))
(declare-datatypes ((Heap 0)) (((HeapCtor  (HeapContents (Array Int HeapObject))))))

(declare-fun atom1 () Bool)
(declare-fun atom2 () Bool)
(declare-fun atom3 () Bool)
(declare-fun inv_main21873min (Heap) Bool)
(declare-fun u (Int) Bool)

(assert (u 1))
(assert (=> atom3 atom1))
(assert (=> atom3 (u 9)))
(assert (forall ((h Heap)) (=> (and atom1 (inv_main21873min h)) false)))
(assert (forall ((h Heap) (hh Heap) (idx Int) (p Heap))
  (let 
    ((a!2 
      (ite 
        (> idx 0)
        (select (HeapContents p) 1)
        defObj)))
    (=> 
      (and 
        (= h (ite  (> idx 0) (HeapCtor (store (HeapContents hh) idx defObj)) hh))
        ((_ is O_item) a!2)
        (= hh (ite  (> (data (getitem a!2)) 0) (HeapCtor (store (HeapContents p) (data (getitem a!2)) defObj)) p))) 
      (inv_main21873min h)))))

(assert (forall ((h Heap) (b Bool) (hh Heap))
    (=> 
      (and 
        (inv_main21873min hh)
        (= h (ite b (HeapCtor (store (HeapContents hh) 1 defObj)) hh))
        ((_ is O_item) (ite  b (select (HeapContents hh) 1) defObj)))  
      (inv_main21873min h))))
(assert (=> atom2 atom3))
(assert (forall ((arr (Array Int HeapObject)))
  (=> 
    ( and atom2 (= defObj (select arr 0))) 
    atom3)))
(assert (forall ((i Int)) (=> (u i) atom2)))

(check-sat)

When using the latest version of z3 I get

$ ~/z3/build/z3 test.smt2 
sat

However this instance is unsat and before commit f50f211 (fixing #7505) z3 was able to give the correct answer:

$ ~/z3-bd3d288a085b1543e8130983be7e1bc1d1becb9f/build/z3 test.smt2
unsat
@NikolajBjorner
Copy link
Contributor
NikolajBjorner commented Feb 25, 2025 •
edited
Loading

@hgvk94 - this asserts if you run it with

  • z3 7566.smt2 /v:2 /tr:mbp /tr:spacer /tr:qe

ASSERTION VIOLATION
File: C:\z3\src\qe\qe_mbp.cpp
Line: 607
!eval.is_false(fml)

-------- [qe] qe::mbproj::impl::qel_project C:\z3\src\qe\qe_mbp.cpp:551 ---------
After mbp_tg:
false models 0
Vars:

NikolajBjorner added a commit that referenced this issue Feb 25, 2025
@NikolajBjorner
fix regression, missing idx increment in iterator loop #7566
db997cd
arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
fix regression, missing idx increment in iterator loop Z3Prover#7566
eec4a59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@agurfinkel agurfinkel

Labels
qel
Projects
None yet
Milestone
No milestone
Development

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