CODEWITHSUNDEEP
z3smtquantifiers
Pramod
Pramod

Reputation: 9456

Quantifier patterns in Z3

I am having trouble attempting to prove this fairly simple Z3 query.

(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(declare-fun sum (Int) Int)
(declare-fun list () (Array Int Int))
(declare-fun i0 () Int)
(declare-fun s0 () Int)
(declare-fun i1 () Int)
(declare-fun s1 () Int)
(assert (forall ((n Int))
  (! (or (not (<= n 0)) (= (sum n) 0)) 
     :pattern ((sum n)))))
(assert (forall ((n Int))
  (! (let ((a1 (= (sum n)
                   (+ (select list (- n 1))
                      (sum (- n 1))))))
       (or (<= n 0) a1))
     :pattern ((sum n)))))
(assert (>= i0 0))
(assert (= s0 (sum i0)))
(assert (= i1 (+ 1 i0)))
(assert (= s1 (+ 1 s0 (select list i0))))
(assert (not (= s1 (sum i1))))

(check-sat)

Seems to me that the final assertion should instantiate the second quantified statement for i1 while the assert involving s0 should instantiate the quantifiers for i0. These two should should easily lead to UNSAT.

However, Z3 returns unknown. What am I missing?

Upvotes: 0

Views: 337

Answers (1)

Pramod
Pramod

Reputation: 9456

Never mind, there was an silly error in my query.

This code:

(assert (= s1 (+ 1 s0 (select list i0))))

should have been:

(assert (= s1 (+ s0 (select list i0))))

Upvotes: 1

Related Questions