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


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

(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 (= x1 x2)
:assumption (= y1 y2) 

:assumption (= x2 1)
:assumption (= y2 2)

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

:formula true
)