search

Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

Empty universes #7220

Closed remysucre closed 1 month ago

remysucre commented 1 month ago

The following program should be satisfied by the sort with the empty universe, but z3 returns unsat: 

(declare-sort T)
(assert (forall ((x T)) (not (= x x))))
(check-sat)
NikolajBjorner commented 1 month ago

This is not a bug. First-order simple sorted logic builds in that all sorts are non-empty.