z3
z3 copied to clipboard
Z3Prover
Massive space leak with simple sequence benchmark
The following benchmark is actually rather simple, in the sense that a simple substitution of variables should find the sat model relatively quickly. Indeed, up until Nov 29th, z3 quickly answered it correctly as sat. A fresh build of z3, however, seems to exhibit a massive space leak, consuming more and more memory by the second, and gets eventually killed on my Mac-computer.
(set-option :produce-models true)
(set-logic ALL)
(define-fun s1 () Int 0)
(define-fun s3 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
(define-fun s5 () Int 1)
(define-fun s7 () (Seq Int) (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7)))
(define-fun s15 () (Seq (Seq Int)) (seq.++ (seq.unit (seq.++ (seq.unit 8) (seq.unit 9) (seq.unit 10))) (seq.unit (seq.++ (seq.unit 11) (seq.unit 12) (seq.unit 13)))))
(define-fun s17 () Int 4)
(declare-fun s0 () (Seq (Seq Int))) ; tracks user variable "a"
(define-fun s2 () (Seq Int) (seq.nth s0 s1))
(define-fun s4 () Bool (= s2 s3))
(define-fun s6 () (Seq Int) (seq.nth s0 s5))
(define-fun s8 () Bool (= s6 s7))
(define-fun s9 () Int (seq.len s0))
(define-fun s10 () Int (- s9 s5))
(define-fun s11 () (Seq (Seq Int)) (seq.extract s0 s5 s10))
(define-fun s12 () Int (seq.len s11))
(define-fun s13 () Int (- s12 s5))
(define-fun s14 () (Seq (Seq Int)) (seq.extract s11 s5 s13))
(define-fun s16 () Bool (= s14 s15))
(define-fun s18 () Bool (= s9 s17))
(assert s4)
(assert s8)
(assert s16)
(assert s18)
(check-sat)
Update: Still observing the same memory behavior with z3 built this morning.
It performs conflicting simplifications that cancel the effect of the other. It accumulates the same equality again as a subgoal. I haven't figured out how to do this right, e.g., to enforce convergent simplifications. This is specific to nested sequences.