search

uuverifiers / princess

The Princess Theorem Prover
Other
22 stars 4 forks source link

Unsoundness with quantifiers and ADTs #1

Closed pruemmer closed 2 years ago

pruemmer commented 2 years ago

Result should be unsat but is sat:

(set-logic ALL)
(declare-sort a 0)
(declare-datatypes ((prod 0)) (((Pair (gx a) (gy a)))))
(declare-fun p () prod)
(assert (forall ((x a) (y a)) (not (= p (Pair x y)))))
(check-sat)
pruemmer commented 2 years ago

This problem only occurs with option +incremental

pruemmer commented 2 years ago

Fixed