blob: c15ea9e0c84c1d91704f42d24a952a0a59313ad3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(set-option :incremental false)
(set-info :source "Generating minimum transitivity constraints in P-time for deciding Equality Logic,
Ofer Strichman and Mirron Rozanov,
SMT Workshop 2005.
Translator: Leonardo de Moura.")
(set-info :status unsat)
(set-info :category "crafted")
(set-info :difficulty "0")
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x0 () U)
(declare-fun y0 () U)
(declare-fun z0 () U)
(check-sat-assuming ( (not (= x0 x0)) ))
|
