Skip to content

Commit c9ac626

Browse files
wabscalewabscale
committed
Add compile time smt to cxx compilation
1 parent 7e1b71b commit c9ac626

File tree

8 files changed

+715
-471
lines changed

8 files changed

+715
-471
lines changed

‎.gitignore

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,5 @@
11
*.swp
22
*.swo
3+
*.o
4+
smt
5+
bin

‎Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ smtlib-objs += SMTLIB/Messages.o
1414
smtlib-objs += SMTLIB/Float.o
1515
smtlib-objs += SMTLIB/NativeBitVector.o
1616

17-
smt: smt.o aes.o $(smtlib-objs)
17+
smt: theory.o smt.o aes.o $(smtlib-objs)
1818
nvcc $^ -o $@
1919

2020
all: smt

‎generate.sh

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
#!/usr/bin/env zsh
2+
3+
# Usage:
4+
# ./convert.sh file1.smt2
5+
#
6+
# -> theory.cu
7+
8+
set -e
9+
cd $(realpath $(dirname))
10+
mkdir -p bin
11+
12+
if [ "$#" = "0" ]; then
13+
echo 'Supply a theory file' 1>&2
14+
exit 1
15+
fi
16+
17+
18+
beginswith() { case $2 in "$1"*) true;; *) false;; esac; }
19+
format() { clang-format - }
20+
21+
22+
transpose() {
23+
sed 's/abort();/return 1;/' | \
24+
sed 's/extern "C" int/__device__ int/' | \
25+
sed 's/size != 32/size < 16/' | \
26+
sed 's/jfs_warning("Wrong sized input tried.\\n");//' | \
27+
sed 's/SMTLIB\/BitVector.h/SMTLIB\/BufferRef.h/' | \
28+
sed 's/#include/\/\/ #include/' | \
29+
sed 's/\/\/ Begin program/#include "theory.h"/'
30+
}
31+
32+
33+
smt2cxx() {
34+
docker run -it --rm -v $(pwd):/out -u $(id -u):$(id -g) \
35+
delcypher/jfs_build:fse_2019 /home/user/jfs/build/bin/jfs-smt2cxx \
36+
/out/${1}
37+
}
38+
39+
40+
41+
for filename in "$@"; do
42+
if beginswith http "${filename}"; then
43+
wget "${filename}" -O theory.smt2
44+
filename=theory.smt2
45+
fi
46+
smt2cxx "${filename}" | transpose | format > theory.cu
47+
make clean smt
48+
mv smt "bin/smt-$(echo ${filename} | tr '.' '-')"
49+
done

‎smt.cu

Lines changed: 19 additions & 470 deletions
Large diffs are not rendered by default.

‎smt.h

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#ifndef SMT_H
2+
#define SMT_H
3+
4+
#include "SMTLIB/BufferRef.h"
5+
#include "SMTLIB/Float.h"
6+
#include "cuda_aes.h"
7+
8+
// Threads per block
9+
#define N 1024
10+
// Number of blocks
11+
#define M 65536
12+
13+
inline void gpuAssert(cudaError_t code, const char *file, int line, bool abort = true);
14+
#define gpuErrchk(ans) { gpuAssert((ans), __FILE__, __LINE__); }
15+
16+
#endif

‎theory.cu

Lines changed: 389 additions & 0 deletions
Large diffs are not rendered by default.

‎theory.h

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#ifndef THEORY_H
2+
#define THEORY_H
3+
4+
#include "SMTLIB/BufferRef.h"
5+
#include "SMTLIB/Float.h"
6+
#include <stdio.h>
7+
8+
extern __device__ int solved;
9+
extern volatile int finished_dev;
10+
11+
// Size of all variables needed by the SMT formula, in bytes
12+
__device__ int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size);
13+
14+
#endif

‎theory.smt2

