This project is read-only.

Sort error in proof


Consider the following SMT-LIB 2 problem:
(set-option :produce-proofs true)
(set-logic AUFLIA)
(declare-sort B$ 0)
(declare-sort A_set$ 0)
(declare-sort A_set_set$ 0)
(declare-sort A_set_set_set$ 0)
(declare-sort A_set_set_bool_fun$ 0)
(declare-fun a$ () B$)
(declare-fun uu$ (B$) A_set_set_bool_fun$)
(declare-fun uua$ () A_set_set_bool_fun$)
(declare-fun card$ (A_set$) Bool)
(declare-fun card$a (A_set_set_set$) Bool)
(declare-fun member$ (A_set$) A_set_set_bool_fun$)
(declare-fun collect$ (A_set_set_bool_fun$) A_set_set_set$)
(declare-fun fun_app$ (A_set_set_bool_fun$ A_set_set$) Bool)
(declare-fun partitions$ (A_set_set$ B$) Bool)
(assert (! (forall ((?v0 A_set_set$)) (! (= (fun_app$ uua$ ?v0) (and (partitions$ ?v0 a$) (forall ((?v1 A_set$)) (=> (fun_app$ (member$ ?v1) ?v0) (card$ ?v1))))) :pattern ((fun_app$ uua$ ?v0)))) :named a0))
(assert (! (forall ((?v0 B$) (?v1 A_set_set$)) (! (= (fun_app$ (uu$ ?v0) ?v1) (and (partitions$ ?v1 ?v0) (forall ((?v2 A_set$)) (=> (fun_app$ (member$ ?v2) ?v1) (card$ ?v2))))) :pattern ((fun_app$ (uu$ ?v0) ?v1)))) :named a1))
(assert (! (forall ((?v0 A_set_set_bool_fun$) (?v1 A_set_set_bool_fun$)) (=> (forall ((?v2 A_set_set$)) (= (fun_app$ ?v0 ?v2) (fun_app$ ?v1 ?v2))) (= (collect$ ?v0) (collect$ ?v1)))) :named a2))
(assert (! (forall ((?v0 B$)) (card$a (collect$ (uu$ ?v0)))) :named a3))
(assert (! (not (card$a (collect$ uua$))) :named a4))
The proof we obtain is sort-incorrect, whether we use an oldish version of Z3 from about one year ago or the latest repository version. In several places, the ill-sorted term
(fun_app$ (member$ ?v1) ?v1)
appears in it. However, ?v1 cannot be simultaneously of sort "A_set" and "A_set_set".


wintersteiger wrote May 30, 2016 at 3:09 PM

Z3 has moved to GitHub a long time ago, and the Codeplex pages or repositories are not in use anymore. At first glance, your problem still exists though. Could you please submit a new issue in our new issue tracker?