test/regress/regress0/uf/eq_diamond1.smt


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

(benchmark eq_diamond1
:source{
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
Ofer Strichman and Mirron Rozanov,
SMT Workshop 2005.

Translator: Leonardo de Moura. }
:status unsat
:category { crafted }
:logic QF_UF
:difficulty { 0 }
:extrafuns ((x0 U) (y0 U) (z0 U)
)
:formula (and 
(not (= x0 x0))))