Bug and patch
23 views
Skip to first unread message
Edward Schwartz
Oct 11, 2011, 10:15:38 AM10/11/11
to stp-users
There's a simple bug in the CVC parser that was causing stp to crash for us. Here's the error as told by valgrind:
ed@ed-Ubu64:/tmp/0x00020e6f.0x223c0f19-3$ valgrind stp -v http---graphics8.nytimes.com-adx-images-ADS-25-81-ad.258131-12.18.10_TB_HL_LivingRoom.jpg.6.0x009c4a60.stp
==8888== Memcheck, a memory error detector
==8888== Copyright (C) 2002-2010, and GNU GPL'd, by Julian Seward et al.
==8888== Using Valgrind-3.6.1 and LibVEX; rerun with -h for copyright info
==8888== Command: stp -v http---graphics8.nytimes.com-adx-images-ADS-25-81-ad.258131-12.18.10_TB_HL_LivingRoom.jpg.6.0x009c4a60.stp
==8888==
==8888== Mismatched free() / delete / delete []
==8888== at 0x4C27FFF: operator delete(void*) (vg_replace_malloc.c:387)
==8888== by 0x4389F0: cvcparse(void*) (cvc.y:1080)
==8888== by 0x40606F: main (main.cpp:530)
==8888== Address 0x5d4b400 is 0 bytes inside a block of size 10 alloc'd
==8888== at 0x4C28FAC: malloc (vg_replace_malloc.c:236)
==8888== by 0x56522F1: strdup (strdup.c:43)
==8888== by 0x42DDB6: cvclex() (cvc.lex:152)
==8888== by 0x4359F1: cvcparse(void*) (parsecvc.cpp:1816)
==8888== by 0x40606F: main (main.cpp:530)
Here's the simple patch:
--- src/parser/cvc.y (revision 1401)
+++ src/parser/cvc.y (working copy)
@@ -1077,7 +1077,7 @@
//2. Ensure that LET variables are not
//2. defined more than once
parserInterface->letMgr.LetExprMgr($1,*$3);
- delete $1;
+ free($1);
delete $3;
}
| STRING_TOK ':' Type '=' Expr
Trevor Hansen
Oct 11, 2011, 8:21:07 PM10/11/11
to stp-users
Hi Edward,
> There's a simple bug in the CVC parser that was causing stp to crash for us.
> Here's the error as told by valgrind:
Thanks for the patch. It's fixed in revision 1402.
Trevor.
> Here's a triggering input:http://plaid.cylab.cmu.edu:8080/~ed/http---graphics8.nytimes.com-adx-...
> There's a simple bug in the CVC parser that was causing stp to crash for us.
> Here's the error as told by valgrind:
Trevor.
Trevor Hansen
Oct 23, 2011, 8:26:38 AM10/23/11
to stp-users
Hi Edward,
I've looked more at your testcase.
STP does particularly badly on it because STP only does abstraction-
refinement of array-reads. It rewrites all the array-writes away
before it begins its abstraction refinement. Solvers like Boolector
and Sonolar also do abstraction refinement on array-writes. Version
0.1 of STP did array-write abstraction/refinement, but it's not
currently working.
Rewriting away the array-writes can introduce a quadratic number of
extra nodes. It does that on your problem. It doesn't often happen. In
effect every array read is pushed down through the chain of array
writes until it gets to a symbol (i.e. an array literal).
If you run with the "-s" option you'll see that the number of nodes
grows sharply after "transformation", which is the step that rewrites
away the array-writes.
If you can turn some array-writes into array-reads then STP will solve
your problem faster.
Below is a simplified example which also blows up. It has 300 array
reads, over a chain of 300 array writes. So STP rewrites it to from
600 nodes, to something like 90,000 nodes. Changing the array-writes
to array-reads is easy to do in this example because they are all at
distinct indices.
Trev.
(set-logic QF_ABV)
(set-info :smt-lib-version 2.0)
(set-info :status unknown)
(declare-fun v281 () (_ BitVec 20))
(declare-fun v64 () (_ BitVec 20))
(declare-fun v57 () (_ BitVec 20))
(declare-fun v141 () (_ BitVec 20))
(declare-fun v181 () (_ BitVec 20))
(declare-fun v102 () (_ BitVec 20))
(declare-fun v210 () (_ BitVec 20))
(declare-fun v292 () (_ BitVec 20))
(declare-fun v48 () (_ BitVec 20))
(declare-fun v152 () (_ BitVec 20))
(declare-fun v192 () (_ BitVec 20))
(declare-fun v254 () (_ BitVec 20))
(declare-fun v73 () (_ BitVec 20))
(declare-fun v113 () (_ BitVec 20))
(declare-fun v221 () (_ BitVec 20))
(declare-fun v163 () (_ BitVec 20))
(declare-fun v42 () (_ BitVec 20))
(declare-fun v84 () (_ BitVec 20))
(declare-fun v124 () (_ BitVec 20))
(declare-fun v274 () (_ BitVec 20))
(declare-fun v232 () (_ BitVec 20))
(declare-fun v25 () (_ BitVec 20))
(declare-fun v13 () (_ BitVec 20))
(declare-fun v50 () (_ BitVec 20))
(declare-fun v134 () (_ BitVec 20))
(declare-fun v174 () (_ BitVec 20))
(declare-fun v243 () (_ BitVec 20))
(declare-fun v95 () (_ BitVec 20))
(declare-fun v263 () (_ BitVec 20))
(declare-fun v203 () (_ BitVec 20))
(declare-fun v7 () (_ BitVec 20))
(declare-fun v285 () (_ BitVec 20))
(declare-fun v61 () (_ BitVec 20))
(declare-fun v145 () (_ BitVec 20))
(declare-fun v185 () (_ BitVec 20))
(declare-fun v247 () (_ BitVec 20))
(declare-fun v106 () (_ BitVec 20))
(declare-fun v214 () (_ BitVec 20))
(declare-fun v296 () (_ BitVec 20))
(declare-fun v156 () (_ BitVec 20))
(declare-fun v35 () (_ BitVec 20))
(declare-fun v77 () (_ BitVec 20))
(declare-fun v117 () (_ BitVec 20))
(declare-fun v267 () (_ BitVec 20))
(declare-fun v225 () (_ BitVec 20))
(declare-fun v18 () (_ BitVec 20))
(declare-fun v167 () (_ BitVec 20))
(declare-fun v236 () (_ BitVec 20))
(declare-fun v88 () (_ BitVec 20))
(declare-fun v256 () (_ BitVec 20))
(declare-fun v196 () (_ BitVec 20))
(declare-fun v278 () (_ BitVec 20))
(declare-fun v29 () (_ BitVec 20))
(declare-fun v9 () (_ BitVec 20))
(declare-fun v54 () (_ BitVec 20))
(declare-fun v138 () (_ BitVec 20))
(declare-fun v178 () (_ BitVec 20))
(declare-fun v99 () (_ BitVec 20))
(declare-fun v207 () (_ BitVec 20))
(declare-fun v289 () (_ BitVec 20))
(declare-fun v66 () (_ BitVec 20))
(declare-fun v1 () (_ BitVec 20))
(declare-fun v45 () (_ BitVec 20))
(declare-fun v129 () (_ BitVec 20))
(declare-fun v149 () (_ BitVec 20))
(declare-fun v189 () (_ BitVec 20))
(declare-fun v251 () (_ BitVec 20))
(declare-fun v70 () (_ BitVec 20))
(declare-fun v110 () (_ BitVec 20))
(declare-fun v218 () (_ BitVec 20))
(declare-fun v160 () (_ BitVec 20))
(declare-fun v39 () (_ BitVec 20))
(declare-fun v81 () (_ BitVec 20))
(declare-fun v121 () (_ BitVec 20))
(declare-fun v271 () (_ BitVec 20))
(declare-fun v229 () (_ BitVec 20))
(declare-fun v22 () (_ BitVec 20))
(declare-fun v10 () (_ BitVec 20))
(declare-fun v194 () (_ BitVec 20))
(declare-fun v171 () (_ BitVec 20))
(declare-fun v240 () (_ BitVec 20))
(declare-fun v92 () (_ BitVec 20))
(declare-fun v260 () (_ BitVec 20))
(declare-fun v200 () (_ BitVec 20))
(declare-fun v16 () (_ BitVec 20))
(declare-fun v282 () (_ BitVec 20))
(declare-fun v58 () (_ BitVec 20))
(declare-fun v142 () (_ BitVec 20))
(declare-fun v182 () (_ BitVec 20))
(declare-fun v103 () (_ BitVec 20))
(declare-fun v211 () (_ BitVec 20))
(declare-fun v293 () (_ BitVec 20))
(declare-fun v49 () (_ BitVec 20))
(declare-fun v153 () (_ BitVec 20))
(declare-fun v255 () (_ BitVec 20))
(declare-fun v74 () (_ BitVec 20))
(declare-fun v114 () (_ BitVec 20))
(declare-fun v264 () (_ BitVec 20))
(declare-fun v222 () (_ BitVec 20))
(declare-fun v164 () (_ BitVec 20))
(declare-fun v43 () (_ BitVec 20))
(declare-fun v85 () (_ BitVec 20))
(declare-fun v125 () (_ BitVec 20))
(declare-fun v275 () (_ BitVec 20))
(declare-fun v233 () (_ BitVec 20))
(declare-fun v0 () (_ BitVec 20))
(declare-fun v26 () (_ BitVec 20))
(declare-fun v14 () (_ BitVec 20))
(declare-fun v51 () (_ BitVec 20))
(declare-fun v135 () (_ BitVec 20))
(declare-fun v175 () (_ BitVec 20))
(declare-fun v244 () (_ BitVec 20))
(declare-fun v96 () (_ BitVec 20))
(declare-fun v204 () (_ BitVec 20))
(declare-fun v286 () (_ BitVec 20))
(declare-fun v62 () (_ BitVec 20))
(declare-fun v146 () (_ BitVec 20))
(declare-fun v186 () (_ BitVec 20))
(declare-fun v248 () (_ BitVec 20))
(declare-fun v67 () (_ BitVec 20))
(declare-fun v107 () (_ BitVec 20))
(declare-fun v215 () (_ BitVec 20))
(declare-fun v297 () (_ BitVec 20))
(declare-fun v157 () (_ BitVec 20))
(declare-fun v36 () (_ BitVec 20))
(declare-fun v78 () (_ BitVec 20))
(declare-fun v118 () (_ BitVec 20))
(declare-fun v268 () (_ BitVec 20))
(declare-fun v226 () (_ BitVec 20))
(declare-fun v19 () (_ BitVec 20))
(declare-fun v168 () (_ BitVec 20))
(declare-fun v237 () (_ BitVec 20))
(declare-fun v89 () (_ BitVec 20))
(declare-fun v257 () (_ BitVec 20))
(declare-fun v197 () (_ BitVec 20))
(declare-fun v279 () (_ BitVec 20))
(declare-fun v30 () (_ BitVec 20))
(declare-fun v55 () (_ BitVec 20))
(declare-fun v139 () (_ BitVec 20))
(declare-fun v179 () (_ BitVec 20))
(declare-fun v100 () (_ BitVec 20))
(declare-fun v208 () (_ BitVec 20))
(declare-fun v290 () (_ BitVec 20))
(declare-fun v46 () (_ BitVec 20))
(declare-fun v150 () (_ BitVec 20))
(declare-fun v4 () (_ BitVec 20))
(declare-fun v190 () (_ BitVec 20))
(declare-fun v252 () (_ BitVec 20))
(declare-fun v71 () (_ BitVec 20))
(declare-fun v111 () (_ BitVec 20))
(declare-fun v219 () (_ BitVec 20))
(declare-fun v130 () (_ BitVec 20))
(declare-fun v161 () (_ BitVec 20))
(declare-fun v2 () (_ BitVec 20))
(declare-fun at () (Array (_ BitVec 20) (_ BitVec 20) ))
(declare-fun v40 () (_ BitVec 20))
(declare-fun v82 () (_ BitVec 20))
(declare-fun v122 () (_ BitVec 20))
(declare-fun v272 () (_ BitVec 20))
(declare-fun v230 () (_ BitVec 20))
(declare-fun v11 () (_ BitVec 20))
(declare-fun v23 () (_ BitVec 20))
(declare-fun v195 () (_ BitVec 20))
(declare-fun v8 () (_ BitVec 20))
(declare-fun v132 () (_ BitVec 20))
(declare-fun v172 () (_ BitVec 20))
(declare-fun v241 () (_ BitVec 20))
(declare-fun v93 () (_ BitVec 20))
(declare-fun v261 () (_ BitVec 20))
(declare-fun v201 () (_ BitVec 20))
(declare-fun v33 () (_ BitVec 20))
(declare-fun v283 () (_ BitVec 20))
(declare-fun v59 () (_ BitVec 20))
(declare-fun v143 () (_ BitVec 20))
(declare-fun v183 () (_ BitVec 20))
(declare-fun v104 () (_ BitVec 20))
(declare-fun v212 () (_ BitVec 20))
(declare-fun v294 () (_ BitVec 20))
(declare-fun v154 () (_ BitVec 20))
(declare-fun v75 () (_ BitVec 20))
(declare-fun v115 () (_ BitVec 20))
(declare-fun v265 () (_ BitVec 20))
(declare-fun v223 () (_ BitVec 20))
(declare-fun v165 () (_ BitVec 20))
(declare-fun v234 () (_ BitVec 20))
(declare-fun v86 () (_ BitVec 20))
(declare-fun v126 () (_ BitVec 20))
(declare-fun v276 () (_ BitVec 20))
(declare-fun v27 () (_ BitVec 20))
(declare-fun v15 () (_ BitVec 20))
(declare-fun v52 () (_ BitVec 20))
(declare-fun v136 () (_ BitVec 20))
(declare-fun v176 () (_ BitVec 20))
(declare-fun v245 () (_ BitVec 20))
(declare-fun v97 () (_ BitVec 20))
(declare-fun v205 () (_ BitVec 20))
(declare-fun v287 () (_ BitVec 20))
(declare-fun v32 () (_ BitVec 20))
(declare-fun v63 () (_ BitVec 20))
(declare-fun v147 () (_ BitVec 20))
(declare-fun v187 () (_ BitVec 20))
(declare-fun v131 () (_ BitVec 20))
(declare-fun v249 () (_ BitVec 20))
(declare-fun v68 () (_ BitVec 20))
(declare-fun v108 () (_ BitVec 20))
(declare-fun v216 () (_ BitVec 20))
(declare-fun v298 () (_ BitVec 20))
(declare-fun v158 () (_ BitVec 20))
(declare-fun v37 () (_ BitVec 20))
(declare-fun v79 () (_ BitVec 20))
(declare-fun v119 () (_ BitVec 20))
(declare-fun v269 () (_ BitVec 20))
(declare-fun v227 () (_ BitVec 20))
(declare-fun v20 () (_ BitVec 20))
(declare-fun v169 () (_ BitVec 20))
(declare-fun v238 () (_ BitVec 20))
(declare-fun v90 () (_ BitVec 20))
(declare-fun v258 () (_ BitVec 20))
(declare-fun v198 () (_ BitVec 20))
(declare-fun v280 () (_ BitVec 20))
(declare-fun v31 () (_ BitVec 20))
(declare-fun v56 () (_ BitVec 20))
(declare-fun v140 () (_ BitVec 20))
(declare-fun v180 () (_ BitVec 20))
(declare-fun v101 () (_ BitVec 20))
(declare-fun v209 () (_ BitVec 20))
(declare-fun v291 () (_ BitVec 20))
(declare-fun v47 () (_ BitVec 20))
(declare-fun v151 () (_ BitVec 20))
(declare-fun v191 () (_ BitVec 20))
(declare-fun v253 () (_ BitVec 20))
(declare-fun v72 () (_ BitVec 20))
(declare-fun v112 () (_ BitVec 20))
(declare-fun v220 () (_ BitVec 20))
(declare-fun v162 () (_ BitVec 20))
(declare-fun v5 () (_ BitVec 20))
(declare-fun v41 () (_ BitVec 20))
(declare-fun v83 () (_ BitVec 20))
(declare-fun v123 () (_ BitVec 20))
(declare-fun v273 () (_ BitVec 20))
(declare-fun v231 () (_ BitVec 20))
(declare-fun v24 () (_ BitVec 20))
(declare-fun v12 () (_ BitVec 20))
(declare-fun v17 () (_ BitVec 20))
(declare-fun v133 () (_ BitVec 20))
(declare-fun v173 () (_ BitVec 20))
(declare-fun v242 () (_ BitVec 20))
(declare-fun v94 () (_ BitVec 20))
(declare-fun v262 () (_ BitVec 20))
(declare-fun v202 () (_ BitVec 20))
(declare-fun v6 () (_ BitVec 20))
(declare-fun v284 () (_ BitVec 20))
(declare-fun v60 () (_ BitVec 20))
(declare-fun v144 () (_ BitVec 20))
(declare-fun v184 () (_ BitVec 20))
(declare-fun v105 () (_ BitVec 20))
(declare-fun v213 () (_ BitVec 20))
(declare-fun v295 () (_ BitVec 20))
(declare-fun v155 () (_ BitVec 20))
(declare-fun v34 () (_ BitVec 20))
(declare-fun v76 () (_ BitVec 20))
(declare-fun v116 () (_ BitVec 20))
(declare-fun v266 () (_ BitVec 20))
(declare-fun v224 () (_ BitVec 20))
(declare-fun v166 () (_ BitVec 20))
(declare-fun v235 () (_ BitVec 20))
(declare-fun v87 () (_ BitVec 20))
(declare-fun v127 () (_ BitVec 20))
(declare-fun v277 () (_ BitVec 20))
(declare-fun v28 () (_ BitVec 20))
(declare-fun v53 () (_ BitVec 20))
(declare-fun v137 () (_ BitVec 20))
(declare-fun v3 () (_ BitVec 20))
(declare-fun v177 () (_ BitVec 20))
(declare-fun v98 () (_ BitVec 20))
(declare-fun v206 () (_ BitVec 20))
(declare-fun v288 () (_ BitVec 20))
(declare-fun v246 () (_ BitVec 20))
(declare-fun v44 () (_ BitVec 20))
(declare-fun v128 () (_ BitVec 20))
(declare-fun v65 () (_ BitVec 20))
(declare-fun v148 () (_ BitVec 20))
(declare-fun v188 () (_ BitVec 20))
(declare-fun v250 () (_ BitVec 20))
(declare-fun v69 () (_ BitVec 20))
(declare-fun v109 () (_ BitVec 20))
(declare-fun v217 () (_ BitVec 20))
(declare-fun v299 () (_ BitVec 20))
(declare-fun v159 () (_ BitVec 20))
(declare-fun v38 () (_ BitVec 20))
(declare-fun v80 () (_ BitVec 20))
(declare-fun v120 () (_ BitVec 20))
(declare-fun v270 () (_ BitVec 20))
(declare-fun v228 () (_ BitVec 20))
(declare-fun v21 () (_ BitVec 20))
(declare-fun v193 () (_ BitVec 20))
(declare-fun v170 () (_ BitVec 20))
(declare-fun v239 () (_ BitVec 20))
(declare-fun v91 () (_ BitVec 20))
(declare-fun v259 () (_ BitVec 20))
(declare-fun v199 () (_ BitVec 20))
(assert (let ((?let_k_0 (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store at (_ bv0 20) (_ bv0 20)) (_ bv1 20) (_
bv1 20)) (_ bv2 20) (_ bv2 20)) (_ bv3 20) (_ bv3 20)) (_ bv4 20) (_
bv4 20)) (_ bv5 20) (_ bv5 20)) (_ bv6 20) (_ bv6 20)) (_ bv7 20) (_
bv7 20)) (_ bv8 20) (_ bv8 20)) (_ bv9 20) (_ bv9 20)) (_ bv10 20) (_
bv10 20)) (_ bv11 20) (_ bv11 20)) (_ bv12 20) (_ bv12 20)) (_ bv13
20) (_ bv13 20)) (_ bv14 20) (_ bv14 20)) (_ bv15 20) (_ bv15 20)) (_
bv16 20) (_ bv16 20)) (_ bv17 20) (_ bv17 20)) (_ bv18 20) (_ bv18
20)) (_ bv19 20) (_ bv19 20)) (_ bv20 20) (_ bv20 20)) (_ bv21 20) (_
bv21 20)) (_ bv22 20) (_ bv22 20)) (_ bv23 20) (_ bv23 20)) (_ bv24
20) (_ bv24 20)) (_ bv25 20) (_ bv25 20)) (_ bv26 20) (_ bv26 20)) (_
bv27 20) (_ bv27 20)) (_ bv28 20) (_ bv28 20)) (_ bv29 20) (_ bv29
20)) (_ bv30 20) (_ bv30 20)) (_ bv31 20) (_ bv31 20)) (_ bv32 20) (_
bv32 20)) (_ bv33 20) (_ bv33 20)) (_ bv34 20) (_ bv34 20)) (_ bv35
20) (_ bv35 20)) (_ bv36 20) (_ bv36 20)) (_ bv37 20) (_ bv37 20)) (_
bv38 20) (_ bv38 20)) (_ bv39 20) (_ bv39 20)) (_ bv40 20) (_ bv40
20)) (_ bv41 20) (_ bv41 20)) (_ bv42 20) (_ bv42 20)) (_ bv43 20) (_
bv43 20)) (_ bv44 20) (_ bv44 20)) (_ bv45 20) (_ bv45 20)) (_ bv46
20) (_ bv46 20)) (_ bv47 20) (_ bv47 20)) (_ bv48 20) (_ bv48 20)) (_
bv49 20) (_ bv49 20)) (_ bv50 20) (_ bv50 20)) (_ bv51 20) (_ bv51
20)) (_ bv52 20) (_ bv52 20)) (_ bv53 20) (_ bv53 20)) (_ bv54 20) (_
bv54 20)) (_ bv55 20) (_ bv55 20)) (_ bv56 20) (_ bv56 20)) (_ bv57
20) (_ bv57 20)) (_ bv58 20) (_ bv58 20)) (_ bv59 20) (_ bv59 20)) (_
bv60 20) (_ bv60 20)) (_ bv61 20) (_ bv61 20)) (_ bv62 20) (_ bv62
20)) (_ bv63 20) (_ bv63 20)) (_ bv64 20) (_ bv64 20)) (_ bv65 20) (_
bv65 20)) (_ bv66 20) (_ bv66 20)) (_ bv67 20) (_ bv67 20)) (_ bv68
20) (_ bv68 20)) (_ bv69 20) (_ bv69 20)) (_ bv70 20) (_ bv70 20)) (_
bv71 20) (_ bv71 20)) (_ bv72 20) (_ bv72 20)) (_ bv73 20) (_ bv73
20)) (_ bv74 20) (_ bv74 20)) (_ bv75 20) (_ bv75 20)) (_ bv76 20) (_
bv76 20)) (_ bv77 20) (_ bv77 20)) (_ bv78 20) (_ bv78 20)) (_ bv79
20) (_ bv79 20)) (_ bv80 20) (_ bv80 20)) (_ bv81 20) (_ bv81 20)) (_
bv82 20) (_ bv82 20)) (_ bv83 20) (_ bv83 20)) (_ bv84 20) (_ bv84
20)) (_ bv85 20) (_ bv85 20)) (_ bv86 20) (_ bv86 20)) (_ bv87 20) (_
bv87 20)) (_ bv88 20) (_ bv88 20)) (_ bv89 20) (_ bv89 20)) (_ bv90
20) (_ bv90 20)) (_ bv91 20) (_ bv91 20)) (_ bv92 20) (_ bv92 20)) (_
bv93 20) (_ bv93 20)) (_ bv94 20) (_ bv94 20)) (_ bv95 20) (_ bv95
20)) (_ bv96 20) (_ bv96 20)) (_ bv97 20) (_ bv97 20)) (_ bv98 20) (_
bv98 20)) (_ bv99 20) (_ bv99 20)) (_ bv100 20) (_ bv100 20)) (_ bv101
20) (_ bv101 20)) (_ bv102 20) (_ bv102 20)) (_ bv103 20) (_ bv103
20)) (_ bv104 20) (_ bv104 20)) (_ bv105 20) (_ bv105 20)) (_ bv106
20) (_ bv106 20)) (_ bv107 20) (_ bv107 20)) (_ bv108 20) (_ bv108
20)) (_ bv109 20) (_ bv109 20)) (_ bv110 20) (_ bv110 20)) (_ bv111
20) (_ bv111 20)) (_ bv112 20) (_ bv112 20)) (_ bv113 20) (_ bv113
20)) (_ bv114 20) (_ bv114 20)) (_ bv115 20) (_ bv115 20)) (_ bv116
20) (_ bv116 20)) (_ bv117 20) (_ bv117 20)) (_ bv118 20) (_ bv118
20)) (_ bv119 20) (_ bv119 20)) (_ bv120 20) (_ bv120 20)) (_ bv121
20) (_ bv121 20)) (_ bv122 20) (_ bv122 20)) (_ bv123 20) (_ bv123
20)) (_ bv124 20) (_ bv124 20)) (_ bv125 20) (_ bv125 20)) (_ bv126
20) (_ bv126 20)) (_ bv127 20) (_ bv127 20)) (_ bv128 20) (_ bv128
20)) (_ bv129 20) (_ bv129 20)) (_ bv130 20) (_ bv130 20)) (_ bv131
20) (_ bv131 20)) (_ bv132 20) (_ bv132 20)) (_ bv133 20) (_ bv133
20)) (_ bv134 20) (_ bv134 20)) (_ bv135 20) (_ bv135 20)) (_ bv136
20) (_ bv136 20)) (_ bv137 20) (_ bv137 20)) (_ bv138 20) (_ bv138
20)) (_ bv139 20) (_ bv139 20)) (_ bv140 20) (_ bv140 20)) (_ bv141
20) (_ bv141 20)) (_ bv142 20) (_ bv142 20)) (_ bv143 20) (_ bv143
20)) (_ bv144 20) (_ bv144 20)) (_ bv145 20) (_ bv145 20)) (_ bv146
20) (_ bv146 20)) (_ bv147 20) (_ bv147 20)) (_ bv148 20) (_ bv148
20)) (_ bv149 20) (_ bv149 20)) (_ bv150 20) (_ bv150 20)) (_ bv151
20) (_ bv151 20)) (_ bv152 20) (_ bv152 20)) (_ bv153 20) (_ bv153
20)) (_ bv154 20) (_ bv154 20)) (_ bv155 20) (_ bv155 20)) (_ bv156
20) (_ bv156 20)) (_ bv157 20) (_ bv157 20)) (_ bv158 20) (_ bv158
20)) (_ bv159 20) (_ bv159 20)) (_ bv160 20) (_ bv160 20)) (_ bv161
20) (_ bv161 20)) (_ bv162 20) (_ bv162 20)) (_ bv163 20) (_ bv163
20)) (_ bv164 20) (_ bv164 20)) (_ bv165 20) (_ bv165 20)) (_ bv166
20) (_ bv166 20)) (_ bv167 20) (_ bv167 20)) (_ bv168 20) (_ bv168
20)) (_ bv169 20) (_ bv169 20)) (_ bv170 20) (_ bv170 20)) (_ bv171
20) (_ bv171 20)) (_ bv172 20) (_ bv172 20)) (_ bv173 20) (_ bv173
20)) (_ bv174 20) (_ bv174 20)) (_ bv175 20) (_ bv175 20)) (_ bv176
20) (_ bv176 20)) (_ bv177 20) (_ bv177 20)) (_ bv178 20) (_ bv178
20)) (_ bv179 20) (_ bv179 20)) (_ bv180 20) (_ bv180 20)) (_ bv181
20) (_ bv181 20)) (_ bv182 20) (_ bv182 20)) (_ bv183 20) (_ bv183
20)) (_ bv184 20) (_ bv184 20)) (_ bv185 20) (_ bv185 20)) (_ bv186
20) (_ bv186 20)) (_ bv187 20) (_ bv187 20)) (_ bv188 20) (_ bv188
20)) (_ bv189 20) (_ bv189 20)) (_ bv190 20) (_ bv190 20)) (_ bv191
20) (_ bv191 20)) (_ bv192 20) (_ bv192 20)) (_ bv193 20) (_ bv193
20)) (_ bv194 20) (_ bv194 20)) (_ bv195 20) (_ bv195 20)) (_ bv196
20) (_ bv196 20)) (_ bv197 20) (_ bv197 20)) (_ bv198 20) (_ bv198
20)) (_ bv199 20) (_ bv199 20)) (_ bv200 20) (_ bv200 20)) (_ bv201
20) (_ bv201 20)) (_ bv202 20) (_ bv202 20)) (_ bv203 20) (_ bv203
20)) (_ bv204 20) (_ bv204 20)) (_ bv205 20) (_ bv205 20)) (_ bv206
20) (_ bv206 20)) (_ bv207 20) (_ bv207 20)) (_ bv208 20) (_ bv208
20)) (_ bv209 20) (_ bv209 20)) (_ bv210 20) (_ bv210 20)) (_ bv211
20) (_ bv211 20)) (_ bv212 20) (_ bv212 20)) (_ bv213 20) (_ bv213
20)) (_ bv214 20) (_ bv214 20)) (_ bv215 20) (_ bv215 20)) (_ bv216
20) (_ bv216 20)) (_ bv217 20) (_ bv217 20)) (_ bv218 20) (_ bv218
20)) (_ bv219 20) (_ bv219 20)) (_ bv220 20) (_ bv220 20)) (_ bv221
20) (_ bv221 20)) (_ bv222 20) (_ bv222 20)) (_ bv223 20) (_ bv223
20)) (_ bv224 20) (_ bv224 20)) (_ bv225 20) (_ bv225 20)) (_ bv226
20) (_ bv226 20)) (_ bv227 20) (_ bv227 20)) (_ bv228 20) (_ bv228
20)) (_ bv229 20) (_ bv229 20)) (_ bv230 20) (_ bv230 20)) (_ bv231
20) (_ bv231 20)) (_ bv232 20) (_ bv232 20)) (_ bv233 20) (_ bv233
20)) (_ bv234 20) (_ bv234 20)) (_ bv235 20) (_ bv235 20)) (_ bv236
20) (_ bv236 20)) (_ bv237 20) (_ bv237 20)) (_ bv238 20) (_ bv238
20)) (_ bv239 20) (_ bv239 20)) (_ bv240 20) (_ bv240 20)) (_ bv241
20) (_ bv241 20)) (_ bv242 20) (_ bv242 20)) (_ bv243 20) (_ bv243
20)) (_ bv244 20) (_ bv244 20)) (_ bv245 20) (_ bv245 20)) (_ bv246
20) (_ bv246 20)) (_ bv247 20) (_ bv247 20)) (_ bv248 20) (_ bv248
20)) (_ bv249 20) (_ bv249 20)) (_ bv250 20) (_ bv250 20)) (_ bv251
20) (_ bv251 20)) (_ bv252 20) (_ bv252 20)) (_ bv253 20) (_ bv253
20)) (_ bv254 20) (_ bv254 20)) (_ bv255 20) (_ bv255 20)) (_ bv256
20) (_ bv256 20)) (_ bv257 20) (_ bv257 20)) (_ bv258 20) (_ bv258
20)) (_ bv259 20) (_ bv259 20)) (_ bv260 20) (_ bv260 20)) (_ bv261
20) (_ bv261 20)) (_ bv262 20) (_ bv262 20)) (_ bv263 20) (_ bv263
20)) (_ bv264 20) (_ bv264 20)) (_ bv265 20) (_ bv265 20)) (_ bv266
20) (_ bv266 20)) (_ bv267 20) (_ bv267 20)) (_ bv268 20) (_ bv268
20)) (_ bv269 20) (_ bv269 20)) (_ bv270 20) (_ bv270 20)) (_ bv271
20) (_ bv271 20)) (_ bv272 20) (_ bv272 20)) (_ bv273 20) (_ bv273
20)) (_ bv274 20) (_ bv274 20)) (_ bv275 20) (_ bv275 20)) (_ bv276
20) (_ bv276 20)) (_ bv277 20) (_ bv277 20)) (_ bv278 20) (_ bv278
20)) (_ bv279 20) (_ bv279 20)) (_ bv280 20) (_ bv280 20)) (_ bv281
20) (_ bv281 20)) (_ bv282 20) (_ bv282 20)) (_ bv283 20) (_ bv283
20)) (_ bv284 20) (_ bv284 20)) (_ bv285 20) (_ bv285 20)) (_ bv286
20) (_ bv286 20)) (_ bv287 20) (_ bv287 20)) (_ bv288 20) (_ bv288
20)) (_ bv289 20) (_ bv289 20)) (_ bv290 20) (_ bv290 20)) (_ bv291
20) (_ bv291 20)) (_ bv292 20) (_ bv292 20)) (_ bv293 20) (_ bv293
20)) (_ bv294 20) (_ bv294 20)) (_ bv295 20) (_ bv295 20)) (_ bv296
20) (_ bv296 20)) (_ bv297 20) (_ bv297 20)) (_ bv298 20) (_ bv298
20)) (_ bv299 20) (_ bv299 20)) ))
(and (= v0 (select ?let_k_0 v0)) (and (= v1 (select ?let_k_0 v1)) (and
(= v2 (select ?let_k_0 v2)) (and (= v3 (select ?let_k_0 v3)) (and (=
v4 (select ?let_k_0 v4)) (and (= v5 (select ?let_k_0 v5)) (and (= v6
(select ?let_k_0 v6)) (and (= v7 (select ?let_k_0 v7)) (and (= v8
(select ?let_k_0 v8)) (and (= v9 (select ?let_k_0 v9)) (and (= v10
(select ?let_k_0 v10)) (and (= v11 (select ?let_k_0 v11)) (and (= v12
(select ?let_k_0 v12)) (and (= v13 (select ?let_k_0 v13)) (and (= v14
(select ?let_k_0 v14)) (and (= v15 (select ?let_k_0 v15)) (and (= v16
(select ?let_k_0 v16)) (and (= v17 (select ?let_k_0 v17)) (and (= v18
(select ?let_k_0 v18)) (and (= v19 (select ?let_k_0 v19)) (and (= v20
(select ?let_k_0 v20)) (and (= v21 (select ?let_k_0 v21)) (and (= v22
(select ?let_k_0 v22)) (and (= v23 (select ?let_k_0 v23)) (and (= v24
(select ?let_k_0 v24)) (and (= v25 (select ?let_k_0 v25)) (and (= v26
(select ?let_k_0 v26)) (and (= v27 (select ?let_k_0 v27)) (and (= v28
(select ?let_k_0 v28)) (and (= v29 (select ?let_k_0 v29)) (and (= v30
(select ?let_k_0 v30)) (and (= v31 (select ?let_k_0 v31)) (and (= v32
(select ?let_k_0 v32)) (and (= v33 (select ?let_k_0 v33)) (and (= v34
(select ?let_k_0 v34)) (and (= v35 (select ?let_k_0 v35)) (and (= v36
(select ?let_k_0 v36)) (and (= v37 (select ?let_k_0 v37)) (and (= v38
(select ?let_k_0 v38)) (and (= v39 (select ?let_k_0 v39)) (and (= v40
(select ?let_k_0 v40)) (and (= v41 (select ?let_k_0 v41)) (and (= v42
(select ?let_k_0 v42)) (and (= v43 (select ?let_k_0 v43)) (and (= v44
(select ?let_k_0 v44)) (and (= v45 (select ?let_k_0 v45)) (and (= v46
(select ?let_k_0 v46)) (and (= v47 (select ?let_k_0 v47)) (and (= v48
(select ?let_k_0 v48)) (and (= v49 (select ?let_k_0 v49)) (and (= v50
(select ?let_k_0 v50)) (and (= v51 (select ?let_k_0 v51)) (and (= v52
(select ?let_k_0 v52)) (and (= v53 (select ?let_k_0 v53)) (and (= v54
(select ?let_k_0 v54)) (and (= v55 (select ?let_k_0 v55)) (and (= v56
(select ?let_k_0 v56)) (and (= v57 (select ?let_k_0 v57)) (and (= v58
(select ?let_k_0 v58)) (and (= v59 (select ?let_k_0 v59)) (and (= v60
(select ?let_k_0 v60)) (and (= v61 (select ?let_k_0 v61)) (and (= v62
(select ?let_k_0 v62)) (and (= v63 (select ?let_k_0 v63)) (and (= v64
(select ?let_k_0 v64)) (and (= v65 (select ?let_k_0 v65)) (and (= v66
(select ?let_k_0 v66)) (and (= v67 (select ?let_k_0 v67)) (and (= v68
(select ?let_k_0 v68)) (and (= v69 (select ?let_k_0 v69)) (and (= v70
(select ?let_k_0 v70)) (and (= v71 (select ?let_k_0 v71)) (and (= v72
(select ?let_k_0 v72)) (and (= v73 (select ?let_k_0 v73)) (and (= v74
(select ?let_k_0 v74)) (and (= v75 (select ?let_k_0 v75)) (and (= v76
(select ?let_k_0 v76)) (and (= v77 (select ?let_k_0 v77)) (and (= v78
(select ?let_k_0 v78)) (and (= v79 (select ?let_k_0 v79)) (and (= v80
(select ?let_k_0 v80)) (and (= v81 (select ?let_k_0 v81)) (and (= v82
(select ?let_k_0 v82)) (and (= v83 (select ?let_k_0 v83)) (and (= v84
(select ?let_k_0 v84)) (and (= v85 (select ?let_k_0 v85)) (and (= v86
(select ?let_k_0 v86)) (and (= v87 (select ?let_k_0 v87)) (and (= v88
(select ?let_k_0 v88)) (and (= v89 (select ?let_k_0 v89)) (and (= v90
(select ?let_k_0 v90)) (and (= v91 (select ?let_k_0 v91)) (and (= v92
(select ?let_k_0 v92)) (and (= v93 (select ?let_k_0 v93)) (and (= v94
(select ?let_k_0 v94)) (and (= v95 (select ?let_k_0 v95)) (and (= v96
(select ?let_k_0 v96)) (and (= v97 (select ?let_k_0 v97)) (and (= v98
(select ?let_k_0 v98)) (and (= v99 (select ?let_k_0 v99)) (and (= v100
(select ?let_k_0 v100)) (and (= v101 (select ?let_k_0 v101)) (and (=
v102 (select ?let_k_0 v102)) (and (= v103 (select ?let_k_0 v103)) (and
(= v104 (select ?let_k_0 v104)) (and (= v105 (select ?let_k_0 v105))
(and (= v106 (select ?let_k_0 v106)) (and (= v107 (select ?let_k_0
v107)) (and (= v108 (select ?let_k_0 v108)) (and (= v109 (select ?
let_k_0 v109)) (and (= v110 (select ?let_k_0 v110)) (and (= v111
(select ?let_k_0 v111)) (and (= v112 (select ?let_k_0 v112)) (and (=
v113 (select ?let_k_0 v113)) (and (= v114 (select ?let_k_0 v114)) (and
(= v115 (select ?let_k_0 v115)) (and (= v116 (select ?let_k_0 v116))
(and (= v117 (select ?let_k_0 v117)) (and (= v118 (select ?let_k_0
v118)) (and (= v119 (select ?let_k_0 v119)) (and (= v120 (select ?
let_k_0 v120)) (and (= v121 (select ?let_k_0 v121)) (and (= v122
(select ?let_k_0 v122)) (and (= v123 (select ?let_k_0 v123)) (and (=
v124 (select ?let_k_0 v124)) (and (= v125 (select ?let_k_0 v125)) (and
(= v126 (select ?let_k_0 v126)) (and (= v127 (select ?let_k_0 v127))
(and (= v128 (select ?let_k_0 v128)) (and (= v129 (select ?let_k_0
v129)) (and (= v130 (select ?let_k_0 v130)) (and (= v131 (select ?
let_k_0 v131)) (and (= v132 (select ?let_k_0 v132)) (and (= v133
(select ?let_k_0 v133)) (and (= v134 (select ?let_k_0 v134)) (and (=
v135 (select ?let_k_0 v135)) (and (= v136 (select ?let_k_0 v136)) (and
(= v137 (select ?let_k_0 v137)) (and (= v138 (select ?let_k_0 v138))
(and (= v139 (select ?let_k_0 v139)) (and (= v140 (select ?let_k_0
v140)) (and (= v141 (select ?let_k_0 v141)) (and (= v142 (select ?
let_k_0 v142)) (and (= v143 (select ?let_k_0 v143)) (and (= v144
(select ?let_k_0 v144)) (and (= v145 (select ?let_k_0 v145)) (and (=
v146 (select ?let_k_0 v146)) (and (= v147 (select ?let_k_0 v147)) (and
(= v148 (select ?let_k_0 v148)) (and (= v149 (select ?let_k_0 v149))
(and (= v150 (select ?let_k_0 v150)) (and (= v151 (select ?let_k_0
v151)) (and (= v152 (select ?let_k_0 v152)) (and (= v153 (select ?
let_k_0 v153)) (and (= v154 (select ?let_k_0 v154)) (and (= v155
(select ?let_k_0 v155)) (and (= v156 (select ?let_k_0 v156)) (and (=
v157 (select ?let_k_0 v157)) (and (= v158 (select ?let_k_0 v158)) (and
(= v159 (select ?let_k_0 v159)) (and (= v160 (select ?let_k_0 v160))
(and (= v161 (select ?let_k_0 v161)) (and (= v162 (select ?let_k_0
v162)) (and (= v163 (select ?let_k_0 v163)) (and (= v164 (select ?
let_k_0 v164)) (and (= v165 (select ?let_k_0 v165)) (and (= v166
(select ?let_k_0 v166)) (and (= v167 (select ?let_k_0 v167)) (and (=
v168 (select ?let_k_0 v168)) (and (= v169 (select ?let_k_0 v169)) (and
(= v170 (select ?let_k_0 v170)) (and (= v171 (select ?let_k_0 v171))
(and (= v172 (select ?let_k_0 v172)) (and (= v173 (select ?let_k_0
v173)) (and (= v174 (select ?let_k_0 v174)) (and (= v175 (select ?
let_k_0 v175)) (and (= v176 (select ?let_k_0 v176)) (and (= v177
(select ?let_k_0 v177)) (and (= v178 (select ?let_k_0 v178)) (and (=
v179 (select ?let_k_0 v179)) (and (= v180 (select ?let_k_0 v180)) (and
(= v181 (select ?let_k_0 v181)) (and (= v182 (select ?let_k_0 v182))
(and (= v183 (select ?let_k_0 v183)) (and (= v184 (select ?let_k_0
v184)) (and (= v185 (select ?let_k_0 v185)) (and (= v186 (select ?
let_k_0 v186)) (and (= v187 (select ?let_k_0 v187)) (and (= v188
(select ?let_k_0 v188)) (and (= v189 (select ?let_k_0 v189)) (and (=
v190 (select ?let_k_0 v190)) (and (= v191 (select ?let_k_0 v191)) (and
(= v192 (select ?let_k_0 v192)) (and (= v193 (select ?let_k_0 v193))
(and (= v194 (select ?let_k_0 v194)) (and (= v195 (select ?let_k_0
v195)) (and (= v196 (select ?let_k_0 v196)) (and (= v197 (select ?
let_k_0 v197)) (and (= v198 (select ?let_k_0 v198)) (and (= v199
(select ?let_k_0 v199)) (and (= v200 (select ?let_k_0 v200)) (and (=
v201 (select ?let_k_0 v201)) (and (= v202 (select ?let_k_0 v202)) (and
(= v203 (select ?let_k_0 v203)) (and (= v204 (select ?let_k_0 v204))
(and (= v205 (select ?let_k_0 v205)) (and (= v206 (select ?let_k_0
v206)) (and (= v207 (select ?let_k_0 v207)) (and (= v208 (select ?
let_k_0 v208)) (and (= v209 (select ?let_k_0 v209)) (and (= v210
(select ?let_k_0 v210)) (and (= v211 (select ?let_k_0 v211)) (and (=
v212 (select ?let_k_0 v212)) (and (= v213 (select ?let_k_0 v213)) (and
(= v214 (select ?let_k_0 v214)) (and (= v215 (select ?let_k_0 v215))
(and (= v216 (select ?let_k_0 v216)) (and (= v217 (select ?let_k_0
v217)) (and (= v218 (select ?let_k_0 v218)) (and (= v219 (select ?
let_k_0 v219)) (and (= v220 (select ?let_k_0 v220)) (and (= v221
(select ?let_k_0 v221)) (and (= v222 (select ?let_k_0 v222)) (and (=
v223 (select ?let_k_0 v223)) (and (= v224 (select ?let_k_0 v224)) (and
(= v225 (select ?let_k_0 v225)) (and (= v226 (select ?let_k_0 v226))
(and (= v227 (select ?let_k_0 v227)) (and (= v228 (select ?let_k_0
v228)) (and (= v229 (select ?let_k_0 v229)) (and (= v230 (select ?
let_k_0 v230)) (and (= v231 (select ?let_k_0 v231)) (and (= v232
(select ?let_k_0 v232)) (and (= v233 (select ?let_k_0 v233)) (and (=
v234 (select ?let_k_0 v234)) (and (= v235 (select ?let_k_0 v235)) (and
(= v236 (select ?let_k_0 v236)) (and (= v237 (select ?let_k_0 v237))
(and (= v238 (select ?let_k_0 v238)) (and (= v239 (select ?let_k_0
v239)) (and (= v240 (select ?let_k_0 v240)) (and (= v241 (select ?
let_k_0 v241)) (and (= v242 (select ?let_k_0 v242)) (and (= v243
(select ?let_k_0 v243)) (and (= v244 (select ?let_k_0 v244)) (and (=
v245 (select ?let_k_0 v245)) (and (= v246 (select ?let_k_0 v246)) (and
(= v247 (select ?let_k_0 v247)) (and (= v248 (select ?let_k_0 v248))
(and (= v249 (select ?let_k_0 v249)) (and (= v250 (select ?let_k_0
v250)) (and (= v251 (select ?let_k_0 v251)) (and (= v252 (select ?
let_k_0 v252)) (and (= v253 (select ?let_k_0 v253)) (and (= v254
(select ?let_k_0 v254)) (and (= v255 (select ?let_k_0 v255)) (and (=
v256 (select ?let_k_0 v256)) (and (= v257 (select ?let_k_0 v257)) (and
(= v258 (select ?let_k_0 v258)) (and (= v259 (select ?let_k_0 v259))
(and (= v260 (select ?let_k_0 v260)) (and (= v261 (select ?let_k_0
v261)) (and (= v262 (select ?let_k_0 v262)) (and (= v263 (select ?
let_k_0 v263)) (and (= v264 (select ?let_k_0 v264)) (and (= v265
(select ?let_k_0 v265)) (and (= v266 (select ?let_k_0 v266)) (and (=
v267 (select ?let_k_0 v267)) (and (= v268 (select ?let_k_0 v268)) (and
(= v269 (select ?let_k_0 v269)) (and (= v270 (select ?let_k_0 v270))
(and (= v271 (select ?let_k_0 v271)) (and (= v272 (select ?let_k_0
v272)) (and (= v273 (select ?let_k_0 v273)) (and (= v274 (select ?
let_k_0 v274)) (and (= v275 (select ?let_k_0 v275)) (and (= v276
(select ?let_k_0 v276)) (and (= v277 (select ?let_k_0 v277)) (and (=
v278 (select ?let_k_0 v278)) (and (= v279 (select ?let_k_0 v279)) (and
(= v280 (select ?let_k_0 v280)) (and (= v281 (select ?let_k_0 v281))
(and (= v282 (select ?let_k_0 v282)) (and (= v283 (select ?let_k_0
v283)) (and (= v284 (select ?let_k_0 v284)) (and (= v285 (select ?
let_k_0 v285)) (and (= v286 (select ?let_k_0 v286)) (and (= v287
(select ?let_k_0 v287)) (and (= v288 (select ?let_k_0 v288)) (and (=
v289 (select ?let_k_0 v289)) (and (= v290 (select ?let_k_0 v290)) (and
(= v291 (select ?let_k_0 v291)) (and (= v292 (select ?let_k_0 v292))
(and (= v293 (select ?let_k_0 v293)) (and (= v294 (select ?let_k_0
v294)) (and (= v295 (select ?let_k_0 v295)) (and (= v296 (select ?
let_k_0 v296)) (and (= v297 (select ?let_k_0 v297)) (and (= v298
(select ?let_k_0 v298)) (= v299 (select ?let_k_0
v299))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )
)
(check-sat)
(exit)
I've looked more at your testcase.
STP does particularly badly on it because STP only does abstraction-
refinement of array-reads. It rewrites all the array-writes away
before it begins its abstraction refinement. Solvers like Boolector
and Sonolar also do abstraction refinement on array-writes. Version
0.1 of STP did array-write abstraction/refinement, but it's not
currently working.
Rewriting away the array-writes can introduce a quadratic number of
extra nodes. It does that on your problem. It doesn't often happen. In
effect every array read is pushed down through the chain of array
writes until it gets to a symbol (i.e. an array literal).
If you run with the "-s" option you'll see that the number of nodes
grows sharply after "transformation", which is the step that rewrites
away the array-writes.
If you can turn some array-writes into array-reads then STP will solve
your problem faster.
Below is a simplified example which also blows up. It has 300 array
reads, over a chain of 300 array writes. So STP rewrites it to from
600 nodes, to something like 90,000 nodes. Changing the array-writes
to array-reads is easy to do in this example because they are all at
distinct indices.
Trev.
(set-logic QF_ABV)
(set-info :smt-lib-version 2.0)
(set-info :status unknown)
(declare-fun v281 () (_ BitVec 20))
(declare-fun v64 () (_ BitVec 20))
(declare-fun v57 () (_ BitVec 20))
(declare-fun v141 () (_ BitVec 20))
(declare-fun v181 () (_ BitVec 20))
(declare-fun v102 () (_ BitVec 20))
(declare-fun v210 () (_ BitVec 20))
(declare-fun v292 () (_ BitVec 20))
(declare-fun v48 () (_ BitVec 20))
(declare-fun v152 () (_ BitVec 20))
(declare-fun v192 () (_ BitVec 20))
(declare-fun v254 () (_ BitVec 20))
(declare-fun v73 () (_ BitVec 20))
(declare-fun v113 () (_ BitVec 20))
(declare-fun v221 () (_ BitVec 20))
(declare-fun v163 () (_ BitVec 20))
(declare-fun v42 () (_ BitVec 20))
(declare-fun v84 () (_ BitVec 20))
(declare-fun v124 () (_ BitVec 20))
(declare-fun v274 () (_ BitVec 20))
(declare-fun v232 () (_ BitVec 20))
(declare-fun v25 () (_ BitVec 20))
(declare-fun v13 () (_ BitVec 20))
(declare-fun v50 () (_ BitVec 20))
(declare-fun v134 () (_ BitVec 20))
(declare-fun v174 () (_ BitVec 20))
(declare-fun v243 () (_ BitVec 20))
(declare-fun v95 () (_ BitVec 20))
(declare-fun v263 () (_ BitVec 20))
(declare-fun v203 () (_ BitVec 20))
(declare-fun v7 () (_ BitVec 20))
(declare-fun v285 () (_ BitVec 20))
(declare-fun v61 () (_ BitVec 20))
(declare-fun v145 () (_ BitVec 20))
(declare-fun v185 () (_ BitVec 20))
(declare-fun v247 () (_ BitVec 20))
(declare-fun v106 () (_ BitVec 20))
(declare-fun v214 () (_ BitVec 20))
(declare-fun v296 () (_ BitVec 20))
(declare-fun v156 () (_ BitVec 20))
(declare-fun v35 () (_ BitVec 20))
(declare-fun v77 () (_ BitVec 20))
(declare-fun v117 () (_ BitVec 20))
(declare-fun v267 () (_ BitVec 20))
(declare-fun v225 () (_ BitVec 20))
(declare-fun v18 () (_ BitVec 20))
(declare-fun v167 () (_ BitVec 20))
(declare-fun v236 () (_ BitVec 20))
(declare-fun v88 () (_ BitVec 20))
(declare-fun v256 () (_ BitVec 20))
(declare-fun v196 () (_ BitVec 20))
(declare-fun v278 () (_ BitVec 20))
(declare-fun v29 () (_ BitVec 20))
(declare-fun v9 () (_ BitVec 20))
(declare-fun v54 () (_ BitVec 20))
(declare-fun v138 () (_ BitVec 20))
(declare-fun v178 () (_ BitVec 20))
(declare-fun v99 () (_ BitVec 20))
(declare-fun v207 () (_ BitVec 20))
(declare-fun v289 () (_ BitVec 20))
(declare-fun v66 () (_ BitVec 20))
(declare-fun v1 () (_ BitVec 20))
(declare-fun v45 () (_ BitVec 20))
(declare-fun v129 () (_ BitVec 20))
(declare-fun v149 () (_ BitVec 20))
(declare-fun v189 () (_ BitVec 20))
(declare-fun v251 () (_ BitVec 20))
(declare-fun v70 () (_ BitVec 20))
(declare-fun v110 () (_ BitVec 20))
(declare-fun v218 () (_ BitVec 20))
(declare-fun v160 () (_ BitVec 20))
(declare-fun v39 () (_ BitVec 20))
(declare-fun v81 () (_ BitVec 20))
(declare-fun v121 () (_ BitVec 20))
(declare-fun v271 () (_ BitVec 20))
(declare-fun v229 () (_ BitVec 20))
(declare-fun v22 () (_ BitVec 20))
(declare-fun v10 () (_ BitVec 20))
(declare-fun v194 () (_ BitVec 20))
(declare-fun v171 () (_ BitVec 20))
(declare-fun v240 () (_ BitVec 20))
(declare-fun v92 () (_ BitVec 20))
(declare-fun v260 () (_ BitVec 20))
(declare-fun v200 () (_ BitVec 20))
(declare-fun v16 () (_ BitVec 20))
(declare-fun v282 () (_ BitVec 20))
(declare-fun v58 () (_ BitVec 20))
(declare-fun v142 () (_ BitVec 20))
(declare-fun v182 () (_ BitVec 20))
(declare-fun v103 () (_ BitVec 20))
(declare-fun v211 () (_ BitVec 20))
(declare-fun v293 () (_ BitVec 20))
(declare-fun v49 () (_ BitVec 20))
(declare-fun v153 () (_ BitVec 20))
(declare-fun v255 () (_ BitVec 20))
(declare-fun v74 () (_ BitVec 20))
(declare-fun v114 () (_ BitVec 20))
(declare-fun v264 () (_ BitVec 20))
(declare-fun v222 () (_ BitVec 20))
(declare-fun v164 () (_ BitVec 20))
(declare-fun v43 () (_ BitVec 20))
(declare-fun v85 () (_ BitVec 20))
(declare-fun v125 () (_ BitVec 20))
(declare-fun v275 () (_ BitVec 20))
(declare-fun v233 () (_ BitVec 20))
(declare-fun v0 () (_ BitVec 20))
(declare-fun v26 () (_ BitVec 20))
(declare-fun v14 () (_ BitVec 20))
(declare-fun v51 () (_ BitVec 20))
(declare-fun v135 () (_ BitVec 20))
(declare-fun v175 () (_ BitVec 20))
(declare-fun v244 () (_ BitVec 20))
(declare-fun v96 () (_ BitVec 20))
(declare-fun v204 () (_ BitVec 20))
(declare-fun v286 () (_ BitVec 20))
(declare-fun v62 () (_ BitVec 20))
(declare-fun v146 () (_ BitVec 20))
(declare-fun v186 () (_ BitVec 20))
(declare-fun v248 () (_ BitVec 20))
(declare-fun v67 () (_ BitVec 20))
(declare-fun v107 () (_ BitVec 20))
(declare-fun v215 () (_ BitVec 20))
(declare-fun v297 () (_ BitVec 20))
(declare-fun v157 () (_ BitVec 20))
(declare-fun v36 () (_ BitVec 20))
(declare-fun v78 () (_ BitVec 20))
(declare-fun v118 () (_ BitVec 20))
(declare-fun v268 () (_ BitVec 20))
(declare-fun v226 () (_ BitVec 20))
(declare-fun v19 () (_ BitVec 20))
(declare-fun v168 () (_ BitVec 20))
(declare-fun v237 () (_ BitVec 20))
(declare-fun v89 () (_ BitVec 20))
(declare-fun v257 () (_ BitVec 20))
(declare-fun v197 () (_ BitVec 20))
(declare-fun v279 () (_ BitVec 20))
(declare-fun v30 () (_ BitVec 20))
(declare-fun v55 () (_ BitVec 20))
(declare-fun v139 () (_ BitVec 20))
(declare-fun v179 () (_ BitVec 20))
(declare-fun v100 () (_ BitVec 20))
(declare-fun v208 () (_ BitVec 20))
(declare-fun v290 () (_ BitVec 20))
(declare-fun v46 () (_ BitVec 20))
(declare-fun v150 () (_ BitVec 20))
(declare-fun v4 () (_ BitVec 20))
(declare-fun v190 () (_ BitVec 20))
(declare-fun v252 () (_ BitVec 20))
(declare-fun v71 () (_ BitVec 20))
(declare-fun v111 () (_ BitVec 20))
(declare-fun v219 () (_ BitVec 20))
(declare-fun v130 () (_ BitVec 20))
(declare-fun v161 () (_ BitVec 20))
(declare-fun v2 () (_ BitVec 20))
(declare-fun at () (Array (_ BitVec 20) (_ BitVec 20) ))
(declare-fun v40 () (_ BitVec 20))
(declare-fun v82 () (_ BitVec 20))
(declare-fun v122 () (_ BitVec 20))
(declare-fun v272 () (_ BitVec 20))
(declare-fun v230 () (_ BitVec 20))
(declare-fun v11 () (_ BitVec 20))
(declare-fun v23 () (_ BitVec 20))
(declare-fun v195 () (_ BitVec 20))
(declare-fun v8 () (_ BitVec 20))
(declare-fun v132 () (_ BitVec 20))
(declare-fun v172 () (_ BitVec 20))
(declare-fun v241 () (_ BitVec 20))
(declare-fun v93 () (_ BitVec 20))
(declare-fun v261 () (_ BitVec 20))
(declare-fun v201 () (_ BitVec 20))
(declare-fun v33 () (_ BitVec 20))
(declare-fun v283 () (_ BitVec 20))
(declare-fun v59 () (_ BitVec 20))
(declare-fun v143 () (_ BitVec 20))
(declare-fun v183 () (_ BitVec 20))
(declare-fun v104 () (_ BitVec 20))
(declare-fun v212 () (_ BitVec 20))
(declare-fun v294 () (_ BitVec 20))
(declare-fun v154 () (_ BitVec 20))
(declare-fun v75 () (_ BitVec 20))
(declare-fun v115 () (_ BitVec 20))
(declare-fun v265 () (_ BitVec 20))
(declare-fun v223 () (_ BitVec 20))
(declare-fun v165 () (_ BitVec 20))
(declare-fun v234 () (_ BitVec 20))
(declare-fun v86 () (_ BitVec 20))
(declare-fun v126 () (_ BitVec 20))
(declare-fun v276 () (_ BitVec 20))
(declare-fun v27 () (_ BitVec 20))
(declare-fun v15 () (_ BitVec 20))
(declare-fun v52 () (_ BitVec 20))
(declare-fun v136 () (_ BitVec 20))
(declare-fun v176 () (_ BitVec 20))
(declare-fun v245 () (_ BitVec 20))
(declare-fun v97 () (_ BitVec 20))
(declare-fun v205 () (_ BitVec 20))
(declare-fun v287 () (_ BitVec 20))
(declare-fun v32 () (_ BitVec 20))
(declare-fun v63 () (_ BitVec 20))
(declare-fun v147 () (_ BitVec 20))
(declare-fun v187 () (_ BitVec 20))
(declare-fun v131 () (_ BitVec 20))
(declare-fun v249 () (_ BitVec 20))
(declare-fun v68 () (_ BitVec 20))
(declare-fun v108 () (_ BitVec 20))
(declare-fun v216 () (_ BitVec 20))
(declare-fun v298 () (_ BitVec 20))
(declare-fun v158 () (_ BitVec 20))
(declare-fun v37 () (_ BitVec 20))
(declare-fun v79 () (_ BitVec 20))
(declare-fun v119 () (_ BitVec 20))
(declare-fun v269 () (_ BitVec 20))
(declare-fun v227 () (_ BitVec 20))
(declare-fun v20 () (_ BitVec 20))
(declare-fun v169 () (_ BitVec 20))
(declare-fun v238 () (_ BitVec 20))
(declare-fun v90 () (_ BitVec 20))
(declare-fun v258 () (_ BitVec 20))
(declare-fun v198 () (_ BitVec 20))
(declare-fun v280 () (_ BitVec 20))
(declare-fun v31 () (_ BitVec 20))
(declare-fun v56 () (_ BitVec 20))
(declare-fun v140 () (_ BitVec 20))
(declare-fun v180 () (_ BitVec 20))
(declare-fun v101 () (_ BitVec 20))
(declare-fun v209 () (_ BitVec 20))
(declare-fun v291 () (_ BitVec 20))
(declare-fun v47 () (_ BitVec 20))
(declare-fun v151 () (_ BitVec 20))
(declare-fun v191 () (_ BitVec 20))
(declare-fun v253 () (_ BitVec 20))
(declare-fun v72 () (_ BitVec 20))
(declare-fun v112 () (_ BitVec 20))
(declare-fun v220 () (_ BitVec 20))
(declare-fun v162 () (_ BitVec 20))
(declare-fun v5 () (_ BitVec 20))
(declare-fun v41 () (_ BitVec 20))
(declare-fun v83 () (_ BitVec 20))
(declare-fun v123 () (_ BitVec 20))
(declare-fun v273 () (_ BitVec 20))
(declare-fun v231 () (_ BitVec 20))
(declare-fun v24 () (_ BitVec 20))
(declare-fun v12 () (_ BitVec 20))
(declare-fun v17 () (_ BitVec 20))
(declare-fun v133 () (_ BitVec 20))
(declare-fun v173 () (_ BitVec 20))
(declare-fun v242 () (_ BitVec 20))
(declare-fun v94 () (_ BitVec 20))
(declare-fun v262 () (_ BitVec 20))
(declare-fun v202 () (_ BitVec 20))
(declare-fun v6 () (_ BitVec 20))
(declare-fun v284 () (_ BitVec 20))
(declare-fun v60 () (_ BitVec 20))
(declare-fun v144 () (_ BitVec 20))
(declare-fun v184 () (_ BitVec 20))
(declare-fun v105 () (_ BitVec 20))
(declare-fun v213 () (_ BitVec 20))
(declare-fun v295 () (_ BitVec 20))
(declare-fun v155 () (_ BitVec 20))
(declare-fun v34 () (_ BitVec 20))
(declare-fun v76 () (_ BitVec 20))
(declare-fun v116 () (_ BitVec 20))
(declare-fun v266 () (_ BitVec 20))
(declare-fun v224 () (_ BitVec 20))
(declare-fun v166 () (_ BitVec 20))
(declare-fun v235 () (_ BitVec 20))
(declare-fun v87 () (_ BitVec 20))
(declare-fun v127 () (_ BitVec 20))
(declare-fun v277 () (_ BitVec 20))
(declare-fun v28 () (_ BitVec 20))
(declare-fun v53 () (_ BitVec 20))
(declare-fun v137 () (_ BitVec 20))
(declare-fun v3 () (_ BitVec 20))
(declare-fun v177 () (_ BitVec 20))
(declare-fun v98 () (_ BitVec 20))
(declare-fun v206 () (_ BitVec 20))
(declare-fun v288 () (_ BitVec 20))
(declare-fun v246 () (_ BitVec 20))
(declare-fun v44 () (_ BitVec 20))
(declare-fun v128 () (_ BitVec 20))
(declare-fun v65 () (_ BitVec 20))
(declare-fun v148 () (_ BitVec 20))
(declare-fun v188 () (_ BitVec 20))
(declare-fun v250 () (_ BitVec 20))
(declare-fun v69 () (_ BitVec 20))
(declare-fun v109 () (_ BitVec 20))
(declare-fun v217 () (_ BitVec 20))
(declare-fun v299 () (_ BitVec 20))
(declare-fun v159 () (_ BitVec 20))
(declare-fun v38 () (_ BitVec 20))
(declare-fun v80 () (_ BitVec 20))
(declare-fun v120 () (_ BitVec 20))
(declare-fun v270 () (_ BitVec 20))
(declare-fun v228 () (_ BitVec 20))
(declare-fun v21 () (_ BitVec 20))
(declare-fun v193 () (_ BitVec 20))
(declare-fun v170 () (_ BitVec 20))
(declare-fun v239 () (_ BitVec 20))
(declare-fun v91 () (_ BitVec 20))
(declare-fun v259 () (_ BitVec 20))
(declare-fun v199 () (_ BitVec 20))
(assert (let ((?let_k_0 (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store
(store (store (store (store at (_ bv0 20) (_ bv0 20)) (_ bv1 20) (_
bv1 20)) (_ bv2 20) (_ bv2 20)) (_ bv3 20) (_ bv3 20)) (_ bv4 20) (_
bv4 20)) (_ bv5 20) (_ bv5 20)) (_ bv6 20) (_ bv6 20)) (_ bv7 20) (_
bv7 20)) (_ bv8 20) (_ bv8 20)) (_ bv9 20) (_ bv9 20)) (_ bv10 20) (_
bv10 20)) (_ bv11 20) (_ bv11 20)) (_ bv12 20) (_ bv12 20)) (_ bv13
20) (_ bv13 20)) (_ bv14 20) (_ bv14 20)) (_ bv15 20) (_ bv15 20)) (_
bv16 20) (_ bv16 20)) (_ bv17 20) (_ bv17 20)) (_ bv18 20) (_ bv18
20)) (_ bv19 20) (_ bv19 20)) (_ bv20 20) (_ bv20 20)) (_ bv21 20) (_
bv21 20)) (_ bv22 20) (_ bv22 20)) (_ bv23 20) (_ bv23 20)) (_ bv24
20) (_ bv24 20)) (_ bv25 20) (_ bv25 20)) (_ bv26 20) (_ bv26 20)) (_
bv27 20) (_ bv27 20)) (_ bv28 20) (_ bv28 20)) (_ bv29 20) (_ bv29
20)) (_ bv30 20) (_ bv30 20)) (_ bv31 20) (_ bv31 20)) (_ bv32 20) (_
bv32 20)) (_ bv33 20) (_ bv33 20)) (_ bv34 20) (_ bv34 20)) (_ bv35
20) (_ bv35 20)) (_ bv36 20) (_ bv36 20)) (_ bv37 20) (_ bv37 20)) (_
bv38 20) (_ bv38 20)) (_ bv39 20) (_ bv39 20)) (_ bv40 20) (_ bv40
20)) (_ bv41 20) (_ bv41 20)) (_ bv42 20) (_ bv42 20)) (_ bv43 20) (_
bv43 20)) (_ bv44 20) (_ bv44 20)) (_ bv45 20) (_ bv45 20)) (_ bv46
20) (_ bv46 20)) (_ bv47 20) (_ bv47 20)) (_ bv48 20) (_ bv48 20)) (_
bv49 20) (_ bv49 20)) (_ bv50 20) (_ bv50 20)) (_ bv51 20) (_ bv51
20)) (_ bv52 20) (_ bv52 20)) (_ bv53 20) (_ bv53 20)) (_ bv54 20) (_
bv54 20)) (_ bv55 20) (_ bv55 20)) (_ bv56 20) (_ bv56 20)) (_ bv57
20) (_ bv57 20)) (_ bv58 20) (_ bv58 20)) (_ bv59 20) (_ bv59 20)) (_
bv60 20) (_ bv60 20)) (_ bv61 20) (_ bv61 20)) (_ bv62 20) (_ bv62
20)) (_ bv63 20) (_ bv63 20)) (_ bv64 20) (_ bv64 20)) (_ bv65 20) (_
bv65 20)) (_ bv66 20) (_ bv66 20)) (_ bv67 20) (_ bv67 20)) (_ bv68
20) (_ bv68 20)) (_ bv69 20) (_ bv69 20)) (_ bv70 20) (_ bv70 20)) (_
bv71 20) (_ bv71 20)) (_ bv72 20) (_ bv72 20)) (_ bv73 20) (_ bv73
20)) (_ bv74 20) (_ bv74 20)) (_ bv75 20) (_ bv75 20)) (_ bv76 20) (_
bv76 20)) (_ bv77 20) (_ bv77 20)) (_ bv78 20) (_ bv78 20)) (_ bv79
20) (_ bv79 20)) (_ bv80 20) (_ bv80 20)) (_ bv81 20) (_ bv81 20)) (_
bv82 20) (_ bv82 20)) (_ bv83 20) (_ bv83 20)) (_ bv84 20) (_ bv84
20)) (_ bv85 20) (_ bv85 20)) (_ bv86 20) (_ bv86 20)) (_ bv87 20) (_
bv87 20)) (_ bv88 20) (_ bv88 20)) (_ bv89 20) (_ bv89 20)) (_ bv90
20) (_ bv90 20)) (_ bv91 20) (_ bv91 20)) (_ bv92 20) (_ bv92 20)) (_
bv93 20) (_ bv93 20)) (_ bv94 20) (_ bv94 20)) (_ bv95 20) (_ bv95
20)) (_ bv96 20) (_ bv96 20)) (_ bv97 20) (_ bv97 20)) (_ bv98 20) (_
bv98 20)) (_ bv99 20) (_ bv99 20)) (_ bv100 20) (_ bv100 20)) (_ bv101
20) (_ bv101 20)) (_ bv102 20) (_ bv102 20)) (_ bv103 20) (_ bv103
20)) (_ bv104 20) (_ bv104 20)) (_ bv105 20) (_ bv105 20)) (_ bv106
20) (_ bv106 20)) (_ bv107 20) (_ bv107 20)) (_ bv108 20) (_ bv108
20)) (_ bv109 20) (_ bv109 20)) (_ bv110 20) (_ bv110 20)) (_ bv111
20) (_ bv111 20)) (_ bv112 20) (_ bv112 20)) (_ bv113 20) (_ bv113
20)) (_ bv114 20) (_ bv114 20)) (_ bv115 20) (_ bv115 20)) (_ bv116
20) (_ bv116 20)) (_ bv117 20) (_ bv117 20)) (_ bv118 20) (_ bv118
20)) (_ bv119 20) (_ bv119 20)) (_ bv120 20) (_ bv120 20)) (_ bv121
20) (_ bv121 20)) (_ bv122 20) (_ bv122 20)) (_ bv123 20) (_ bv123
20)) (_ bv124 20) (_ bv124 20)) (_ bv125 20) (_ bv125 20)) (_ bv126
20) (_ bv126 20)) (_ bv127 20) (_ bv127 20)) (_ bv128 20) (_ bv128
20)) (_ bv129 20) (_ bv129 20)) (_ bv130 20) (_ bv130 20)) (_ bv131
20) (_ bv131 20)) (_ bv132 20) (_ bv132 20)) (_ bv133 20) (_ bv133
20)) (_ bv134 20) (_ bv134 20)) (_ bv135 20) (_ bv135 20)) (_ bv136
20) (_ bv136 20)) (_ bv137 20) (_ bv137 20)) (_ bv138 20) (_ bv138
20)) (_ bv139 20) (_ bv139 20)) (_ bv140 20) (_ bv140 20)) (_ bv141
20) (_ bv141 20)) (_ bv142 20) (_ bv142 20)) (_ bv143 20) (_ bv143
20)) (_ bv144 20) (_ bv144 20)) (_ bv145 20) (_ bv145 20)) (_ bv146
20) (_ bv146 20)) (_ bv147 20) (_ bv147 20)) (_ bv148 20) (_ bv148
20)) (_ bv149 20) (_ bv149 20)) (_ bv150 20) (_ bv150 20)) (_ bv151
20) (_ bv151 20)) (_ bv152 20) (_ bv152 20)) (_ bv153 20) (_ bv153
20)) (_ bv154 20) (_ bv154 20)) (_ bv155 20) (_ bv155 20)) (_ bv156
20) (_ bv156 20)) (_ bv157 20) (_ bv157 20)) (_ bv158 20) (_ bv158
20)) (_ bv159 20) (_ bv159 20)) (_ bv160 20) (_ bv160 20)) (_ bv161
20) (_ bv161 20)) (_ bv162 20) (_ bv162 20)) (_ bv163 20) (_ bv163
20)) (_ bv164 20) (_ bv164 20)) (_ bv165 20) (_ bv165 20)) (_ bv166
20) (_ bv166 20)) (_ bv167 20) (_ bv167 20)) (_ bv168 20) (_ bv168
20)) (_ bv169 20) (_ bv169 20)) (_ bv170 20) (_ bv170 20)) (_ bv171
20) (_ bv171 20)) (_ bv172 20) (_ bv172 20)) (_ bv173 20) (_ bv173
20)) (_ bv174 20) (_ bv174 20)) (_ bv175 20) (_ bv175 20)) (_ bv176
20) (_ bv176 20)) (_ bv177 20) (_ bv177 20)) (_ bv178 20) (_ bv178
20)) (_ bv179 20) (_ bv179 20)) (_ bv180 20) (_ bv180 20)) (_ bv181
20) (_ bv181 20)) (_ bv182 20) (_ bv182 20)) (_ bv183 20) (_ bv183
20)) (_ bv184 20) (_ bv184 20)) (_ bv185 20) (_ bv185 20)) (_ bv186
20) (_ bv186 20)) (_ bv187 20) (_ bv187 20)) (_ bv188 20) (_ bv188
20)) (_ bv189 20) (_ bv189 20)) (_ bv190 20) (_ bv190 20)) (_ bv191
20) (_ bv191 20)) (_ bv192 20) (_ bv192 20)) (_ bv193 20) (_ bv193
20)) (_ bv194 20) (_ bv194 20)) (_ bv195 20) (_ bv195 20)) (_ bv196
20) (_ bv196 20)) (_ bv197 20) (_ bv197 20)) (_ bv198 20) (_ bv198
20)) (_ bv199 20) (_ bv199 20)) (_ bv200 20) (_ bv200 20)) (_ bv201
20) (_ bv201 20)) (_ bv202 20) (_ bv202 20)) (_ bv203 20) (_ bv203
20)) (_ bv204 20) (_ bv204 20)) (_ bv205 20) (_ bv205 20)) (_ bv206
20) (_ bv206 20)) (_ bv207 20) (_ bv207 20)) (_ bv208 20) (_ bv208
20)) (_ bv209 20) (_ bv209 20)) (_ bv210 20) (_ bv210 20)) (_ bv211
20) (_ bv211 20)) (_ bv212 20) (_ bv212 20)) (_ bv213 20) (_ bv213
20)) (_ bv214 20) (_ bv214 20)) (_ bv215 20) (_ bv215 20)) (_ bv216
20) (_ bv216 20)) (_ bv217 20) (_ bv217 20)) (_ bv218 20) (_ bv218
20)) (_ bv219 20) (_ bv219 20)) (_ bv220 20) (_ bv220 20)) (_ bv221
20) (_ bv221 20)) (_ bv222 20) (_ bv222 20)) (_ bv223 20) (_ bv223
20)) (_ bv224 20) (_ bv224 20)) (_ bv225 20) (_ bv225 20)) (_ bv226
20) (_ bv226 20)) (_ bv227 20) (_ bv227 20)) (_ bv228 20) (_ bv228
20)) (_ bv229 20) (_ bv229 20)) (_ bv230 20) (_ bv230 20)) (_ bv231
20) (_ bv231 20)) (_ bv232 20) (_ bv232 20)) (_ bv233 20) (_ bv233
20)) (_ bv234 20) (_ bv234 20)) (_ bv235 20) (_ bv235 20)) (_ bv236
20) (_ bv236 20)) (_ bv237 20) (_ bv237 20)) (_ bv238 20) (_ bv238
20)) (_ bv239 20) (_ bv239 20)) (_ bv240 20) (_ bv240 20)) (_ bv241
20) (_ bv241 20)) (_ bv242 20) (_ bv242 20)) (_ bv243 20) (_ bv243
20)) (_ bv244 20) (_ bv244 20)) (_ bv245 20) (_ bv245 20)) (_ bv246
20) (_ bv246 20)) (_ bv247 20) (_ bv247 20)) (_ bv248 20) (_ bv248
20)) (_ bv249 20) (_ bv249 20)) (_ bv250 20) (_ bv250 20)) (_ bv251
20) (_ bv251 20)) (_ bv252 20) (_ bv252 20)) (_ bv253 20) (_ bv253
20)) (_ bv254 20) (_ bv254 20)) (_ bv255 20) (_ bv255 20)) (_ bv256
20) (_ bv256 20)) (_ bv257 20) (_ bv257 20)) (_ bv258 20) (_ bv258
20)) (_ bv259 20) (_ bv259 20)) (_ bv260 20) (_ bv260 20)) (_ bv261
20) (_ bv261 20)) (_ bv262 20) (_ bv262 20)) (_ bv263 20) (_ bv263
20)) (_ bv264 20) (_ bv264 20)) (_ bv265 20) (_ bv265 20)) (_ bv266
20) (_ bv266 20)) (_ bv267 20) (_ bv267 20)) (_ bv268 20) (_ bv268
20)) (_ bv269 20) (_ bv269 20)) (_ bv270 20) (_ bv270 20)) (_ bv271
20) (_ bv271 20)) (_ bv272 20) (_ bv272 20)) (_ bv273 20) (_ bv273
20)) (_ bv274 20) (_ bv274 20)) (_ bv275 20) (_ bv275 20)) (_ bv276
20) (_ bv276 20)) (_ bv277 20) (_ bv277 20)) (_ bv278 20) (_ bv278
20)) (_ bv279 20) (_ bv279 20)) (_ bv280 20) (_ bv280 20)) (_ bv281
20) (_ bv281 20)) (_ bv282 20) (_ bv282 20)) (_ bv283 20) (_ bv283
20)) (_ bv284 20) (_ bv284 20)) (_ bv285 20) (_ bv285 20)) (_ bv286
20) (_ bv286 20)) (_ bv287 20) (_ bv287 20)) (_ bv288 20) (_ bv288
20)) (_ bv289 20) (_ bv289 20)) (_ bv290 20) (_ bv290 20)) (_ bv291
20) (_ bv291 20)) (_ bv292 20) (_ bv292 20)) (_ bv293 20) (_ bv293
20)) (_ bv294 20) (_ bv294 20)) (_ bv295 20) (_ bv295 20)) (_ bv296
20) (_ bv296 20)) (_ bv297 20) (_ bv297 20)) (_ bv298 20) (_ bv298
20)) (_ bv299 20) (_ bv299 20)) ))
(and (= v0 (select ?let_k_0 v0)) (and (= v1 (select ?let_k_0 v1)) (and
(= v2 (select ?let_k_0 v2)) (and (= v3 (select ?let_k_0 v3)) (and (=
v4 (select ?let_k_0 v4)) (and (= v5 (select ?let_k_0 v5)) (and (= v6
(select ?let_k_0 v6)) (and (= v7 (select ?let_k_0 v7)) (and (= v8
(select ?let_k_0 v8)) (and (= v9 (select ?let_k_0 v9)) (and (= v10
(select ?let_k_0 v10)) (and (= v11 (select ?let_k_0 v11)) (and (= v12
(select ?let_k_0 v12)) (and (= v13 (select ?let_k_0 v13)) (and (= v14
(select ?let_k_0 v14)) (and (= v15 (select ?let_k_0 v15)) (and (= v16
(select ?let_k_0 v16)) (and (= v17 (select ?let_k_0 v17)) (and (= v18
(select ?let_k_0 v18)) (and (= v19 (select ?let_k_0 v19)) (and (= v20
(select ?let_k_0 v20)) (and (= v21 (select ?let_k_0 v21)) (and (= v22
(select ?let_k_0 v22)) (and (= v23 (select ?let_k_0 v23)) (and (= v24
(select ?let_k_0 v24)) (and (= v25 (select ?let_k_0 v25)) (and (= v26
(select ?let_k_0 v26)) (and (= v27 (select ?let_k_0 v27)) (and (= v28
(select ?let_k_0 v28)) (and (= v29 (select ?let_k_0 v29)) (and (= v30
(select ?let_k_0 v30)) (and (= v31 (select ?let_k_0 v31)) (and (= v32
(select ?let_k_0 v32)) (and (= v33 (select ?let_k_0 v33)) (and (= v34
(select ?let_k_0 v34)) (and (= v35 (select ?let_k_0 v35)) (and (= v36
(select ?let_k_0 v36)) (and (= v37 (select ?let_k_0 v37)) (and (= v38
(select ?let_k_0 v38)) (and (= v39 (select ?let_k_0 v39)) (and (= v40
(select ?let_k_0 v40)) (and (= v41 (select ?let_k_0 v41)) (and (= v42
(select ?let_k_0 v42)) (and (= v43 (select ?let_k_0 v43)) (and (= v44
(select ?let_k_0 v44)) (and (= v45 (select ?let_k_0 v45)) (and (= v46
(select ?let_k_0 v46)) (and (= v47 (select ?let_k_0 v47)) (and (= v48
(select ?let_k_0 v48)) (and (= v49 (select ?let_k_0 v49)) (and (= v50
(select ?let_k_0 v50)) (and (= v51 (select ?let_k_0 v51)) (and (= v52
(select ?let_k_0 v52)) (and (= v53 (select ?let_k_0 v53)) (and (= v54
(select ?let_k_0 v54)) (and (= v55 (select ?let_k_0 v55)) (and (= v56
(select ?let_k_0 v56)) (and (= v57 (select ?let_k_0 v57)) (and (= v58
(select ?let_k_0 v58)) (and (= v59 (select ?let_k_0 v59)) (and (= v60
(select ?let_k_0 v60)) (and (= v61 (select ?let_k_0 v61)) (and (= v62
(select ?let_k_0 v62)) (and (= v63 (select ?let_k_0 v63)) (and (= v64
(select ?let_k_0 v64)) (and (= v65 (select ?let_k_0 v65)) (and (= v66
(select ?let_k_0 v66)) (and (= v67 (select ?let_k_0 v67)) (and (= v68
(select ?let_k_0 v68)) (and (= v69 (select ?let_k_0 v69)) (and (= v70
(select ?let_k_0 v70)) (and (= v71 (select ?let_k_0 v71)) (and (= v72
(select ?let_k_0 v72)) (and (= v73 (select ?let_k_0 v73)) (and (= v74
(select ?let_k_0 v74)) (and (= v75 (select ?let_k_0 v75)) (and (= v76
(select ?let_k_0 v76)) (and (= v77 (select ?let_k_0 v77)) (and (= v78
(select ?let_k_0 v78)) (and (= v79 (select ?let_k_0 v79)) (and (= v80
(select ?let_k_0 v80)) (and (= v81 (select ?let_k_0 v81)) (and (= v82
(select ?let_k_0 v82)) (and (= v83 (select ?let_k_0 v83)) (and (= v84
(select ?let_k_0 v84)) (and (= v85 (select ?let_k_0 v85)) (and (= v86
(select ?let_k_0 v86)) (and (= v87 (select ?let_k_0 v87)) (and (= v88
(select ?let_k_0 v88)) (and (= v89 (select ?let_k_0 v89)) (and (= v90
(select ?let_k_0 v90)) (and (= v91 (select ?let_k_0 v91)) (and (= v92
(select ?let_k_0 v92)) (and (= v93 (select ?let_k_0 v93)) (and (= v94
(select ?let_k_0 v94)) (and (= v95 (select ?let_k_0 v95)) (and (= v96
(select ?let_k_0 v96)) (and (= v97 (select ?let_k_0 v97)) (and (= v98
(select ?let_k_0 v98)) (and (= v99 (select ?let_k_0 v99)) (and (= v100
(select ?let_k_0 v100)) (and (= v101 (select ?let_k_0 v101)) (and (=
v102 (select ?let_k_0 v102)) (and (= v103 (select ?let_k_0 v103)) (and
(= v104 (select ?let_k_0 v104)) (and (= v105 (select ?let_k_0 v105))
(and (= v106 (select ?let_k_0 v106)) (and (= v107 (select ?let_k_0
v107)) (and (= v108 (select ?let_k_0 v108)) (and (= v109 (select ?
let_k_0 v109)) (and (= v110 (select ?let_k_0 v110)) (and (= v111
(select ?let_k_0 v111)) (and (= v112 (select ?let_k_0 v112)) (and (=
v113 (select ?let_k_0 v113)) (and (= v114 (select ?let_k_0 v114)) (and
(= v115 (select ?let_k_0 v115)) (and (= v116 (select ?let_k_0 v116))
(and (= v117 (select ?let_k_0 v117)) (and (= v118 (select ?let_k_0
v118)) (and (= v119 (select ?let_k_0 v119)) (and (= v120 (select ?
let_k_0 v120)) (and (= v121 (select ?let_k_0 v121)) (and (= v122
(select ?let_k_0 v122)) (and (= v123 (select ?let_k_0 v123)) (and (=
v124 (select ?let_k_0 v124)) (and (= v125 (select ?let_k_0 v125)) (and
(= v126 (select ?let_k_0 v126)) (and (= v127 (select ?let_k_0 v127))
(and (= v128 (select ?let_k_0 v128)) (and (= v129 (select ?let_k_0
v129)) (and (= v130 (select ?let_k_0 v130)) (and (= v131 (select ?
let_k_0 v131)) (and (= v132 (select ?let_k_0 v132)) (and (= v133
(select ?let_k_0 v133)) (and (= v134 (select ?let_k_0 v134)) (and (=
v135 (select ?let_k_0 v135)) (and (= v136 (select ?let_k_0 v136)) (and
(= v137 (select ?let_k_0 v137)) (and (= v138 (select ?let_k_0 v138))
(and (= v139 (select ?let_k_0 v139)) (and (= v140 (select ?let_k_0
v140)) (and (= v141 (select ?let_k_0 v141)) (and (= v142 (select ?
let_k_0 v142)) (and (= v143 (select ?let_k_0 v143)) (and (= v144
(select ?let_k_0 v144)) (and (= v145 (select ?let_k_0 v145)) (and (=
v146 (select ?let_k_0 v146)) (and (= v147 (select ?let_k_0 v147)) (and
(= v148 (select ?let_k_0 v148)) (and (= v149 (select ?let_k_0 v149))
(and (= v150 (select ?let_k_0 v150)) (and (= v151 (select ?let_k_0
v151)) (and (= v152 (select ?let_k_0 v152)) (and (= v153 (select ?
let_k_0 v153)) (and (= v154 (select ?let_k_0 v154)) (and (= v155
(select ?let_k_0 v155)) (and (= v156 (select ?let_k_0 v156)) (and (=
v157 (select ?let_k_0 v157)) (and (= v158 (select ?let_k_0 v158)) (and
(= v159 (select ?let_k_0 v159)) (and (= v160 (select ?let_k_0 v160))
(and (= v161 (select ?let_k_0 v161)) (and (= v162 (select ?let_k_0
v162)) (and (= v163 (select ?let_k_0 v163)) (and (= v164 (select ?
let_k_0 v164)) (and (= v165 (select ?let_k_0 v165)) (and (= v166
(select ?let_k_0 v166)) (and (= v167 (select ?let_k_0 v167)) (and (=
v168 (select ?let_k_0 v168)) (and (= v169 (select ?let_k_0 v169)) (and
(= v170 (select ?let_k_0 v170)) (and (= v171 (select ?let_k_0 v171))
(and (= v172 (select ?let_k_0 v172)) (and (= v173 (select ?let_k_0
v173)) (and (= v174 (select ?let_k_0 v174)) (and (= v175 (select ?
let_k_0 v175)) (and (= v176 (select ?let_k_0 v176)) (and (= v177
(select ?let_k_0 v177)) (and (= v178 (select ?let_k_0 v178)) (and (=
v179 (select ?let_k_0 v179)) (and (= v180 (select ?let_k_0 v180)) (and
(= v181 (select ?let_k_0 v181)) (and (= v182 (select ?let_k_0 v182))
(and (= v183 (select ?let_k_0 v183)) (and (= v184 (select ?let_k_0
v184)) (and (= v185 (select ?let_k_0 v185)) (and (= v186 (select ?
let_k_0 v186)) (and (= v187 (select ?let_k_0 v187)) (and (= v188
(select ?let_k_0 v188)) (and (= v189 (select ?let_k_0 v189)) (and (=
v190 (select ?let_k_0 v190)) (and (= v191 (select ?let_k_0 v191)) (and
(= v192 (select ?let_k_0 v192)) (and (= v193 (select ?let_k_0 v193))
(and (= v194 (select ?let_k_0 v194)) (and (= v195 (select ?let_k_0
v195)) (and (= v196 (select ?let_k_0 v196)) (and (= v197 (select ?
let_k_0 v197)) (and (= v198 (select ?let_k_0 v198)) (and (= v199
(select ?let_k_0 v199)) (and (= v200 (select ?let_k_0 v200)) (and (=
v201 (select ?let_k_0 v201)) (and (= v202 (select ?let_k_0 v202)) (and
(= v203 (select ?let_k_0 v203)) (and (= v204 (select ?let_k_0 v204))
(and (= v205 (select ?let_k_0 v205)) (and (= v206 (select ?let_k_0
v206)) (and (= v207 (select ?let_k_0 v207)) (and (= v208 (select ?
let_k_0 v208)) (and (= v209 (select ?let_k_0 v209)) (and (= v210
(select ?let_k_0 v210)) (and (= v211 (select ?let_k_0 v211)) (and (=
v212 (select ?let_k_0 v212)) (and (= v213 (select ?let_k_0 v213)) (and
(= v214 (select ?let_k_0 v214)) (and (= v215 (select ?let_k_0 v215))
(and (= v216 (select ?let_k_0 v216)) (and (= v217 (select ?let_k_0
v217)) (and (= v218 (select ?let_k_0 v218)) (and (= v219 (select ?
let_k_0 v219)) (and (= v220 (select ?let_k_0 v220)) (and (= v221
(select ?let_k_0 v221)) (and (= v222 (select ?let_k_0 v222)) (and (=
v223 (select ?let_k_0 v223)) (and (= v224 (select ?let_k_0 v224)) (and
(= v225 (select ?let_k_0 v225)) (and (= v226 (select ?let_k_0 v226))
(and (= v227 (select ?let_k_0 v227)) (and (= v228 (select ?let_k_0
v228)) (and (= v229 (select ?let_k_0 v229)) (and (= v230 (select ?
let_k_0 v230)) (and (= v231 (select ?let_k_0 v231)) (and (= v232
(select ?let_k_0 v232)) (and (= v233 (select ?let_k_0 v233)) (and (=
v234 (select ?let_k_0 v234)) (and (= v235 (select ?let_k_0 v235)) (and
(= v236 (select ?let_k_0 v236)) (and (= v237 (select ?let_k_0 v237))
(and (= v238 (select ?let_k_0 v238)) (and (= v239 (select ?let_k_0
v239)) (and (= v240 (select ?let_k_0 v240)) (and (= v241 (select ?
let_k_0 v241)) (and (= v242 (select ?let_k_0 v242)) (and (= v243
(select ?let_k_0 v243)) (and (= v244 (select ?let_k_0 v244)) (and (=
v245 (select ?let_k_0 v245)) (and (= v246 (select ?let_k_0 v246)) (and
(= v247 (select ?let_k_0 v247)) (and (= v248 (select ?let_k_0 v248))
(and (= v249 (select ?let_k_0 v249)) (and (= v250 (select ?let_k_0
v250)) (and (= v251 (select ?let_k_0 v251)) (and (= v252 (select ?
let_k_0 v252)) (and (= v253 (select ?let_k_0 v253)) (and (= v254
(select ?let_k_0 v254)) (and (= v255 (select ?let_k_0 v255)) (and (=
v256 (select ?let_k_0 v256)) (and (= v257 (select ?let_k_0 v257)) (and
(= v258 (select ?let_k_0 v258)) (and (= v259 (select ?let_k_0 v259))
(and (= v260 (select ?let_k_0 v260)) (and (= v261 (select ?let_k_0
v261)) (and (= v262 (select ?let_k_0 v262)) (and (= v263 (select ?
let_k_0 v263)) (and (= v264 (select ?let_k_0 v264)) (and (= v265
(select ?let_k_0 v265)) (and (= v266 (select ?let_k_0 v266)) (and (=
v267 (select ?let_k_0 v267)) (and (= v268 (select ?let_k_0 v268)) (and
(= v269 (select ?let_k_0 v269)) (and (= v270 (select ?let_k_0 v270))
(and (= v271 (select ?let_k_0 v271)) (and (= v272 (select ?let_k_0
v272)) (and (= v273 (select ?let_k_0 v273)) (and (= v274 (select ?
let_k_0 v274)) (and (= v275 (select ?let_k_0 v275)) (and (= v276
(select ?let_k_0 v276)) (and (= v277 (select ?let_k_0 v277)) (and (=
v278 (select ?let_k_0 v278)) (and (= v279 (select ?let_k_0 v279)) (and
(= v280 (select ?let_k_0 v280)) (and (= v281 (select ?let_k_0 v281))
(and (= v282 (select ?let_k_0 v282)) (and (= v283 (select ?let_k_0
v283)) (and (= v284 (select ?let_k_0 v284)) (and (= v285 (select ?
let_k_0 v285)) (and (= v286 (select ?let_k_0 v286)) (and (= v287
(select ?let_k_0 v287)) (and (= v288 (select ?let_k_0 v288)) (and (=
v289 (select ?let_k_0 v289)) (and (= v290 (select ?let_k_0 v290)) (and
(= v291 (select ?let_k_0 v291)) (and (= v292 (select ?let_k_0 v292))
(and (= v293 (select ?let_k_0 v293)) (and (= v294 (select ?let_k_0
v294)) (and (= v295 (select ?let_k_0 v295)) (and (= v296 (select ?
let_k_0 v296)) (and (= v297 (select ?let_k_0 v297)) (and (= v298
(select ?let_k_0 v298)) (= v299 (select ?let_k_0
v299))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )
)
(check-sat)
(exit)
Reply all
Reply to author
Forward
0 new messages