search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.26k stars 1.48k forks source link

Z3 opt: unknown but no model #139

Closed zpavlinovic closed 9 years ago

zpavlinovic commented 9 years ago

The attached script finishes immediately with unknown giving no model. Patterns are used and model based quantifier instantiation is turned off.

Tried suggestions from the following links with no success: http://stackoverflow.com/questions/22670784/why-does-z3-return-unknown-on-this-simple-input http://stackoverflow.com/questions/15806141/keep-getting-unknown-result-with-pattern-usage-in-smtlib-v2-input

Should a particular solver be used to get the model? Sorry for the long script.

(set-option :print-success false)
(set-info :smt-lib-version 2.0)
(set-option :MODEL.V2 true)
(set-option :auto-config false)
(set-option :smt.mbqi false)

(declare-fun tickleBool (Bool) Bool)
(assert (and (tickleBool true) (tickleBool false)))
(declare-fun strConst__li2bpl11 () Int)
(declare-fun strConst__li2bpl2 () Int)
(declare-fun strConst__li2bpl9 () Int)
(declare-fun strConst__li2bpl6 () Int)
(declare-fun strConst__li2bpl10 () Int)
(declare-fun strConst__li2bpl7 () Int)
(declare-fun strConst__li2bpl8 () Int)
(declare-fun strConst__li2bpl3 () Int)
(declare-fun strConst__li2bpl5 () Int)
(declare-fun strConst__li2bpl4 () Int)
(declare-fun strConst__li2bpl1 () Int)
(declare-fun strConst__li2bpl12 () Int)
(declare-fun strConst__li2bpl0 () Int)
(declare-fun NULL () Int)
(declare-fun li2bplFunctionConstant190 () Int)
(declare-fun li2bplFunctionConstant201 () Int)
(declare-fun li2bplFunctionConstant204 () Int)
(declare-fun li2bplFunctionConstant206 () Int)
(declare-fun li2bplFunctionConstant207 () Int)
(declare-fun li2bplFunctionConstant209 () Int)
(declare-fun li2bplFunctionConstant210 () Int)
(declare-fun li2bplFunctionConstant211 () Int)
(declare-fun li2bplFunctionConstant217 () Int)
(declare-fun li2bplFunctionConstant228 () Int)
(declare-fun li2bplFunctionConstant247 () Int)
(declare-fun li2bplFunctionConstant250 () Int)
(declare-fun li2bplFunctionConstant298 () Int)
(declare-fun li2bplFunctionConstant300 () Int)
(declare-fun li2bplFunctionConstant303 () Int)
(declare-fun POW2 (Int) Bool)
(declare-fun BAND (Int Int) Int)
(declare-fun BOR (Int Int) Int)
(declare-fun BNOT (Int) Int)
(assert (distinct strConst__li2bpl11 strConst__li2bpl2 strConst__li2bpl9 strConst__li2bpl6 strConst__li2bpl10 strConst__li2bpl7 strConst__li2bpl8 strConst__li2bpl3 strConst__li2bpl5 strConst__li2bpl4 strConst__li2bpl1 strConst__li2bpl12 strConst__li2bpl0)
)
(assert (= NULL 0))
(assert (= li2bplFunctionConstant190 190))
(assert (= li2bplFunctionConstant201 201))
(assert (= li2bplFunctionConstant204 204))
(assert (= li2bplFunctionConstant206 206))
(assert (= li2bplFunctionConstant207 207))
(assert (= li2bplFunctionConstant209 209))
(assert (= li2bplFunctionConstant210 210))
(assert (= li2bplFunctionConstant211 211))
(assert (= li2bplFunctionConstant217 217))
(assert (= li2bplFunctionConstant228 228))
(assert (= li2bplFunctionConstant247 247))
(assert (= li2bplFunctionConstant250 250))
(assert (= li2bplFunctionConstant298 298))
(assert (= li2bplFunctionConstant300 300))
(assert (= li2bplFunctionConstant303 303))
(assert (forall ((x Int) ) (!  (=> (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (= x 0) (= x 1)) (= x 2)) (= x 4)) (= x 8)) (= x 16)) (= x 32)) (= x 64)) (= x 128)) (= x 256)) (= x 512)) (= x 1024)) (= x 2048)) (= x 4096)) (= x 8192)) (= x 16384)) (= x 32768)) (= x 65536)) (= x 131072)) (= x 262144)) (= x 524288)) (= x 1048576)) (= x 2097152)) (= x 4194304)) (= x 8388608)) (= x 16777216)) (= x 33554432)) (= x 67108864)) (= x 134217728)) (= x 268435456)) (= x 536870912)) (= x 1073741824)) (= x 2147483648)) (= x (- 0 2147483648))) (POW2 x))
 :qid |fdcfailc.17323:15|
 :skolemid |4|
 :pattern ( (POW2 x))
)))
(assert (forall ((f Int) ) (! (= (BAND 0 f) 0)
 :qid |fdcfailc.17325:15|
 :skolemid |5|
 :pattern ( (BAND 0 f))
)))
(assert (forall ((f@@0 Int) ) (! (= (BAND f@@0 f@@0) f@@0)
 :qid |fdcfailc.17327:15|
 :skolemid |6|
 :pattern ( (BAND f@@0 f@@0))
)))
(assert (forall ((f@@1 Int) ) (! (= (BOR 0 f@@1) f@@1)
 :qid |fdcfailc.17329:15|
 :skolemid |7|
 :pattern ( (BOR 0 f@@1))
)))
(assert (forall ((f@@2 Int) ) (! (= (BOR f@@2 0) f@@2)
 :qid |fdcfailc.17331:15|
 :skolemid |8|
 :pattern ( (BOR f@@2 0))
)))
(assert (forall ((x@@0 Int) (f@@3 Int) ) (!  (=> (and (and (POW2 x@@0) (POW2 f@@3)) (not (= x@@0 f@@3))) (= (BAND x@@0 f@@3) 0))
 :qid |fdcfailc.17333:15|
 :skolemid |9|
 :pattern ( (BAND x@@0 f@@3))
)))
(assert (forall ((a Int) (b Int) (c Int) ) (! (= (BOR a (BOR b c)) (BOR (BOR a b) c))
 :qid |fdcfailc.17335:15|
 :skolemid |10|
 :pattern ( (BOR a (BOR b c)))
)))
(assert (forall ((a@@0 Int) (b@@0 Int) (c@@0 Int) ) (! (= (BAND a@@0 (BOR b@@0 c@@0)) (BAND (BOR b@@0 c@@0) a@@0))
 :qid |fdcfailc.17337:15|
 :skolemid |11|
 :pattern ( (BAND a@@0 (BOR b@@0 c@@0)))
)))
(assert (forall ((x@@1 Int) (f1 Int) (f2 Int) ) (!  (and (=> (and (and (not (= f1 f2)) (POW2 f1)) (POW2 f2)) (= (BAND (BOR x@@1 f1) f2) (BAND x@@1 f2))) (=> (= f1 f2) (= (BAND (BOR x@@1 f1) f2) f1)))
 :qid |fdcfailc.17339:15|
 :skolemid |12|
 :pattern ( (BAND (BOR x@@1 f1) f2))
)))
(assert (forall ((x@@2 Int) (f1@@0 Int) (f2@@0 Int) ) (!  (and (=> (and (and (not (= f1@@0 f2@@0)) (POW2 f1@@0)) (POW2 f2@@0)) (= (BAND (BAND x@@2 (BNOT f1@@0)) f2@@0) (BAND x@@2 f2@@0))) (=> (and (and (= f1@@0 f2@@0) (POW2 f1@@0)) (POW2 f2@@0)) (= (BAND (BAND x@@2 (BNOT f1@@0)) f2@@0) 0)))
 :qid |fdcfailc.17341:15|
 :skolemid |13|
 :pattern ( (BAND (BAND x@@2 (BNOT f1@@0)) f2@@0))
)))
(assert (forall ((x@@3 Int) (f1@@1 Int) (f2@@1 Int) ) (!  (and (=> (and (and (not (= f1@@1 f2@@1)) (POW2 f1@@1)) (POW2 f2@@1)) (= (BAND (BOR f1@@1 x@@3) f2@@1) (BAND x@@3 f2@@1))) (=> (= f1@@1 f2@@1) (= (BAND (BOR f1@@1 x@@3) f2@@1) f1@@1)))
 :qid |fdcfailc.17343:15|
 :skolemid |14|
 :pattern ( (BAND (BOR f1@@1 x@@3) f2@@1))
)))
(assert (forall ((x@@4 Int) (y Int) (f2@@2 Int) ) (!  (=> (POW2 f2@@2) (or (= (BAND (BAND x@@4 y) f2@@2) 0) (= (BAND (BAND x@@4 y) f2@@2) (BAND x@@4 f2@@2))))
 :qid |fdcfailc.17345:15|
 :skolemid |15|
 :pattern ( (BAND (BAND x@@4 y) f2@@2))
)))
(assert true)
(push 1)
(declare-fun ControlFlow (Int Int) Int)
(declare-fun %lbl%+SI11 () Bool)
(declare-fun %lbl%@SI12 () Bool)
(declare-fun SIV@235 () Int)
(declare-fun SIV@765 () Int)
(declare-fun SIV@236 () Int)
(declare-fun SIV@587 () Int)
(declare-fun SIV@237 () Int)
(declare-fun SIV@696 () Int)
(declare-fun SIV@238 () Int)
(declare-fun SIV@559 () Int)
(declare-fun SIV@239 () Int)
(declare-fun SIV@607 () Int)
(declare-fun SIV@240 () Int)
(declare-fun SIV@693 () Int)
(declare-fun SIV@241 () Int)
(declare-fun SIV@758 () Int)
(declare-fun SIV@242 () Int)
(declare-fun SIV@593 () Int)
(declare-fun SIV@243 () Int)
(declare-fun SIV@592 () Int)
(declare-fun SIV@244 () Int)
(declare-fun SIV@591 () Int)
(declare-fun SIV@245 () Int)
(declare-fun SIV@590 () Int)
(declare-fun SIV@246 () Int)
(declare-fun SIV@589 () Int)
(declare-fun SIV@247 () Int)
(declare-fun SIV@588 () Int)
(declare-fun SIV@248 () Int)
(declare-fun SIV@604 () Int)
(declare-fun SIV@249 () Int)
(declare-fun SIV@613 () Int)
(declare-fun SIV@250 () Int)
(declare-fun SIV@695 () Int)
(declare-fun SIV@251 () Int)
(declare-fun SIV@605 () Int)
(declare-fun SIV@252 () Int)
(declare-fun SIV@746 () Int)
(declare-fun SIV@253 () (Array Int Int))
(declare-fun SIV@598 () (Array Int Int))
(declare-fun SIV@254 () (Array Int Int))
(declare-fun SIV@584 () (Array Int Int))
(declare-fun SIV@255 () (Array Int Int))
(declare-fun SIV@586 () (Array Int Int))
(declare-fun SIV@256 () (Array Int Int))
(declare-fun SIV@594 () (Array Int Int))
(declare-fun SIV@257 () (Array Int Int))
(declare-fun SIV@595 () (Array Int Int))
(declare-fun SIV@258 () (Array Int Int))
(declare-fun SIV@596 () (Array Int Int))
(declare-fun SIV@259 () Int)
(declare-fun SIV@626 () Int)
(declare-fun SIV@260 () Int)
(declare-fun SIV@691 () Int)
(declare-fun SIV@261 () Int)
(declare-fun SIV@619 () Int)
(declare-fun SIV@262 () (Array Int Int))
(declare-fun SIV@597 () (Array Int Int))
(declare-fun SIV@263 () (Array Int Int))
(declare-fun SIV@599 () (Array Int Int))
(declare-fun SIV@264 () (Array Int Int))
(declare-fun SIV@600 () (Array Int Int))
(declare-fun SIV@265 () (Array Int Int))
(declare-fun SIV@601 () (Array Int Int))
(declare-fun SIV@266 () (Array Int Int))
(declare-fun SIV@602 () (Array Int Int))
(declare-fun SIV@267 () (Array Int Int))
(declare-fun SIV@603 () (Array Int Int))
(declare-fun SIV@268 () (Array Int Int))
(declare-fun SIV@606 () (Array Int Int))
(declare-fun SIV@269 () (Array Int Int))
(declare-fun SIV@608 () (Array Int Int))
(declare-fun SIV@270 () Int)
(declare-fun SIV@609 () Int)
(declare-fun SIV@271 () (Array Int Int))
(declare-fun SIV@610 () (Array Int Int))
(declare-fun SIV@272 () (Array Int Int))
(declare-fun SIV@611 () (Array Int Int))
(declare-fun SIV@273 () (Array Int Int))
(declare-fun SIV@612 () (Array Int Int))
(declare-fun SIV@274 () (Array Int Int))
(declare-fun SIV@614 () (Array Int Int))
(declare-fun SIV@275 () (Array Int Int))
(declare-fun SIV@615 () (Array Int Int))
(declare-fun SIV@276 () (Array Int Int))
(declare-fun SIV@616 () (Array Int Int))
(declare-fun SIV@277 () (Array Int Int))
(declare-fun SIV@617 () (Array Int Int))
(declare-fun SIV@278 () (Array Int Int))
(declare-fun SIV@618 () (Array Int Int))
(declare-fun SIV@279 () (Array Int Int))
(declare-fun SIV@620 () (Array Int Int))
(declare-fun SIV@280 () (Array Int Int))
(declare-fun SIV@621 () (Array Int Int))
(declare-fun SIV@281 () (Array Int Int))
(declare-fun SIV@622 () (Array Int Int))
(declare-fun SIV@282 () (Array Int Int))
(declare-fun SIV@623 () (Array Int Int))
(declare-fun SIV@283 () (Array Int Int))
(declare-fun SIV@624 () (Array Int Int))
(declare-fun SIV@284 () (Array Int Int))
(declare-fun SIV@625 () (Array Int Int))
(declare-fun SIV@285 () (Array Int Int))
(declare-fun SIV@627 () (Array Int Int))
(declare-fun SIV@286 () (Array Int Int))
(declare-fun SIV@628 () (Array Int Int))
(declare-fun SIV@287 () (Array Int Int))
(declare-fun SIV@629 () (Array Int Int))
(declare-fun SIV@288 () (Array Int Int))
(declare-fun SIV@630 () (Array Int Int))
(declare-fun SIV@289 () (Array Int Int))
(declare-fun SIV@631 () (Array Int Int))
(declare-fun SIV@290 () (Array Int Int))
(declare-fun SIV@632 () (Array Int Int))
(declare-fun SIV@291 () (Array Int Int))
(declare-fun SIV@633 () (Array Int Int))
(declare-fun SIV@292 () (Array Int Int))
(declare-fun SIV@634 () (Array Int Int))
(declare-fun SIV@293 () (Array Int Int))
(declare-fun SIV@635 () (Array Int Int))
(declare-fun SIV@294 () (Array Int Int))
(declare-fun SIV@636 () (Array Int Int))
(declare-fun SIV@295 () (Array Int Int))
(declare-fun SIV@637 () (Array Int Int))
(declare-fun SIV@296 () (Array Int Int))
(declare-fun SIV@638 () (Array Int Int))
(declare-fun SIV@297 () (Array Int Int))
(declare-fun SIV@639 () (Array Int Int))
(declare-fun SIV@298 () (Array Int Int))
(declare-fun SIV@640 () (Array Int Int))
(declare-fun SIV@299 () (Array Int Int))
(declare-fun SIV@641 () (Array Int Int))
(declare-fun SIV@300 () (Array Int Int))
(declare-fun SIV@642 () (Array Int Int))
(declare-fun SIV@301 () (Array Int Int))
(declare-fun SIV@643 () (Array Int Int))
(declare-fun SIV@302 () (Array Int Int))
(declare-fun SIV@644 () (Array Int Int))
(declare-fun SIV@303 () (Array Int Int))
(declare-fun SIV@645 () (Array Int Int))
(declare-fun SIV@304 () (Array Int Int))
(declare-fun SIV@646 () (Array Int Int))
(declare-fun SIV@305 () (Array Int Int))
(declare-fun SIV@647 () (Array Int Int))
(declare-fun SIV@306 () (Array Int Int))
(declare-fun SIV@648 () (Array Int Int))
(declare-fun SIV@307 () (Array Int Int))
(declare-fun SIV@649 () (Array Int Int))
(declare-fun SIV@308 () (Array Int Int))
(declare-fun SIV@650 () (Array Int Int))
(declare-fun SIV@309 () (Array Int Int))
(declare-fun SIV@651 () (Array Int Int))
(declare-fun SIV@310 () (Array Int Int))
(declare-fun SIV@652 () (Array Int Int))
(declare-fun SIV@311 () (Array Int Int))
(declare-fun SIV@653 () (Array Int Int))
(declare-fun SIV@312 () (Array Int Int))
(declare-fun SIV@654 () (Array Int Int))
(declare-fun SIV@313 () (Array Int Int))
(declare-fun SIV@655 () (Array Int Int))
(declare-fun SIV@314 () (Array Int Int))
(declare-fun SIV@656 () (Array Int Int))
(declare-fun SIV@315 () (Array Int Int))
(declare-fun SIV@657 () (Array Int Int))
(declare-fun SIV@316 () (Array Int Int))
(declare-fun SIV@658 () (Array Int Int))
(declare-fun SIV@317 () (Array Int Int))
(declare-fun SIV@659 () (Array Int Int))
(declare-fun SIV@318 () (Array Int Int))
(declare-fun SIV@660 () (Array Int Int))
(declare-fun SIV@319 () (Array Int Int))
(declare-fun SIV@661 () (Array Int Int))
(declare-fun SIV@320 () (Array Int Int))
(declare-fun SIV@662 () (Array Int Int))
(declare-fun SIV@321 () (Array Int Int))
(declare-fun SIV@663 () (Array Int Int))
(declare-fun SIV@322 () (Array Int Int))
(declare-fun SIV@664 () (Array Int Int))
(declare-fun SIV@323 () (Array Int Int))
(declare-fun SIV@665 () (Array Int Int))
(declare-fun SIV@324 () (Array Int Int))
(declare-fun SIV@666 () (Array Int Int))
(declare-fun SIV@325 () (Array Int Int))
(declare-fun SIV@667 () (Array Int Int))
(declare-fun SIV@326 () (Array Int Int))
(declare-fun SIV@668 () (Array Int Int))
(declare-fun SIV@327 () (Array Int Int))
(declare-fun SIV@669 () (Array Int Int))
(declare-fun SIV@328 () (Array Int Int))
(declare-fun SIV@670 () (Array Int Int))
(declare-fun SIV@329 () (Array Int Int))
(declare-fun SIV@671 () (Array Int Int))
(declare-fun SIV@330 () (Array Int Int))
(declare-fun SIV@672 () (Array Int Int))
(declare-fun SIV@331 () (Array Int Int))
(declare-fun SIV@673 () (Array Int Int))
(declare-fun SIV@332 () (Array Int Int))
(declare-fun SIV@674 () (Array Int Int))
(declare-fun SIV@333 () (Array Int Int))
(declare-fun SIV@675 () (Array Int Int))
(declare-fun SIV@334 () (Array Int Int))
(declare-fun SIV@676 () (Array Int Int))
(declare-fun SIV@335 () (Array Int Int))
(declare-fun SIV@677 () (Array Int Int))
(declare-fun SIV@336 () (Array Int Int))
(declare-fun SIV@678 () (Array Int Int))
(declare-fun SIV@337 () (Array Int Int))
(declare-fun SIV@679 () (Array Int Int))
(declare-fun SIV@338 () (Array Int Int))
(declare-fun SIV@680 () (Array Int Int))
(declare-fun SIV@339 () (Array Int Int))
(declare-fun SIV@681 () (Array Int Int))
(declare-fun SIV@340 () (Array Int Int))
(declare-fun SIV@682 () (Array Int Int))
(declare-fun SIV@341 () (Array Int Int))
(declare-fun SIV@683 () (Array Int Int))
(declare-fun SIV@342 () (Array Int Int))
(declare-fun SIV@684 () (Array Int Int))
(declare-fun SIV@343 () (Array Int Int))
(declare-fun SIV@685 () (Array Int Int))
(declare-fun SIV@344 () (Array Int Int))
(declare-fun SIV@686 () (Array Int Int))
(declare-fun SIV@345 () (Array Int Int))
(declare-fun SIV@687 () (Array Int Int))
(declare-fun SIV@346 () (Array Int Int))
(declare-fun SIV@688 () (Array Int Int))
(declare-fun SIV@347 () (Array Int Int))
(declare-fun SIV@689 () (Array Int Int))
(declare-fun SIV@348 () (Array Int Int))
(declare-fun SIV@690 () (Array Int Int))
(declare-fun SIV@349 () (Array Int Int))
(declare-fun SIV@692 () (Array Int Int))
(declare-fun SIV@350 () (Array Int Int))
(declare-fun SIV@694 () (Array Int Int))
(declare-fun SIV@351 () (Array Int Int))
(declare-fun SIV@697 () (Array Int Int))
(declare-fun SIV@352 () (Array Int Int))
(declare-fun SIV@698 () (Array Int Int))
(declare-fun SIV@353 () (Array Int Int))
(declare-fun SIV@699 () (Array Int Int))
(declare-fun SIV@354 () (Array Int Int))
(declare-fun SIV@700 () (Array Int Int))
(declare-fun SIV@355 () (Array Int Int))
(declare-fun SIV@701 () (Array Int Int))
(declare-fun SIV@356 () (Array Int Int))
(declare-fun SIV@702 () (Array Int Int))
(declare-fun SIV@357 () (Array Int Int))
(declare-fun SIV@703 () (Array Int Int))
(declare-fun SIV@358 () (Array Int Int))
(declare-fun SIV@704 () (Array Int Int))
(declare-fun SIV@359 () (Array Int Int))
(declare-fun SIV@705 () (Array Int Int))
(declare-fun SIV@360 () (Array Int Int))
(declare-fun SIV@706 () (Array Int Int))
(declare-fun SIV@361 () (Array Int Int))
(declare-fun SIV@707 () (Array Int Int))
(declare-fun SIV@362 () (Array Int Int))
(declare-fun SIV@708 () (Array Int Int))
(declare-fun SIV@363 () (Array Int Int))
(declare-fun SIV@709 () (Array Int Int))
(declare-fun SIV@364 () (Array Int Int))
(declare-fun SIV@710 () (Array Int Int))
(declare-fun SIV@365 () (Array Int Int))
(declare-fun SIV@711 () (Array Int Int))
(declare-fun SIV@366 () (Array Int Int))
(declare-fun SIV@712 () (Array Int Int))
(declare-fun SIV@367 () (Array Int Int))
(declare-fun SIV@713 () (Array Int Int))
(declare-fun SIV@368 () (Array Int Int))
(declare-fun SIV@714 () (Array Int Int))
(declare-fun SIV@369 () (Array Int Int))
(declare-fun SIV@715 () (Array Int Int))
(declare-fun SIV@370 () (Array Int Int))
(declare-fun SIV@716 () (Array Int Int))
(declare-fun SIV@371 () (Array Int Int))
(declare-fun SIV@717 () (Array Int Int))
(declare-fun SIV@372 () (Array Int Int))
(declare-fun SIV@718 () (Array Int Int))
(declare-fun SIV@373 () (Array Int Int))
(declare-fun SIV@719 () (Array Int Int))
(declare-fun SIV@374 () (Array Int Int))
(declare-fun SIV@720 () (Array Int Int))
(declare-fun SIV@375 () (Array Int Int))
(declare-fun SIV@721 () (Array Int Int))
(declare-fun SIV@376 () (Array Int Int))
(declare-fun SIV@722 () (Array Int Int))
(declare-fun SIV@377 () (Array Int Int))
(declare-fun SIV@723 () (Array Int Int))
(declare-fun SIV@378 () (Array Int Int))
(declare-fun SIV@724 () (Array Int Int))
(declare-fun SIV@379 () (Array Int Int))
(declare-fun SIV@725 () (Array Int Int))
(declare-fun SIV@380 () (Array Int Int))
(declare-fun SIV@726 () (Array Int Int))
(declare-fun SIV@381 () (Array Int Int))
(declare-fun SIV@727 () (Array Int Int))
(declare-fun SIV@382 () (Array Int Int))
(declare-fun SIV@728 () (Array Int Int))
(declare-fun SIV@383 () (Array Int Int))
(declare-fun SIV@729 () (Array Int Int))
(declare-fun SIV@384 () (Array Int Int))
(declare-fun SIV@730 () (Array Int Int))
(declare-fun SIV@385 () (Array Int Int))
(declare-fun SIV@731 () (Array Int Int))
(declare-fun SIV@386 () (Array Int Int))
(declare-fun SIV@732 () (Array Int Int))
(declare-fun SIV@387 () (Array Int Int))
(declare-fun SIV@733 () (Array Int Int))
(declare-fun SIV@388 () (Array Int Int))
(declare-fun SIV@734 () (Array Int Int))
(declare-fun SIV@389 () (Array Int Int))
(declare-fun SIV@735 () (Array Int Int))
(declare-fun SIV@390 () (Array Int Int))
(declare-fun SIV@736 () (Array Int Int))
(declare-fun SIV@391 () (Array Int Int))
(declare-fun SIV@737 () (Array Int Int))
(declare-fun SIV@392 () (Array Int Int))
(declare-fun SIV@738 () (Array Int Int))
(declare-fun SIV@393 () (Array Int Int))
(declare-fun SIV@739 () (Array Int Int))
(declare-fun SIV@394 () (Array Int Int))
(declare-fun SIV@740 () (Array Int Int))
(declare-fun SIV@395 () (Array Int Int))
(declare-fun SIV@741 () (Array Int Int))
(declare-fun SIV@396 () (Array Int Int))
(declare-fun SIV@742 () (Array Int Int))
(declare-fun SIV@397 () (Array Int Int))
(declare-fun SIV@743 () (Array Int Int))
(declare-fun SIV@398 () (Array Int Int))
(declare-fun SIV@744 () (Array Int Int))
(declare-fun SIV@399 () (Array Int Int))
(declare-fun SIV@745 () (Array Int Int))
(declare-fun SIV@400 () (Array Int Int))
(declare-fun SIV@747 () (Array Int Int))
(declare-fun SIV@401 () (Array Int Int))
(declare-fun SIV@748 () (Array Int Int))
(declare-fun SIV@402 () (Array Int Int))
(declare-fun SIV@749 () (Array Int Int))
(declare-fun SIV@403 () (Array Int Int))
(declare-fun SIV@750 () (Array Int Int))
(declare-fun SIV@404 () (Array Int Int))
(declare-fun SIV@751 () (Array Int Int))
(declare-fun SIV@405 () (Array Int Int))
(declare-fun SIV@752 () (Array Int Int))
(declare-fun SIV@406 () (Array Int Int))
(declare-fun SIV@753 () (Array Int Int))
(declare-fun SIV@407 () (Array Int Int))
(declare-fun SIV@754 () (Array Int Int))
(declare-fun SIV@408 () (Array Int Int))
(declare-fun SIV@755 () (Array Int Int))
(declare-fun SIV@409 () (Array Int Int))
(declare-fun SIV@756 () (Array Int Int))
(declare-fun SIV@410 () (Array Int Int))
(declare-fun SIV@757 () (Array Int Int))
(declare-fun %lbl%+SI15 () Bool)
(declare-fun %lbl%+SI16 () Bool)
(declare-fun %lbl%+SI13 () Bool)
(declare-fun %lbl%@SI14 () Bool)
(declare-fun %lbl%+SI17 () Bool)
(declare-fun %lbl%+SI19 () Bool)
(declare-fun %lbl%+SI18 () Bool)
(declare-fun %lbl%+SI20 () Bool)
(declare-fun SIV@582 () Int)
(declare-fun SIV@583 () (Array Int Int))
(declare-fun SIV@86 () (Array Int Int))
(declare-fun sdv_devobj_pdo () Int)
(declare-fun sdv_harnessDeviceExtension () Int)
(declare-fun sdv_devobj_fdo () Int)
(declare-fun sdv_harnessDeviceExtension_two () Int)
(declare-fun sdv_irp () Int)
(declare-fun SIV@585 () (Array Int Int))
(declare-fun SIV@77 () (Array Int Int))
(declare-fun sdv_harnessStackLocation () Int)
(declare-fun sdv_other_irp () Int)
(declare-fun sdv_other_harnessStackLocation () Int)
(declare-fun %lbl%+si_fcall_417009 () Bool)
(declare-fun SIV@764 () Bool)
(declare-fun %lbl%+SI22 () Bool)
(declare-fun %lbl%+SI21 () Bool)
(declare-fun %lbl%+SI23 () Bool)
(declare-fun SIV@581 () Int)
(declare-fun %lbl%+SI25 () Bool)
(declare-fun %lbl%+SI24 () Bool)
(declare-fun %lbl%+SI26 () Bool)
(declare-fun SIV@0 () Int)
(declare-fun SIV@455 () Int)
(declare-fun SIV@454 () Int)
(declare-fun WHEA_ERROR_PACKET_SECTION_GUID () Int)
(declare-fun SIV@457 () Int)
(declare-fun SIV@456 () Int)
(declare-fun sdv_harnessStackLocation_next () Int)
(declare-fun SIV@459 () Int)
(declare-fun SIV@458 () Int)
(declare-fun sdv_IoReadPartitionTableEx_DRIVE_LAYOUT_INFORMATION_EX () Int)
(declare-fun SIV@461 () Int)
(declare-fun SIV@460 () Int)
(declare-fun sdv_IoBuildAsynchronousFsdRequest_harnessIrp () Int)
(declare-fun SIV@463 () Int)
(declare-fun SIV@462 () Int)
(declare-fun sdv_IoGetDeviceToVerify_DEVICE_OBJECT () Int)
(declare-fun SIV@465 () Int)
(declare-fun SIV@464 () Int)
(declare-fun sdv_IoBuildDeviceIoControlRequest_harnessStackLocation_next () Int)
(declare-fun SIV@467 () Int)
(declare-fun SIV@466 () Int)
(declare-fun sdv_harness_IoBuildSynchronousFsdRequest_IoStatusBlock () Int)
(declare-fun SIV@469 () Int)
(declare-fun SIV@468 () Int)
(declare-fun sdv_ControllerIrp () Int)
(declare-fun SIV@471 () Int)
(declare-fun SIV@470 () Int)
(declare-fun SIV@473 () Int)
(declare-fun SIV@472 () Int)
(declare-fun sdv_IoGetDmaAdapter_DMA_ADAPTER () Int)
(declare-fun SIV@475 () Int)
(declare-fun SIV@474 () Int)
(declare-fun sdv_IoInitializeIrp_harnessIrp () Int)
(declare-fun SIV@477 () Int)
(declare-fun SIV@476 () Int)
(declare-fun sdv_IoGetRelatedDeviceObject_DEVICE_OBJECT () Int)
(declare-fun SIV@479 () Int)
(declare-fun SIV@478 () Int)
(declare-fun sdv_IoBuildSynchronousFsdRequest_harnessStackLocation_next () Int)
(declare-fun SIV@481 () Int)
(declare-fun SIV@480 () Int)
(declare-fun sdv_IoCreateSynchronizationEvent_KEVENT () Int)
(declare-fun SIV@483 () Int)
(declare-fun SIV@482 () Int)
(declare-fun sdv_other_harnessStackLocation_next () Int)
(declare-fun SIV@485 () Int)
(declare-fun SIV@484 () Int)
(declare-fun SIV@487 () Int)
(declare-fun SIV@486 () Int)
(declare-fun sdv_IoCreateController_CONTROLLER_OBJECT () Int)
(declare-fun SIV@489 () Int)
(declare-fun SIV@488 () Int)
(declare-fun sdv_devobj_top () Int)
(declare-fun SIV@491 () Int)
(declare-fun SIV@490 () Int)
(declare-fun sdv_kdpc_val3 () Int)
(declare-fun SIV@493 () Int)
(declare-fun SIV@492 () Int)
(declare-fun sdv_IoBuildSynchronousFsdRequest_harnessIrp () Int)
(declare-fun SIV@495 () Int)
(declare-fun SIV@494 () Int)
(declare-fun sdv_IoGetDeviceObjectPointer_DEVICE_OBJECT () Int)
(declare-fun SIV@497 () Int)
(declare-fun SIV@496 () Int)
(declare-fun sdv_MapRegisterBase_val () Int)
(declare-fun SIV@499 () Int)
(declare-fun SIV@498 () Int)
(declare-fun sdv_IoGetFileObjectGenericMapping_GENERIC_MAPPING () Int)
(declare-fun SIV@501 () Int)
(declare-fun SIV@500 () Int)
(declare-fun sdv_IoMakeAssociatedIrp_harnessIrp () Int)
(declare-fun SIV@503 () Int)
(declare-fun SIV@502 () Int)
(declare-fun sdv_devobj_child_pdo () Int)
(declare-fun SIV@505 () Int)
(declare-fun SIV@504 () Int)
(declare-fun sdv_harnessIrp () Int)
(declare-fun SIV@507 () Int)
(declare-fun SIV@506 () Int)
(declare-fun sdv_IoBuildAsynchronousFsdRequest_harnessStackLocation_next () Int)
(declare-fun SIV@509 () Int)
(declare-fun SIV@508 () Int)
(declare-fun sdv_harness_IoBuildDeviceIoControlRequest_IoStatusBlock () Int)
(declare-fun SIV@511 () Int)
(declare-fun SIV@510 () Int)
(declare-fun sdv_kinterrupt_val () Int)
(declare-fun SIV@513 () Int)
(declare-fun SIV@512 () Int)
(declare-fun sdv_fx_dev_object () Int)
(declare-fun SIV@515 () Int)
(declare-fun SIV@514 () Int)
(declare-fun SIV@517 () Int)
(declare-fun SIV@516 () Int)
(declare-fun sdv_DpcContext () Int)
(declare-fun SIV@519 () Int)
(declare-fun SIV@518 () Int)
(declare-fun sdv_StartIoIrp () Int)
(declare-fun SIV@521 () Int)
(declare-fun SIV@520 () Int)
(declare-fun sdv_harness_IoBuildAsynchronousFsdRequest_IoStatusBlock () Int)
(declare-fun SIV@523 () Int)
(declare-fun SIV@522 () Int)
(declare-fun sdv_PowerIrp () Int)
(declare-fun SIV@525 () Int)
(declare-fun SIV@524 () Int)
(declare-fun sdv_IoBuildDeviceIoControlRequest_harnessIrp () Int)
(declare-fun SIV@527 () Int)
(declare-fun SIV@526 () Int)
(declare-fun sdv_other_harnessIrp () Int)
(declare-fun SIV@529 () Int)
(declare-fun SIV@528 () Int)
(declare-fun sdv_IoCreateNotificationEvent_KEVENT () Int)
(declare-fun SIV@531 () Int)
(declare-fun SIV@530 () Int)
(declare-fun SIV@533 () Int)
(declare-fun SIV@532 () Int)
(declare-fun sdv_MmMapIoSpace_int () Int)
(declare-fun SIV@535 () Int)
(declare-fun SIV@534 () Int)
(declare-fun SIV@537 () Int)
(declare-fun SIV@536 () Int)
(declare-fun SIV@539 () Int)
(declare-fun SIV@538 () Int)
(declare-fun sdv_pv1 () Int)
(declare-fun SIV@541 () Int)
(declare-fun SIV@540 () Int)
(declare-fun sdv_pv3 () Int)
(declare-fun SIV@543 () Int)
(declare-fun SIV@542 () Int)
(declare-fun sdv_kdpc () Int)
(declare-fun SIV@545 () Int)
(declare-fun SIV@544 () Int)
(declare-fun sdv_pv2 () Int)
(declare-fun SIV@547 () Int)
(declare-fun SIV@546 () Int)
(declare-fun sdv_pIoDpcContext () Int)
(declare-fun SIV@549 () Int)
(declare-fun SIV@548 () Int)
(declare-fun SIV@551 () Int)
(declare-fun SIV@550 () Int)
(declare-fun SIV@553 () Int)
(declare-fun SIV@552 () Int)
(declare-fun igdoe () Int)
(declare-fun SIV@555 () Int)
(declare-fun SIV@554 () Int)
(declare-fun sicrni () Int)
(declare-fun SIV@557 () Int)
(declare-fun SIV@556 () Int)
(declare-fun SIV@558 () Int)
(declare-fun %lbl%+si_fcall_413386 () Bool)
(declare-fun SIV@759 () Bool)
(declare-fun %lbl%+si_fcall_413861 () Bool)
(declare-fun SIV@760 () Bool)
(declare-fun %lbl%+si_fcall_414347 () Bool)
(declare-fun SIV@761 () Bool)
(declare-fun %lbl%+si_fcall_414911 () Bool)
(declare-fun SIV@762 () Bool)
(declare-fun %lbl%+si_fcall_415383 () Bool)
(declare-fun SIV@763 () Bool)
(declare-fun %lbl%+SI27 () Bool)
(declare-fun %lbl%+SI28 () Bool)
(assert  (and (= (ControlFlow 0 0) 403973) (not (let ((GeneratedUnifiedExit_correct  (=> (and %lbl%+SI11 true) (or %lbl%@SI12  (=> (= (ControlFlow 0 403968) (- 0 417500)) (not (and (and (and (and (and (and (and (and (= SIV@235 SIV@765) (= SIV@236 SIV@587)) (= SIV@237 SIV@696)) (and (and (= SIV@238 SIV@559) (= SIV@239 SIV@607)) (= SIV@240 SIV@693))) (and (and (and (= SIV@241 SIV@758) (= SIV@242 SIV@593)) (= SIV@243 SIV@592)) (and (= SIV@244 SIV@591) (= SIV@245 SIV@590)))) (and (and (and (and (= SIV@246 SIV@589) (= SIV@247 SIV@588)) (= SIV@248 SIV@604)) (and (and (= SIV@249 SIV@613) (= SIV@250 SIV@695)) (= SIV@251 SIV@605))) (and (and (and (= SIV@252 SIV@746) (= SIV@253 SIV@598)) (= SIV@254 SIV@584)) (and (= SIV@255 SIV@586) (= SIV@256 SIV@594))))) (and (and (and (and (and (= SIV@257 SIV@595) (= SIV@258 SIV@596)) (= SIV@259 SIV@626)) (and (and (= SIV@260 SIV@691) (= SIV@261 SIV@619)) (= SIV@262 SIV@597))) (and (and (and (= SIV@263 SIV@599) (= SIV@264 SIV@600)) (= SIV@265 SIV@601)) (and (= SIV@266 SIV@602) (= SIV@267 SIV@603)))) (and (and (and (and (= SIV@268 SIV@606) (= SIV@269 SIV@608)) (= SIV@270 SIV@609)) (and (and (= SIV@271 SIV@610) (= SIV@272 SIV@611)) (= SIV@273 SIV@612))) (and (and (and (= SIV@274 SIV@614) (= SIV@275 SIV@615)) (= SIV@276 SIV@616)) (and (= SIV@277 SIV@617) (= SIV@278 SIV@618)))))) (and (and (and (and (and (and (= SIV@279 SIV@620) (= SIV@280 SIV@621)) (= SIV@281 SIV@622)) (and (and (= SIV@282 SIV@623) (= SIV@283 SIV@624)) (= SIV@284 SIV@625))) (and (and (and (= SIV@285 SIV@627) (= SIV@286 SIV@628)) (= SIV@287 SIV@629)) (and (= SIV@288 SIV@630) (= SIV@289 SIV@631)))) (and (and (and (and (= SIV@290 SIV@632) (= SIV@291 SIV@633)) (= SIV@292 SIV@634)) (and (and (= SIV@293 SIV@635) (= SIV@294 SIV@636)) (= SIV@295 SIV@637))) (and (and (and (= SIV@296 SIV@638) (= SIV@297 SIV@639)) (= SIV@298 SIV@640)) (and (= SIV@299 SIV@641) (= SIV@300 SIV@642))))) (and (and (and (and (and (= SIV@301 SIV@643) (= SIV@302 SIV@644)) (= SIV@303 SIV@645)) (and (and (= SIV@304 SIV@646) (= SIV@305 SIV@647)) (= SIV@306 SIV@648))) (and (and (and (= SIV@307 SIV@649) (= SIV@308 SIV@650)) (= SIV@309 SIV@651)) (and (= SIV@310 SIV@652) (= SIV@311 SIV@653)))) (and (and (and (and (= SIV@312 SIV@654) (= SIV@313 SIV@655)) (= SIV@314 SIV@656)) (and (and (= SIV@315 SIV@657) (= SIV@316 SIV@658)) (= SIV@317 SIV@659))) (and (and (and (= SIV@318 SIV@660) (= SIV@319 SIV@661)) (= SIV@320 SIV@662)) (and (= SIV@321 SIV@663) (= SIV@322 SIV@664))))))) (and (and (and (and (and (and (and (= SIV@323 SIV@665) (= SIV@324 SIV@666)) (= SIV@325 SIV@667)) (and (and (= SIV@326 SIV@668) (= SIV@327 SIV@669)) (= SIV@328 SIV@670))) (and (and (and (= SIV@329 SIV@671) (= SIV@330 SIV@672)) (= SIV@331 SIV@673)) (and (= SIV@332 SIV@674) (= SIV@333 SIV@675)))) (and (and (and (and (= SIV@334 SIV@676) (= SIV@335 SIV@677)) (= SIV@336 SIV@678)) (and (and (= SIV@337 SIV@679) (= SIV@338 SIV@680)) (= SIV@339 SIV@681))) (and (and (and (= SIV@340 SIV@682) (= SIV@341 SIV@683)) (= SIV@342 SIV@684)) (and (= SIV@343 SIV@685) (= SIV@344 SIV@686))))) (and (and (and (and (and (= SIV@345 SIV@687) (= SIV@346 SIV@688)) (= SIV@347 SIV@689)) (and (and (= SIV@348 SIV@690) (= SIV@349 SIV@692)) (= SIV@350 SIV@694))) (and (and (and (= SIV@351 SIV@697) (= SIV@352 SIV@698)) (= SIV@353 SIV@699)) (and (= SIV@354 SIV@700) (= SIV@355 SIV@701)))) (and (and (and (and (= SIV@356 SIV@702) (= SIV@357 SIV@703)) (= SIV@358 SIV@704)) (and (and (= SIV@359 SIV@705) (= SIV@360 SIV@706)) (= SIV@361 SIV@707))) (and (and (and (= SIV@362 SIV@708) (= SIV@363 SIV@709)) (= SIV@364 SIV@710)) (and (= SIV@365 SIV@711) (= SIV@366 SIV@712)))))) (and (and (and (and (and (and (= SIV@367 SIV@713) (= SIV@368 SIV@714)) (= SIV@369 SIV@715)) (and (and (= SIV@370 SIV@716) (= SIV@371 SIV@717)) (= SIV@372 SIV@718))) (and (and (and (= SIV@373 SIV@719) (= SIV@374 SIV@720)) (= SIV@375 SIV@721)) (and (= SIV@376 SIV@722) (= SIV@377 SIV@723)))) (and (and (and (and (= SIV@378 SIV@724) (= SIV@379 SIV@725)) (= SIV@380 SIV@726)) (and (and (= SIV@381 SIV@727) (= SIV@382 SIV@728)) (= SIV@383 SIV@729))) (and (and (and (= SIV@384 SIV@730) (= SIV@385 SIV@731)) (= SIV@386 SIV@732)) (and (= SIV@387 SIV@733) (= SIV@388 SIV@734))))) (and (and (and (and (and (= SIV@389 SIV@735) (= SIV@390 SIV@736)) (= SIV@391 SIV@737)) (and (and (= SIV@392 SIV@738) (= SIV@393 SIV@739)) (= SIV@394 SIV@740))) (and (and (and (= SIV@395 SIV@741) (= SIV@396 SIV@742)) (= SIV@397 SIV@743)) (and (= SIV@398 SIV@744) (= SIV@399 SIV@745)))) (and (and (and (and (= SIV@400 SIV@747) (= SIV@401 SIV@748)) (= SIV@402 SIV@749)) (and (and (= SIV@403 SIV@750) (= SIV@404 SIV@751)) (= SIV@405 SIV@752))) (and (and (and (= SIV@406 SIV@753) (= SIV@407 SIV@754)) (= SIV@408 SIV@755)) (and (= SIV@409 SIV@756) (= SIV@410 SIV@757))))))))))))))
(let ((LM2_correct  (=> (and %lbl%+SI15 true) (=> (= (ControlFlow 0 11898) 403968) GeneratedUnifiedExit_correct))))
(let ((anon11_Then_correct  (=> (and %lbl%+SI16 true) (=> (and (= SIV@626 0) (= (ControlFlow 0 11897) 11898)) LM2_correct))))
(let ((anon11_Else_correct  (=> (and %lbl%+SI13 true) (=> (= SIV@626 1) (and (or %lbl%@SI14  (=> (= (ControlFlow 0 11896) (- 0 417498)) false)) (=> (= (ControlFlow 0 11896) 403968) GeneratedUnifiedExit_correct))))))
(let ((L26_correct  (=> (and %lbl%+SI17 true) (and (=> (= (ControlFlow 0 11895) 11897) anon11_Then_correct) (=> (= (ControlFlow 0 11895) 11896) anon11_Else_correct)))))
(let ((anon12_Else_correct  (=> (and %lbl%+SI19 true) (=> (and (= SIV@626 1) (= (ControlFlow 0 11894) 11895)) L26_correct))))
(let ((anon12_Then_correct  (=> (and %lbl%+SI18 true) (=> (and (not (= SIV@626 1)) (= (ControlFlow 0 11899) 11895)) L26_correct))))
(let ((L32_correct  (=> (and %lbl%+SI20 true) (=> (not (= SIV@582 0)) (=> (and (= SIV@583 (store SIV@86 (+ sdv_devobj_pdo 44) sdv_harnessDeviceExtension)) (= SIV@584 (store SIV@583 (+ sdv_devobj_fdo 44) sdv_harnessDeviceExtension_two))) (=> (and (and (and (not (= sdv_irp 0)) (> sdv_irp 0)) (and (= SIV@585 (store SIV@77 (+ (+ (+ sdv_irp 128) 0) 48) sdv_harnessStackLocation)) (not (= sdv_other_irp 0)))) (and (and (> sdv_other_irp 0) (= SIV@586 (store SIV@585 (+ (+ (+ sdv_other_irp 128) 0) 48) sdv_other_harnessStackLocation))) (and (and %lbl%+si_fcall_417009 true) SIV@764))) (and (=> (= (ControlFlow 0 11893) 11899) anon12_Then_correct) (=> (= (ControlFlow 0 11893) 11894) anon12_Else_correct))))))))
(let ((anon10_Else_correct  (=> (and %lbl%+SI22 true) (=> (= sdv_harnessDeviceExtension_two 0) (=> (and (= SIV@582 0) (= (ControlFlow 0 11892) 11893)) L32_correct)))))
(let ((anon10_Then_correct  (=> (and %lbl%+SI21 true) (=> (not (= sdv_harnessDeviceExtension_two 0)) (=> (and (= SIV@582 1) (= (ControlFlow 0 11900) 11893)) L32_correct)))))
(let ((L28_correct  (=> (and %lbl%+SI23 true) (=> (not (= SIV@581 0)) (and (=> (= (ControlFlow 0 11891) 11900) anon10_Then_correct) (=> (= (ControlFlow 0 11891) 11892) anon10_Else_correct))))))
(let ((anon9_Else_correct  (=> (and %lbl%+SI25 true) (=> (= sdv_harnessDeviceExtension 0) (=> (and (= SIV@581 0) (= (ControlFlow 0 11890) 11891)) L28_correct)))))
(let ((anon9_Then_correct  (=> (and %lbl%+SI24 true) (=> (not (= sdv_harnessDeviceExtension 0)) (=> (and (= SIV@581 1) (= (ControlFlow 0 11901) 11891)) L28_correct)))))
(let ((anon0_correct  (=> (and %lbl%+SI26 true) (=> (> SIV@0 0) (=> (and (>= 16 0) (or (= SIV@455 SIV@0) (= SIV@455 0))) (=> (and (and (and (and (and (and (and (and (>= SIV@454 (+ SIV@0 16)) (= SIV@455 WHEA_ERROR_PACKET_SECTION_GUID)) (and (not (= WHEA_ERROR_PACKET_SECTION_GUID 0)) (>= 536 0))) (and (and (or (= SIV@457 SIV@454) (= SIV@457 0)) (>= SIV@456 (+ SIV@454 536))) (and (= SIV@457 sdv_harnessStackLocation_next) (not (= sdv_harnessStackLocation_next 0))))) (and (and (and (>= 76 0) (or (= SIV@459 SIV@456) (= SIV@459 0))) (and (>= SIV@458 (+ SIV@456 76)) (= SIV@459 sdv_IoReadPartitionTableEx_DRIVE_LAYOUT_INFORMATION_EX))) (and (and (not (= sdv_IoReadPartitionTableEx_DRIVE_LAYOUT_INFORMATION_EX 0)) (>= 240 0)) (and (or (= SIV@461 SIV@458) (= SIV@461 0)) (>= SIV@460 (+ SIV@458 240)))))) (and (and (and (and (= SIV@461 sdv_IoBuildAsynchronousFsdRequest_harnessIrp) (not (= sdv_IoBuildAsynchronousFsdRequest_harnessIrp 0))) (and (>= 380 0) (or (= SIV@463 SIV@460) (= SIV@463 0)))) (and (and (>= SIV@462 (+ SIV@460 380)) (= SIV@463 sdv_IoGetDeviceToVerify_DEVICE_OBJECT)) (and (not (= sdv_IoGetDeviceToVerify_DEVICE_OBJECT 0)) (>= 536 0)))) (and (and (and (or (= SIV@465 SIV@462) (= SIV@465 0)) (>= SIV@464 (+ SIV@462 536))) (and (= SIV@465 sdv_IoBuildDeviceIoControlRequest_harnessStackLocation_next) (not (= sdv_IoBuildDeviceIoControlRequest_harnessStackLocation_next 0)))) (and (and (>= 12 0) (or (= SIV@467 SIV@464) (= SIV@467 0))) (and (>= SIV@466 (+ SIV@464 12)) (= SIV@467 sdv_harness_IoBuildSynchronousFsdRequest_IoStatusBlock)))))) (and (and (and (and (and (not (= sdv_harness_IoBuildSynchronousFsdRequest_IoStatusBlock 0)) (>= 240 0)) (and (or (= SIV@469 SIV@466) (= SIV@469 0)) (>= SIV@468 (+ SIV@466 240)))) (and (and (= SIV@469 sdv_ControllerIrp) (not (= sdv_ControllerIrp 0))) (and (>= 380 0) (or (= SIV@471 SIV@468) (= SIV@471 0))))) (and (and (and (>= SIV@470 (+ SIV@468 380)) (= SIV@471 sdv_devobj_pdo)) (and (not (= sdv_devobj_pdo 0)) (>= 12 0))) (and (and (or (= SIV@473 SIV@470) (= SIV@473 0)) (>= SIV@472 (+ SIV@470 12))) (and (= SIV@473 sdv_IoGetDmaAdapter_DMA_ADAPTER) (not (= sdv_IoGetDmaAdapter_DMA_ADAPTER 0)))))) (and (and (and (and (>= 240 0) (or (= SIV@475 SIV@472) (= SIV@475 0))) (and (>= SIV@474 (+ SIV@472 240)) (= SIV@475 sdv_IoInitializeIrp_harnessIrp))) (and (and (not (= sdv_IoInitializeIrp_harnessIrp 0)) (>= 380 0)) (and (or (= SIV@477 SIV@474) (= SIV@477 0)) (>= SIV@476 (+ SIV@474 380))))) (and (and (and (= SIV@477 sdv_IoGetRelatedDeviceObject_DEVICE_OBJECT) (not (= sdv_IoGetRelatedDeviceObject_DEVICE_OBJECT 0))) (and (>= 536 0) (or (= SIV@479 SIV@476) (= SIV@479 0)))) (and (and (>= SIV@478 (+ SIV@476 536)) (= SIV@479 sdv_IoBuildSynchronousFsdRequest_harnessStackLocation_next)) (and (not (= sdv_IoBuildSynchronousFsdRequest_harnessStackLocation_next 0)) (>= 156 0))))))) (and (and (and (and (and (and (or (= SIV@481 SIV@478) (= SIV@481 0)) (>= SIV@480 (+ SIV@478 156))) (and (= SIV@481 sdv_IoCreateSynchronizationEvent_KEVENT) (not (= sdv_IoCreateSynchronizationEvent_KEVENT 0)))) (and (and (>= 536 0) (or (= SIV@483 SIV@480) (= SIV@483 0))) (and (>= SIV@482 (+ SIV@480 536)) (= SIV@483 sdv_other_harnessStackLocation_next)))) (and (and (and (not (= sdv_other_harnessStackLocation_next 0)) (>= 536 0)) (and (or (= SIV@485 SIV@482) (= SIV@485 0)) (>= SIV@484 (+ SIV@482 536)))) (and (and (= SIV@485 sdv_harnessStackLocation) (not (= sdv_harnessStackLocation 0))) (and (>= 60 0) (or (= SIV@487 SIV@484) (= SIV@487 0)))))) (and (and (and (and (>= SIV@486 (+ SIV@484 60)) (= SIV@487 sdv_IoCreateController_CONTROLLER_OBJECT)) (and (not (= sdv_IoCreateController_CONTROLLER_OBJECT 0)) (>= 380 0))) (and (and (or (= SIV@489 SIV@486) (= SIV@489 0)) (>= SIV@488 (+ SIV@486 380))) (and (= SIV@489 sdv_devobj_top) (not (= sdv_devobj_top 0))))) (and (and (and (>= 44 0) (or (= SIV@491 SIV@488) (= SIV@491 0))) (and (>= SIV@490 (+ SIV@488 44)) (= SIV@491 sdv_kdpc_val3))) (and (and (not (= sdv_kdpc_val3 0)) (>= 240 0)) (and (or (= SIV@493 SIV@490) (= SIV@493 0)) (>= SIV@492 (+ SIV@490 240))))))) (and (and (and (and (and (= SIV@493 sdv_IoBuildSynchronousFsdRequest_harnessIrp) (not (= sdv_IoBuildSynchronousFsdRequest_harnessIrp 0))) (and (>= 380 0) (or (= SIV@495 SIV@492) (= SIV@495 0)))) (and (and (>= SIV@494 (+ SIV@492 380)) (= SIV@495 sdv_IoGetDeviceObjectPointer_DEVICE_OBJECT)) (and (not (= sdv_IoGetDeviceObjectPointer_DEVICE_OBJECT 0)) (>= 4 0)))) (and (and (and (or (= SIV@497 SIV@494) (= SIV@497 0)) (>= SIV@496 (+ SIV@494 4))) (and (= SIV@497 sdv_MapRegisterBase_val) (not (= sdv_MapRegisterBase_val 0)))) (and (and (>= 16 0) (or (= SIV@499 SIV@496) (= SIV@499 0))) (and (>= SIV@498 (+ SIV@496 16)) (= SIV@499 sdv_IoGetFileObjectGenericMapping_GENERIC_MAPPING))))) (and (and (and (and (not (= sdv_IoGetFileObjectGenericMapping_GENERIC_MAPPING 0)) (>= 240 0)) (and (or (= SIV@501 SIV@498) (= SIV@501 0)) (>= SIV@500 (+ SIV@498 240)))) (and (and (= SIV@501 sdv_IoMakeAssociatedIrp_harnessIrp) (not (= sdv_IoMakeAssociatedIrp_harnessIrp 0))) (and (>= 380 0) (or (= SIV@503 SIV@500) (= SIV@503 0))))) (and (and (and (>= SIV@502 (+ SIV@500 380)) (= SIV@503 sdv_devobj_child_pdo)) (and (not (= sdv_devobj_child_pdo 0)) (>= 240 0))) (and (and (or (= SIV@505 SIV@502) (= SIV@505 0)) (>= SIV@504 (+ SIV@502 240))) (and (= SIV@505 sdv_harnessIrp) (not (= sdv_harnessIrp 0))))))))) (and (and (and (and (and (and (and (>= 536 0) (or (= SIV@507 SIV@504) (= SIV@507 0))) (and (>= SIV@506 (+ SIV@504 536)) (= SIV@507 sdv_IoBuildAsynchronousFsdRequest_harnessStackLocation_next))) (and (and (not (= sdv_IoBuildAsynchronousFsdRequest_harnessStackLocation_next 0)) (>= 12 0)) (and (or (= SIV@509 SIV@506) (= SIV@509 0)) (>= SIV@508 (+ SIV@506 12))))) (and (and (and (= SIV@509 sdv_harness_IoBuildDeviceIoControlRequest_IoStatusBlock) (not (= sdv_harness_IoBuildDeviceIoControlRequest_IoStatusBlock 0))) (and (>= 0 0) (or (= SIV@511 SIV@508) (= SIV@511 0)))) (and (and (>= SIV@510 (+ SIV@508 0)) (= SIV@511 sdv_kinterrupt_val)) (and (not (= sdv_kinterrupt_val 0)) (>= 40 0))))) (and (and (and (and (or (= SIV@513 SIV@510) (= SIV@513 0)) (>= SIV@512 (+ SIV@510 40))) (and (= SIV@513 sdv_fx_dev_object) (not (= sdv_fx_dev_object 0)))) (and (and (>= 380 0) (or (= SIV@515 SIV@512) (= SIV@515 0))) (and (>= SIV@514 (+ SIV@512 380)) (= SIV@515 sdv_devobj_fdo)))) (and (and (and (not (= sdv_devobj_fdo 0)) (>= 4 0)) (and (or (= SIV@517 SIV@514) (= SIV@517 0)) (>= SIV@516 (+ SIV@514 4)))) (and (and (= SIV@517 sdv_DpcContext) (not (= sdv_DpcContext 0))) (and (>= 240 0) (or (= SIV@519 SIV@516) (= SIV@519 0))))))) (and (and (and (and (and (>= SIV@518 (+ SIV@516 240)) (= SIV@519 sdv_StartIoIrp)) (and (not (= sdv_StartIoIrp 0)) (>= 12 0))) (and (and (or (= SIV@521 SIV@518) (= SIV@521 0)) (>= SIV@520 (+ SIV@518 12))) (and (= SIV@521 sdv_harness_IoBuildAsynchronousFsdRequest_IoStatusBlock) (not (= sdv_harness_IoBuildAsynchronousFsdRequest_IoStatusBlock 0))))) (and (and (and (>= 240 0) (or (= SIV@523 SIV@520) (= SIV@523 0))) (and (>= SIV@522 (+ SIV@520 240)) (= SIV@523 sdv_PowerIrp))) (and (and (not (= sdv_PowerIrp 0)) (>= 240 0)) (and (or (= SIV@525 SIV@522) (= SIV@525 0)) (>= SIV@524 (+ SIV@522 240)))))) (and (and (and (and (= SIV@525 sdv_IoBuildDeviceIoControlRequest_harnessIrp) (not (= sdv_IoBuildDeviceIoControlRequest_harnessIrp 0))) (and (>= 240 0) (or (= SIV@527 SIV@524) (= SIV@527 0)))) (and (and (>= SIV@526 (+ SIV@524 240)) (= SIV@527 sdv_other_harnessIrp)) (and (not (= sdv_other_harnessIrp 0)) (>= 156 0)))) (and (and (and (or (= SIV@529 SIV@526) (= SIV@529 0)) (>= SIV@528 (+ SIV@526 156))) (and (= SIV@529 sdv_IoCreateNotificationEvent_KEVENT) (not (= sdv_IoCreateNotificationEvent_KEVENT 0)))) (and (and (>= 536 0) (or (= SIV@531 SIV@528) (= SIV@531 0))) (and (>= SIV@530 (+ SIV@528 536)) (= SIV@531 sdv_other_harnessStackLocation))))))) (and (and (and (and (and (and (not (= sdv_other_harnessStackLocation 0)) (>= 4 0)) (and (or (= SIV@533 SIV@530) (= SIV@533 0)) (>= SIV@532 (+ SIV@530 4)))) (and (and (= SIV@533 sdv_MmMapIoSpace_int) (not (= sdv_MmMapIoSpace_int 0))) (and (>= 4 0) (or (= SIV@535 SIV@532) (= SIV@535 0))))) (and (and (and (>= SIV@534 (+ SIV@532 4)) (= sdv_harnessDeviceExtension_two SIV@535)) (and (>= 4 0) (or (= SIV@537 SIV@534) (= SIV@537 0)))) (and (and (>= SIV@536 (+ SIV@534 4)) (>= 4 0)) (and (or (= SIV@539 SIV@536) (= SIV@539 0)) (>= SIV@538 (+ SIV@536 4)))))) (and (and (and (and (= sdv_pv1 SIV@539) (>= 4 0)) (and (or (= SIV@541 SIV@538) (= SIV@541 0)) (>= SIV@540 (+ SIV@538 4)))) (and (and (= sdv_pv3 SIV@541) (>= 44 0)) (and (or (= SIV@543 SIV@540) (= SIV@543 0)) (>= SIV@542 (+ SIV@540 44))))) (and (and (and (= sdv_kdpc SIV@543) (>= 4 0)) (and (or (= SIV@545 SIV@542) (= SIV@545 0)) (>= SIV@544 (+ SIV@542 4)))) (and (and (= sdv_pv2 SIV@545) (>= 4 0)) (and (or (= SIV@547 SIV@544) (= SIV@547 0)) (>= SIV@546 (+ SIV@544 4))))))) (and (and (and (and (and (= sdv_pIoDpcContext SIV@547) (>= 4 0)) (and (or (= SIV@549 SIV@546) (= SIV@549 0)) (>= SIV@548 (+ SIV@546 4)))) (and (and (>= 4 0) (or (= SIV@551 SIV@548) (= SIV@551 0))) (and (>= SIV@550 (+ SIV@548 4)) (= sdv_harnessDeviceExtension SIV@551)))) (and (and (and (>= 4 0) (or (= SIV@553 SIV@550) (= SIV@553 0))) (and (>= SIV@552 (+ SIV@550 4)) (= igdoe SIV@553))) (and (and (>= 240 0) (or (= SIV@555 SIV@552) (= SIV@555 0))) (and (>= SIV@554 (+ SIV@552 240)) (= sicrni SIV@555))))) (and (and (and (and (>= 28 0) (or (= SIV@557 SIV@554) (= SIV@557 0))) (and (>= SIV@556 (+ SIV@554 28)) (>= 812 0))) (and (and (= SIV@559 SIV@556) (>= SIV@558 (+ SIV@556 812))) (and (and %lbl%+si_fcall_413386 true) SIV@759))) (and (and (and (and %lbl%+si_fcall_413861 true) SIV@760) (and (and %lbl%+si_fcall_414347 true) SIV@761)) (and (and (and %lbl%+si_fcall_414911 true) SIV@762) (and (and %lbl%+si_fcall_415383 true) SIV@763)))))))) (and (=> (= (ControlFlow 0 11889) 11901) anon9_Then_correct) (=> (= (ControlFlow 0 11889) 11890) anon9_Else_correct))))))))
(let ((q@0_correct  (=> (and %lbl%+SI27 true) (=> (= (ControlFlow 0 403966) 11889) anon0_correct))))
(let ((PreconditionGeneratedEntry_correct  (=> (and %lbl%+SI28 true) (=> (= (ControlFlow 0 403973) 403966) q@0_correct))))
PreconditionGeneratedEntry_correct)))))))))))))))))))

(push 1)
(assert-soft  (not SIV@759) :weight 1)
(assert-soft  (not SIV@760) :weight 1)
(assert-soft  (not SIV@761) :weight 1)
(assert-soft  (not SIV@762) :weight 1)
(assert-soft  (not SIV@763) :weight 1)
(assert-soft  (not SIV@764) :weight 1)

(check-sat)
(get-info :reason-unknown)
(get-model)
(get-info :all-statistics)
NikolajBjorner commented 9 years ago

optimization gives up when the solver returns unknown, which is the case where you have quantifiers (and only using patterns)

zpavlinovic commented 9 years ago

I understand, but should I be able to get a (partial) model? As far as I am familiar, in a purely satisfiability setting, after returning an unknown, some portion of the model can be available.

NikolajBjorner commented 9 years ago

yes, added in 77c8e5b