blob: ef44444b71d7391dbbc80e0e3c179fc2e3395a12 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
(benchmark fuzzsmt
:logic QF_LRA
:extrafuns ((v0 Real))
:extrafuns ((v2 Real))
:extrafuns ((v1 Real))
:status sat
:formula
(let (?n1 2)
(let (?n2 (* ?n1 ?n1))
(let (?n3 (~ v0))
(let (?n4 (* ?n1 ?n3))
(let (?n5 (- ?n1 ?n1))
(let (?n6 (- ?n5 v0))
(let (?n7 (- ?n4 ?n6))
(flet ($n8 (= ?n2 ?n7))
(flet ($n9 false)
(let (?n10 (ite $n9 ?n1 v1))
(let (?n11 (+ ?n1 v2))
(flet ($n12 (= ?n10 ?n11))
(let (?n13 (ite $n9 v0 ?n2))
(let (?n14 (~ ?n1))
(let (?n15 (ite $n9 ?n14 ?n1))
(flet ($n16 (= ?n13 ?n15))
(flet ($n17 (= ?n1 ?n7))
(let (?n18 (+ ?n1 ?n1))
(flet ($n19 (= v2 ?n18))
(let (?n20 (ite $n19 v2 ?n1))
(let (?n21 (ite $n17 ?n18 ?n20))
(flet ($n22 (= ?n21 ?n2))
(let (?n23 (ite $n9 ?n21 ?n2))
(flet ($n24 (= ?n23 ?n1))
(flet ($n25 (= ?n7 ?n2))
(flet ($n26 (iff $n24 $n25))
(let (?n27 (~ ?n7))
(flet ($n28 (= ?n27 ?n1))
(let (?n29 (ite $n28 ?n1 ?n1))
(flet ($n30 (= ?n1 ?n29))
(flet ($n31 (implies $n26 $n30))
(flet ($n32 (implies $n9 $n9))
(flet ($n33 (if_then_else $n22 $n31 $n32))
(flet ($n34 (and $n9 $n33))
(flet ($n35 (if_then_else $n16 $n34 $n9))
(flet ($n36 (iff $n12 $n35))
(flet ($n37 (and $n8 $n36))
$n37
))))))))))))))))))))))))))))))))))))))
|
