test/regress/regress0/uflia/diseqprop.04.smt


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

(benchmark test
:logic QF_UFLIA
:extrafuns ((f Int Int))
:extrafuns ((x1 Int))
:extrafuns ((y1 Int))
:extrafuns ((x2 Int))
:extrafuns ((y2 Int))

:extrafuns ((a Int))
:extrafuns ((b Int))

:assumption (= y1 y2) 

:assumption (= (f x1) (f y1))

:assumption (not (= x2 y2))
:assumption (= x1 x2)

:formula true
)