Lines changed: 224 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,224 @@
1+
(set-info :smt-lib-version 2.6)
2+
(set-logic QF_FP)
3+
(set-info :category "crafted")
4+
(set-info :source |Alberto Griggio <[email protected]>. These benchmarks were used for the evaluation in the following paper: L. Haller, A. Griggio, M. Brain, D. Kroening: Deciding floating-point logic with systematic abstraction. FMCAD 2012. Real-numbered literals have been automatically translated by MathSAT|)
5+
(set-info :status sat)
6+
;; MathSAT API call trace
7+
;; generated on 05/20/15 17:24:57
8+
9+
(declare-fun x0 () (_ FloatingPoint 8 24))
10+
(declare-fun x1 () (_ FloatingPoint 8 24))
11+
(declare-fun x2 () (_ FloatingPoint 8 24))
12+
(declare-fun x3 () (_ FloatingPoint 8 24))
13+
(declare-fun x4 () (_ FloatingPoint 8 24))
14+
(declare-fun x5 () (_ FloatingPoint 8 24))
15+
(declare-fun x6 () (_ FloatingPoint 8 24))
16+
(define-fun _t_10 () (_ FloatingPoint 8 24) (fp #b0 #b10000010 #b01000000000000000000000))
17+
(define-fun _t_12 () (_ FloatingPoint 8 24) (fp #b1 #b10000010 #b01000000000000000000000))
18+
(define-fun _t_13 () (_ FloatingPoint 8 24) x0)
19+
(define-fun _t_14 () Bool (fp.leq _t_12 _t_13))
20+
(define-fun _t_15 () Bool (fp.leq _t_13 _t_10))
21+
(define-fun _t_16 () Bool (and _t_14 _t_15))
22+
(assert _t_16)
23+
(define-fun _t_17 () (_ FloatingPoint 8 24) x1)
24+
(define-fun _t_18 () Bool (fp.leq _t_12 _t_17))
25+
(define-fun _t_19 () Bool (fp.leq _t_17 _t_10))
26+
(define-fun _t_20 () Bool (and _t_18 _t_19))
27+
(assert _t_20)
28+
(define-fun _t_21 () (_ FloatingPoint 8 24) x2)
29+
(define-fun _t_22 () Bool (fp.leq _t_12 _t_21))
30+
(define-fun _t_23 () Bool (fp.leq _t_21 _t_10))
31+
(define-fun _t_24 () Bool (and _t_22 _t_23))
32+
(assert _t_24)
33+
(define-fun _t_25 () (_ FloatingPoint 8 24) x3)
34+
(define-fun _t_26 () Bool (fp.leq _t_12 _t_25))
35+
(define-fun _t_27 () Bool (fp.leq _t_25 _t_10))
36+
(define-fun _t_28 () Bool (and _t_26 _t_27))
37+
(assert _t_28)
38+
(define-fun _t_29 () (_ FloatingPoint 8 24) x4)
39+
(define-fun _t_30 () Bool (fp.leq _t_12 _t_29))
40+
(define-fun _t_31 () Bool (fp.leq _t_29 _t_10))
41+
(define-fun _t_32 () Bool (and _t_30 _t_31))
42+
(assert _t_32)
43+
(define-fun _t_33 () (_ FloatingPoint 8 24) x5)
44+
(define-fun _t_34 () Bool (fp.leq _t_12 _t_33))
45+
(define-fun _t_35 () Bool (fp.leq _t_33 _t_10))
46+
(define-fun _t_36 () Bool (and _t_34 _t_35))
47+
(assert _t_36)
48+
(define-fun _t_37 () (_ FloatingPoint 8 24) x6)
49+
(define-fun _t_38 () Bool (fp.leq _t_12 _t_37))
50+
(define-fun _t_39 () Bool (fp.leq _t_37 _t_10))
51+
(define-fun _t_40 () Bool (and _t_38 _t_39))
52+
(assert _t_40)
53+
(define-fun _t_3 () RoundingMode RNE)
54+
(define-fun _t_42 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
55+
(define-fun _t_44 () (_ FloatingPoint 8 24) (fp #b0 #b01111100 #b10011011101001011110010))
56+
(define-fun _t_46 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b10110011001100110011001))
57+
(define-fun _t_47 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_13 _t_46))
58+
(define-fun _t_48 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_42 _t_47))
59+
(define-fun _t_51 () (_ FloatingPoint 8 24) (fp #b1 #b01111101 #b11000010100011110101101))
60+
(define-fun _t_52 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_17 _t_51))
61+
(define-fun _t_53 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_48 _t_52))
62+
(define-fun _t_56 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b00000001100010010011100))
63+
(define-fun _t_57 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_21 _t_56))
64+
(define-fun _t_58 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_53 _t_57))
65+
(define-fun _t_61 () (_ FloatingPoint 8 24) (fp #b1 #b01111011 #b10011101101100100010110))
66+
(define-fun _t_62 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_25 _t_61))
67+
(define-fun _t_63 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_58 _t_62))
68+
(define-fun _t_66 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b00111101111100111011011))
69+
(define-fun _t_67 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_29 _t_66))
70+
(define-fun _t_68 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_63 _t_67))
71+
(define-fun _t_71 () (_ FloatingPoint 8 24) (fp #b1 #b01111010 #b10110010001011010000111))
72+
(define-fun _t_72 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_33 _t_71))
73+
(define-fun _t_73 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_68 _t_72))
74+
(define-fun _t_75 () (_ FloatingPoint 8 24) (fp #b0 #b01111101 #b00101100000010000011001))
75+
(define-fun _t_76 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_37 _t_75))
76+
(define-fun _t_77 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_73 _t_76))
77+
(define-fun _t_78 () Bool (fp.leq _t_77 _t_44))
78+
(assert _t_78)
79+
(define-fun _t_80 () (_ FloatingPoint 8 24) (fp #b0 #b01111010 #b00100110111010010111011))
80+
(define-fun _t_82 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b11000001100010010011100))
81+
(define-fun _t_83 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_13 _t_82))
82+
(define-fun _t_84 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_42 _t_83))
83+
(define-fun _t_87 () (_ FloatingPoint 8 24) (fp #b1 #b01111100 #b01111000110101001111110))
84+
(define-fun _t_88 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_17 _t_87))
85+
(define-fun _t_89 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_84 _t_88))
86+
(define-fun _t_91 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b01011111101111100111011))
87+
(define-fun _t_92 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_21 _t_91))
88+
(define-fun _t_93 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_89 _t_92))
89+
(define-fun _t_96 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b10111101011100001010001))
90+
(define-fun _t_97 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_25 _t_96))
91+
(define-fun _t_98 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_93 _t_97))
92+
(define-fun _t_101 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b01110111110011101101100))
93+
(define-fun _t_102 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_29 _t_101))
94+
(define-fun _t_103 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_98 _t_102))
95+
(define-fun _t_106 () (_ FloatingPoint 8 24) (fp #b1 #b01111101 #b11100001010001111010110))
96+
(define-fun _t_107 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_33 _t_106))
97+
(define-fun _t_108 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_103 _t_107))
98+
(define-fun _t_110 () (_ FloatingPoint 8 24) (fp #b0 #b01111101 #b00000010000011000100101))
99+
(define-fun _t_111 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_37 _t_110))
100+
(define-fun _t_112 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_108 _t_111))
101+
(define-fun _t_113 () Bool (fp.leq _t_80 _t_112))
102+
(assert _t_113)
103+
(define-fun _t_115 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b11111000110101001111110))
104+
(define-fun _t_117 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b01001000001100010010011))
105+
(define-fun _t_118 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_13 _t_117))
106+
(define-fun _t_119 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_42 _t_118))
107+
(define-fun _t_122 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b01011000100100110111001))
108+
(define-fun _t_123 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_17 _t_122))
109+
(define-fun _t_124 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_119 _t_123))
110+
(define-fun _t_127 () (_ FloatingPoint 8 24) (fp #b1 #b01111100 #b10010101100000010000011))
111+
(define-fun _t_128 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_21 _t_127))
112+
(define-fun _t_129 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_124 _t_128))
113+
(define-fun _t_131 () (_ FloatingPoint 8 24) (fp #b0 #b01111101 #b00001011010000111001010))
114+
(define-fun _t_132 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_25 _t_131))
115+
(define-fun _t_133 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_129 _t_132))
116+
(define-fun _t_135 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b10010111100011010101000))
117+
(define-fun _t_136 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_29 _t_135))
118+
(define-fun _t_137 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_133 _t_136))
119+
(define-fun _t_139 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b10111001110110110010001))
120+
(define-fun _t_140 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_33 _t_139))
121+
(define-fun _t_141 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_137 _t_140))
122+
(define-fun _t_144 () (_ FloatingPoint 8 24) (fp #b1 #b01111100 #b01011000000100000110000))
123+
(define-fun _t_145 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_37 _t_144))
124+
(define-fun _t_146 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_141 _t_145))
125+
(define-fun _t_147 () Bool (fp.leq _t_146 _t_115))
126+
(assert _t_147)
127+
(define-fun _t_149 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b00010011011101001011110))
128+
(define-fun _t_151 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b11101101100100010110100))
129+
(define-fun _t_152 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_13 _t_151))
130+
(define-fun _t_153 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_42 _t_152))
131+
(define-fun _t_156 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b01110000001000001100001))
132+
(define-fun _t_157 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_17 _t_156))
133+
(define-fun _t_158 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_153 _t_157))
134+
(define-fun _t_161 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b10100100010110100001110))
135+
(define-fun _t_162 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_21 _t_161))
136+
(define-fun _t_163 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_158 _t_162))
137+
(define-fun _t_165 () (_ FloatingPoint 8 24) (fp #b0 #b01111101 #b11110111110011101101100))
138+
(define-fun _t_166 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_25 _t_165))
139+
(define-fun _t_167 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_163 _t_166))
140+
(define-fun _t_169 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b10111001110110110010001))
141+
(define-fun _t_170 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_29 _t_169))
142+
(define-fun _t_171 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_167 _t_170))
143+
(define-fun _t_173 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b11100100110111010011000))
144+
(define-fun _t_174 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_33 _t_173))
145+
(define-fun _t_175 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_171 _t_174))
146+
(define-fun _t_178 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b01111001110110110010001))
147+
(define-fun _t_179 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_37 _t_178))
148+
(define-fun _t_180 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_175 _t_179))
149+
(define-fun _t_181 () Bool (fp.leq _t_149 _t_180))
150+
(assert _t_181)
151+
(define-fun _t_184 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b11101110100101111000110))
152+
(define-fun _t_187 () (_ FloatingPoint 8 24) (fp #b1 #b01111101 #b10000011000100100110110))
153+
(define-fun _t_188 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_13 _t_187))
154+
(define-fun _t_189 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_42 _t_188))
155+
(define-fun _t_191 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b10010011111101111100110))
156+
(define-fun _t_192 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_17 _t_191))
157+
(define-fun _t_193 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_189 _t_192))
158+
(define-fun _t_195 () (_ FloatingPoint 8 24) (fp #b0 #b01111100 #b01101110100101111000111))
159+
(define-fun _t_196 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_21 _t_195))
160+
(define-fun _t_197 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_193 _t_196))
161+
(define-fun _t_199 () (_ FloatingPoint 8 24) (fp #b0 #b01111100 #b00111101011100001010010))
162+
(define-fun _t_200 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_25 _t_199))
163+
(define-fun _t_201 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_197 _t_200))
164+
(define-fun _t_203 () (_ FloatingPoint 8 24) (fp #b0 #b01111101 #b00100110111010010111100))
165+
(define-fun _t_204 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_29 _t_203))
166+
(define-fun _t_205 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_201 _t_204))
167+
(define-fun _t_207 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b11101100000010000011001))
168+
(define-fun _t_208 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_33 _t_207))
169+
(define-fun _t_209 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_205 _t_208))
170+
(define-fun _t_212 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b00101000111101011100001))
171+
(define-fun _t_213 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_37 _t_212))
172+
(define-fun _t_214 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_209 _t_213))
173+
(define-fun _t_215 () Bool (fp.leq _t_214 _t_184))
174+
(assert _t_215)
175+
(define-fun _t_218 () (_ FloatingPoint 8 24) (fp #b1 #b01111101 #b01100000010000011000101))
176+
(define-fun _t_220 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b11011000100100110111001))
177+
(define-fun _t_221 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_13 _t_220))
178+
(define-fun _t_222 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_42 _t_221))
179+
(define-fun _t_224 () (_ FloatingPoint 8 24) (fp #b0 #b01111100 #b11111101111100111011011))
180+
(define-fun _t_225 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_17 _t_224))
181+
(define-fun _t_226 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_222 _t_225))
182+
(define-fun _t_228 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b00001110010101100000001))
183+
(define-fun _t_229 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_21 _t_228))
184+
(define-fun _t_230 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_226 _t_229))
185+
(define-fun _t_233 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b11011001000101101000100))
186+
(define-fun _t_234 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_25 _t_233))
187+
(define-fun _t_235 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_230 _t_234))
188+
(define-fun _t_237 () (_ FloatingPoint 8 24) (fp #b0 #b01111100 #b00111001010110000000111))
189+
(define-fun _t_238 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_29 _t_237))
190+
(define-fun _t_239 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_235 _t_238))
191+
(define-fun _t_242 () (_ FloatingPoint 8 24) (fp #b1 #b01111101 #b10100001110010101100000))
192+
(define-fun _t_243 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_33 _t_242))
193+
(define-fun _t_244 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_239 _t_243))
194+
(define-fun _t_246 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b01101111000110101010000))
195+
(define-fun _t_247 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_37 _t_246))
196+
(define-fun _t_248 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_244 _t_247))
197+
(define-fun _t_249 () Bool (fp.leq _t_218 _t_248))
198+
(assert _t_249)
199+
(define-fun _t_251 () (_ FloatingPoint 8 24) (fp #b0 #b01111101 #b11011101001011110001100))
200+
(define-fun _t_253 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b00000110001001001101110))
201+
(define-fun _t_254 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_13 _t_253))
202+
(define-fun _t_255 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_42 _t_254))
203+
(define-fun _t_257 () (_ FloatingPoint 8 24) (fp #b0 #b01111011 #b10000101000111101011100))
204+
(define-fun _t_258 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_17 _t_257))
205+
(define-fun _t_259 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_255 _t_258))
206+
(define-fun _t_261 () (_ FloatingPoint 8 24) (fp #b0 #b01111101 #b10000001000001100010010))
207+
(define-fun _t_262 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_21 _t_261))
208+
(define-fun _t_263 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_259 _t_262))
209+
(define-fun _t_265 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b01100001110010101100000))
210+
(define-fun _t_266 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_25 _t_265))
211+
(define-fun _t_267 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_263 _t_266))
212+
(define-fun _t_269 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b01000011100101011000001))
213+
(define-fun _t_270 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_29 _t_269))
214+
(define-fun _t_271 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_267 _t_270))
215+
(define-fun _t_274 () (_ FloatingPoint 8 24) (fp #b1 #b01111110 #b00001010110000001000001))
216+
(define-fun _t_275 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_33 _t_274))
217+
(define-fun _t_276 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_271 _t_275))
218+
(define-fun _t_278 () (_ FloatingPoint 8 24) (fp #b0 #b01111110 #b01011111001110110110001))
219+
(define-fun _t_279 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_37 _t_278))
220+
(define-fun _t_280 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_276 _t_279))
221+
(define-fun _t_281 () Bool (fp.leq _t_251 _t_280))
222+
(assert _t_281)
223+
(check-sat)
224+
(exit)

0 commit comments

Comments
 (0)