diff --git a/regression/ebmc/elbtunnel/elbtunnel.aig.smv b/regression/ebmc/elbtunnel/elbtunnel.aig.smv new file mode 100644 index 000000000..9d8a3c5fd --- /dev/null +++ b/regression/ebmc/elbtunnel/elbtunnel.aig.smv @@ -0,0 +1,806 @@ +MODULE main +VAR +--inputs +AIGER_NEXT_CO_pre_1 : boolean; +AIGER_NEXT_CO_pre_0 : boolean; +AIGER_NEXT_CO_post_1 : boolean; +AIGER_NEXT_CO_post_0 : boolean; +AIGER_NEXT_OHV1_4 : boolean; +AIGER_NEXT_OHV1_3 : boolean; +AIGER_NEXT_OHV1_2 : boolean; +AIGER_NEXT_OHV1_1 : boolean; +AIGER_NEXT_OHV1_0 : boolean; +AIGER_NEXT_OHV2_4 : boolean; +AIGER_NEXT_OHV2_3 : boolean; +AIGER_NEXT_OHV2_2 : boolean; +AIGER_NEXT_OHV2_1 : boolean; +AIGER_NEXT_OHV2_0 : boolean; +H_left_0 : boolean; +H_right_0 : boolean; +H_final_0 : boolean; +AIGER_NEXT_Ti1_2 : boolean; +AIGER_NEXT_Ti1_1 : boolean; +AIGER_NEXT_Ti1_0 : boolean; +AIGER_NEXT_Ti2_2 : boolean; +AIGER_NEXT_Ti2_1 : boolean; +AIGER_NEXT_Ti2_0 : boolean; +AIGER_NEXT_Overtime11_0 : boolean; +AIGER_NEXT_Overtime12_0 : boolean; +AIGER_NEXT_Overtime21_0 : boolean; +AIGER_NEXT_Overtime22_0 : boolean; +AIGER_NEXT_FehldetektionV_0 : boolean; +AIGER_NEXT_FehldetektionN_0 : boolean; +AIGER_NEXT_MisdetektionODMWna_0 : boolean; +AIGER_NEXT_FehldetektionODMWna_0 : boolean; +AIGER_NEXT_H_ODMWna_0 : boolean; +AIGER_NEXT_MisdetektionODleft_0 : boolean; +AIGER_NEXT_FehldetektionODleft_0 : boolean; +AIGER_NEXT_H_ODleft_0 : boolean; +AIGER_NEXT_MisdetektionODright_0 : boolean; +AIGER_NEXT_FehldetektionODright_0 : boolean; +AIGER_NEXT_H_ODright_0 : boolean; +--latches +CO_pre_1 : boolean; +CO_pre_0 : boolean; +CO_post_1 : boolean; +CO_post_0 : boolean; +OHV1_4 : boolean; +OHV1_3 : boolean; +OHV1_2 : boolean; +OHV1_1 : boolean; +OHV1_0 : boolean; +OHV2_4 : boolean; +OHV2_3 : boolean; +OHV2_2 : boolean; +OHV2_1 : boolean; +OHV2_0 : boolean; +Ti1_2 : boolean; +Ti1_1 : boolean; +Ti1_0 : boolean; +Ti2_2 : boolean; +Ti2_1 : boolean; +Ti2_0 : boolean; +Overtime11_0 : boolean; +Overtime12_0 : boolean; +Overtime21_0 : boolean; +Overtime22_0 : boolean; +FehldetektionV_0 : boolean; +FehldetektionN_0 : boolean; +MisdetektionODMWna_0 : boolean; +FehldetektionODMWna_0 : boolean; +H_ODMWna_0 : boolean; +MisdetektionODleft_0 : boolean; +FehldetektionODleft_0 : boolean; +H_ODleft_0 : boolean; +MisdetektionODright_0 : boolean; +FehldetektionODright_0 : boolean; +H_ODright_0 : boolean; +AIGER_VALID : boolean; +AIGER_INITIALIZED : boolean; +ASSIGN +init(CO_pre_1) := FALSE; +next(CO_pre_1) := AIGER_NEXT_CO_pre_1; +init(CO_pre_0) := FALSE; +next(CO_pre_0) := AIGER_NEXT_CO_pre_0; +init(CO_post_1) := FALSE; +next(CO_post_1) := AIGER_NEXT_CO_post_1; +init(CO_post_0) := FALSE; +next(CO_post_0) := AIGER_NEXT_CO_post_0; +init(OHV1_4) := FALSE; +next(OHV1_4) := AIGER_NEXT_OHV1_4; +init(OHV1_3) := FALSE; +next(OHV1_3) := AIGER_NEXT_OHV1_3; +init(OHV1_2) := FALSE; +next(OHV1_2) := AIGER_NEXT_OHV1_2; +init(OHV1_1) := FALSE; +next(OHV1_1) := AIGER_NEXT_OHV1_1; +init(OHV1_0) := FALSE; +next(OHV1_0) := AIGER_NEXT_OHV1_0; +init(OHV2_4) := FALSE; +next(OHV2_4) := AIGER_NEXT_OHV2_4; +init(OHV2_3) := FALSE; +next(OHV2_3) := AIGER_NEXT_OHV2_3; +init(OHV2_2) := FALSE; +next(OHV2_2) := AIGER_NEXT_OHV2_2; +init(OHV2_1) := FALSE; +next(OHV2_1) := AIGER_NEXT_OHV2_1; +init(OHV2_0) := FALSE; +next(OHV2_0) := AIGER_NEXT_OHV2_0; +init(Ti1_2) := FALSE; +next(Ti1_2) := AIGER_NEXT_Ti1_2; +init(Ti1_1) := FALSE; +next(Ti1_1) := AIGER_NEXT_Ti1_1; +init(Ti1_0) := FALSE; +next(Ti1_0) := AIGER_NEXT_Ti1_0; +init(Ti2_2) := FALSE; +next(Ti2_2) := AIGER_NEXT_Ti2_2; +init(Ti2_1) := FALSE; +next(Ti2_1) := AIGER_NEXT_Ti2_1; +init(Ti2_0) := FALSE; +next(Ti2_0) := AIGER_NEXT_Ti2_0; +init(Overtime11_0) := FALSE; +next(Overtime11_0) := AIGER_NEXT_Overtime11_0; +init(Overtime12_0) := FALSE; +next(Overtime12_0) := AIGER_NEXT_Overtime12_0; +init(Overtime21_0) := FALSE; +next(Overtime21_0) := AIGER_NEXT_Overtime21_0; +init(Overtime22_0) := FALSE; +next(Overtime22_0) := AIGER_NEXT_Overtime22_0; +init(FehldetektionV_0) := FALSE; +next(FehldetektionV_0) := AIGER_NEXT_FehldetektionV_0; +init(FehldetektionN_0) := FALSE; +next(FehldetektionN_0) := AIGER_NEXT_FehldetektionN_0; +init(MisdetektionODMWna_0) := FALSE; +next(MisdetektionODMWna_0) := AIGER_NEXT_MisdetektionODMWna_0; +init(FehldetektionODMWna_0) := FALSE; +next(FehldetektionODMWna_0) := AIGER_NEXT_FehldetektionODMWna_0; +init(H_ODMWna_0) := FALSE; +next(H_ODMWna_0) := AIGER_NEXT_H_ODMWna_0; +init(MisdetektionODleft_0) := FALSE; +next(MisdetektionODleft_0) := AIGER_NEXT_MisdetektionODleft_0; +init(FehldetektionODleft_0) := FALSE; +next(FehldetektionODleft_0) := AIGER_NEXT_FehldetektionODleft_0; +init(H_ODleft_0) := FALSE; +next(H_ODleft_0) := AIGER_NEXT_H_ODleft_0; +init(MisdetektionODright_0) := FALSE; +next(MisdetektionODright_0) := AIGER_NEXT_MisdetektionODright_0; +init(FehldetektionODright_0) := FALSE; +next(FehldetektionODright_0) := AIGER_NEXT_FehldetektionODright_0; +init(H_ODright_0) := FALSE; +next(H_ODright_0) := AIGER_NEXT_H_ODright_0; +init(AIGER_VALID) := FALSE; +next(AIGER_VALID) := a1302; +init(AIGER_INITIALIZED) := FALSE; +next(AIGER_INITIALIZED) := TRUE; +DEFINE +--ands +a152 := !AIGER_NEXT_CO_post_0 & !AIGER_NEXT_CO_post_1; +a154 := a152 & !AIGER_NEXT_CO_pre_1; +a156 := a154 & !AIGER_NEXT_CO_pre_0; +a158 := a156 & !AIGER_NEXT_OHV1_4; +a160 := a158 & !AIGER_NEXT_OHV1_3; +a162 := a160 & !AIGER_NEXT_OHV1_2; +a164 := a162 & !AIGER_NEXT_OHV1_1; +a166 := a164 & !AIGER_NEXT_OHV1_0; +a168 := a166 & !AIGER_NEXT_OHV2_4; +a170 := a168 & !AIGER_NEXT_OHV2_3; +a172 := a170 & !AIGER_NEXT_OHV2_2; +a174 := a172 & !AIGER_NEXT_OHV2_1; +a176 := a174 & !AIGER_NEXT_OHV2_0; +a178 := a176 & !AIGER_NEXT_Ti1_1; +a180 := a178 & !AIGER_NEXT_Ti1_0; +a182 := a180 & !AIGER_NEXT_Ti1_2; +a184 := a182 & !AIGER_NEXT_Ti2_1; +a186 := a184 & !AIGER_NEXT_Ti2_0; +a188 := a186 & !AIGER_NEXT_Ti2_2; +a190 := a188 & AIGER_NEXT_Overtime11_0; +a192 := a190 & AIGER_NEXT_Overtime12_0; +a194 := a192 & AIGER_NEXT_Overtime21_0; +a196 := a194 & AIGER_NEXT_Overtime22_0; +a198 := a196 & AIGER_NEXT_FehldetektionV_0; +a200 := a198 & AIGER_NEXT_FehldetektionN_0; +a202 := a200 & AIGER_NEXT_MisdetektionODMWna_0; +a204 := a202 & AIGER_NEXT_FehldetektionODMWna_0; +a206 := a204 & AIGER_NEXT_H_ODMWna_0; +a208 := a206 & AIGER_NEXT_MisdetektionODleft_0; +a210 := a208 & AIGER_NEXT_FehldetektionODleft_0; +a212 := a210 & AIGER_NEXT_H_ODleft_0; +a214 := a212 & AIGER_NEXT_MisdetektionODright_0; +a216 := a214 & AIGER_NEXT_FehldetektionODright_0; +a218 := a216 & AIGER_NEXT_H_ODright_0; +a220 := !a218 & !AIGER_INITIALIZED; +a222 := OHV1_1 & !OHV1_2; +a224 := a222 & !OHV1_3; +a226 := a224 & !OHV1_4; +a228 := !OHV1_1 & OHV1_2; +a230 := a228 & OHV1_3; +a232 := a230 & OHV1_4; +a234 := !a232 & !a226; +a236 := OHV2_1 & !OHV2_2; +a238 := a236 & !OHV2_3; +a240 := a238 & !OHV2_4; +a242 := !a240 & a234; +a244 := !OHV2_1 & OHV2_2; +a246 := a244 & OHV2_3; +a248 := a246 & OHV2_4; +a250 := !a248 & a242; +a252 := a250 & FehldetektionN_0; +a254 := !CO_pre_0 & !CO_pre_1; +a256 := !a254 & !a252; +a258 := !Ti2_0 & !Ti2_1; +a260 := a258 & !Ti2_2; +a262 := Ti2_0 & AIGER_NEXT_Ti2_1; +a264 := !a262 & !Ti2_1; +a266 := !Ti2_0 & AIGER_NEXT_Ti2_0; +a268 := Ti2_0 & !AIGER_NEXT_Ti2_0; +a270 := !a268 & !a266; +a272 := a270 & !AIGER_NEXT_Ti2_1; +a274 := !a272 & Ti2_1; +a276 := !a274 & !a264; +a278 := a276 & AIGER_NEXT_Ti2_2; +a280 := !a278 & !Ti2_2; +a282 := !a272 & !Ti2_1; +a284 := !AIGER_NEXT_Ti2_0 & AIGER_NEXT_Ti2_1; +a286 := !a284 & Ti2_1; +a288 := !a286 & !a282; +a290 := a288 & !AIGER_NEXT_Ti2_2; +a292 := !a290 & Ti2_2; +a294 := !a292 & !a280; +a296 := !a294 & !a260; +a298 := !AIGER_NEXT_Ti2_0 & !AIGER_NEXT_Ti2_1; +a300 := a298 & !AIGER_NEXT_Ti2_2; +a302 := !a300 & a260; +a304 := !a302 & !a296; +a306 := !a304 & !a256; +a308 := AIGER_NEXT_Ti2_0 & AIGER_NEXT_Ti2_1; +a310 := a308 & !AIGER_NEXT_Ti2_2; +a312 := !a310 & a256; +a314 := !a312 & !a306; +a316 := !OHV1_1 & !OHV1_2; +a318 := a316 & !OHV1_3; +a320 := a318 & OHV1_4; +a322 := !OHV2_1 & !OHV2_2; +a324 := a322 & !OHV2_3; +a326 := a324 & OHV2_4; +a328 := !a326 & !a320; +a330 := a328 & FehldetektionV_0; +a332 := !Ti1_0 & !Ti1_1; +a334 := a332 & !Ti1_2; +a336 := Ti1_0 & AIGER_NEXT_Ti1_1; +a338 := !a336 & !Ti1_1; +a340 := !Ti1_0 & AIGER_NEXT_Ti1_0; +a342 := Ti1_0 & !AIGER_NEXT_Ti1_0; +a344 := !a342 & !a340; +a346 := a344 & !AIGER_NEXT_Ti1_1; +a348 := !a346 & Ti1_1; +a350 := !a348 & !a338; +a352 := a350 & AIGER_NEXT_Ti1_2; +a354 := !a352 & !Ti1_2; +a356 := !a346 & !Ti1_1; +a358 := !AIGER_NEXT_Ti1_0 & AIGER_NEXT_Ti1_1; +a360 := !a358 & Ti1_1; +a362 := !a360 & !a356; +a364 := a362 & !AIGER_NEXT_Ti1_2; +a366 := !a364 & Ti1_2; +a368 := !a366 & !a354; +a370 := !a368 & !a334; +a372 := !AIGER_NEXT_Ti1_0 & !AIGER_NEXT_Ti1_1; +a374 := a372 & !AIGER_NEXT_Ti1_2; +a376 := !a374 & a334; +a378 := !a376 & !a370; +a380 := !a378 & a330; +a382 := AIGER_NEXT_Ti1_0 & AIGER_NEXT_Ti1_1; +a384 := a382 & !AIGER_NEXT_Ti1_2; +a386 := !a384 & !a330; +a388 := !a386 & !a380; +a390 := !OHV2_0 & !OHV2_1; +a392 := a390 & !OHV2_2; +a394 := a392 & !OHV2_3; +a396 := a394 & !OHV2_4; +a398 := !OHV2_3 & !OHV2_4; +a400 := !a390 & !OHV2_2; +a402 := OHV2_1 & OHV2_2; +a404 := !a402 & !a400; +a406 := !a404 & a398; +a408 := !a398 & !a322; +a410 := !a408 & !a406; +a412 := a410 & !a396; +a414 := a244 & !OHV2_3; +a416 := a414 & OHV2_4; +a418 := a246 & !OHV2_4; +a420 := a418 & Overtime21_0; +a422 := a418 & !Overtime21_0; +a424 := !a248 & !a240; +a426 := !OHV2_2 & !OHV2_3; +a428 := a426 & !OHV2_4; +a430 := OHV2_0 & !OHV2_1; +a432 := !a430 & a428; +a434 := !a428 & !OHV2_1; +a436 := !a434 & !a432; +a438 := a430 & !OHV2_2; +a440 := !a438 & !a402; +a442 := !a440 & a398; +a444 := a402 & !a398; +a446 := !a444 & !a442; +a448 := a446 & a436; +a450 := a402 & !OHV2_3; +a452 := a450 & !OHV2_4; +a454 := a450 & OHV2_4; +a456 := a454 & Overtime22_0; +a458 := a454 & !Overtime22_0; +a460 := a438 & !OHV2_3; +a462 := a460 & !OHV2_4; +a464 := a402 & OHV2_3; +a466 := a464 & !OHV2_4; +a468 := !AIGER_NEXT_OHV2_0 & !AIGER_NEXT_OHV2_1; +a470 := a468 & !AIGER_NEXT_OHV2_2; +a472 := a470 & !AIGER_NEXT_OHV2_3; +a474 := a472 & !AIGER_NEXT_OHV2_4; +a476 := a464 & OHV2_4; +a478 := a476 & !a474; +a480 := a478 & !a466; +a482 := AIGER_NEXT_OHV2_1 & AIGER_NEXT_OHV2_2; +a484 := a482 & AIGER_NEXT_OHV2_3; +a486 := a484 & AIGER_NEXT_OHV2_4; +a488 := !a486 & a466; +a490 := !a488 & !a480; +a492 := !a490 & !a462; +a494 := !a474 & a462; +a496 := !a494 & !a492; +a498 := !a496 & !a458; +a500 := a482 & !AIGER_NEXT_OHV2_3; +a502 := a500 & AIGER_NEXT_OHV2_4; +a504 := !a502 & a458; +a506 := !a504 & !a498; +a508 := !a506 & !a456; +a510 := AIGER_NEXT_OHV2_0 & !AIGER_NEXT_OHV2_1; +a512 := a510 & !AIGER_NEXT_OHV2_2; +a514 := !a512 & !AIGER_NEXT_OHV2_3; +a516 := !a482 & AIGER_NEXT_OHV2_3; +a518 := !a516 & !a514; +a520 := a518 & !AIGER_NEXT_OHV2_4; +a522 := !a520 & a456; +a524 := !a522 & !a508; +a526 := !a524 & !a452; +a528 := !a502 & a452; +a530 := !a528 & !a526; +a532 := !a530 & !a448; +a534 := !OHV2_0 & !AIGER_NEXT_OHV2_1; +a536 := !OHV2_1 & !AIGER_NEXT_OHV2_2; +a538 := a536 & !a534; +a540 := !a536 & !AIGER_NEXT_OHV2_1; +a542 := !a540 & !a538; +a544 := !a542 & !OHV2_2; +a546 := OHV2_1 & !AIGER_NEXT_OHV2_1; +a548 := !a546 & AIGER_NEXT_OHV2_2; +a550 := !a548 & OHV2_2; +a552 := !a550 & !a544; +a554 := a552 & !AIGER_NEXT_OHV2_3; +a556 := !a554 & !OHV2_3; +a558 := !a482 & !AIGER_NEXT_OHV2_3; +a560 := !OHV2_1 & AIGER_NEXT_OHV2_1; +a562 := !a560 & !a546; +a564 := a562 & !AIGER_NEXT_OHV2_2; +a566 := !a564 & !OHV2_2; +a568 := a562 & AIGER_NEXT_OHV2_2; +a570 := !a568 & OHV2_2; +a572 := !a570 & !a566; +a574 := !a572 & AIGER_NEXT_OHV2_3; +a576 := !a574 & !a558; +a578 := !a576 & OHV2_3; +a580 := !a578 & !a556; +a582 := a580 & AIGER_NEXT_OHV2_4; +a584 := !a582 & !OHV2_4; +a586 := a572 & AIGER_NEXT_OHV2_3; +a588 := !a586 & !OHV2_3; +a590 := !a568 & !OHV2_2; +a592 := !OHV2_1 & !AIGER_NEXT_OHV2_1; +a594 := !a510 & OHV2_1; +a596 := !a594 & !a592; +a598 := a596 & !AIGER_NEXT_OHV2_2; +a600 := !a598 & OHV2_2; +a602 := !a600 & !a590; +a604 := a602 & !AIGER_NEXT_OHV2_3; +a606 := !a604 & OHV2_3; +a608 := !a606 & !a588; +a610 := !a608 & !AIGER_NEXT_OHV2_4; +a612 := !a500 & AIGER_NEXT_OHV2_4; +a614 := !a612 & !a610; +a616 := !a614 & OHV2_4; +a618 := !a616 & !a584; +a620 := !a618 & a448; +a622 := !a620 & !a532; +a624 := !a622 & a424; +a626 := AIGER_NEXT_OHV2_1 & !AIGER_NEXT_OHV2_2; +a628 := a626 & !AIGER_NEXT_OHV2_3; +a630 := a628 & AIGER_NEXT_OHV2_4; +a632 := !a630 & !a424; +a634 := !a632 & !a624; +a636 := !a634 & !a422; +a638 := !AIGER_NEXT_OHV2_1 & AIGER_NEXT_OHV2_2; +a640 := a638 & AIGER_NEXT_OHV2_3; +a642 := a640 & !AIGER_NEXT_OHV2_4; +a644 := !a642 & a422; +a646 := !a644 & !a636; +a648 := !a646 & !a420; +a650 := !a628 & !AIGER_NEXT_OHV2_4; +a652 := !a640 & AIGER_NEXT_OHV2_4; +a654 := !a652 & !a650; +a656 := !a654 & a420; +a658 := !a656 & !a648; +a660 := !a658 & !a416; +a662 := !a642 & a416; +a664 := !a662 & !a660; +a666 := !a664 & !a412; +a668 := !a640 & !AIGER_NEXT_OHV2_4; +a670 := !a534 & !OHV2_1; +a672 := !a670 & !a546; +a674 := a672 & !AIGER_NEXT_OHV2_2; +a676 := !a674 & !OHV2_2; +a678 := !a676 & !a570; +a680 := a678 & !AIGER_NEXT_OHV2_3; +a682 := !a680 & !OHV2_3; +a684 := !a586 & OHV2_3; +a686 := !a684 & !a682; +a688 := !a686 & AIGER_NEXT_OHV2_4; +a690 := !a688 & !a668; +a692 := !a690 & !OHV2_4; +a694 := !a562 & !AIGER_NEXT_OHV2_2; +a696 := !a694 & !a482; +a698 := !a696 & !OHV2_2; +a700 := !a560 & AIGER_NEXT_OHV2_2; +a702 := !a700 & OHV2_2; +a704 := !a702 & !a698; +a706 := a704 & AIGER_NEXT_OHV2_3; +a708 := !a706 & !OHV2_3; +a710 := !a602 & !AIGER_NEXT_OHV2_3; +a712 := !a638 & AIGER_NEXT_OHV2_3; +a714 := !a712 & !a710; +a716 := !a714 & OHV2_3; +a718 := !a716 & !a708; +a720 := a718 & !AIGER_NEXT_OHV2_4; +a722 := !a720 & OHV2_4; +a724 := !a722 & !a692; +a726 := !a724 & a412; +a728 := !a726 & !a666; +a730 := !a728 & !a396; +a732 := !a472 & !AIGER_NEXT_OHV2_4; +a734 := !AIGER_NEXT_OHV2_1 & !AIGER_NEXT_OHV2_2; +a736 := a734 & !AIGER_NEXT_OHV2_3; +a738 := !a736 & AIGER_NEXT_OHV2_4; +a740 := !a738 & !a732; +a742 := !a740 & a396; +a744 := !a742 & !a730; +a746 := !OHV1_0 & !OHV1_1; +a748 := a746 & !OHV1_2; +a750 := a748 & !OHV1_3; +a752 := a750 & !OHV1_4; +a754 := !OHV1_3 & !OHV1_4; +a756 := !a746 & !OHV1_2; +a758 := OHV1_1 & OHV1_2; +a760 := !a758 & !a756; +a762 := !a760 & a754; +a764 := !a754 & !a316; +a766 := !a764 & !a762; +a768 := a766 & !a752; +a770 := a228 & !OHV1_3; +a772 := a770 & OHV1_4; +a774 := a230 & !OHV1_4; +a776 := a774 & Overtime11_0; +a778 := a774 & !Overtime11_0; +a780 := !OHV1_2 & !OHV1_3; +a782 := a780 & !OHV1_4; +a784 := OHV1_0 & !OHV1_1; +a786 := !a784 & a782; +a788 := !a782 & !OHV1_1; +a790 := !a788 & !a786; +a792 := a784 & !OHV1_2; +a794 := !a792 & !a758; +a796 := !a794 & a754; +a798 := a758 & !a754; +a800 := !a798 & !a796; +a802 := a800 & a790; +a804 := a758 & !OHV1_3; +a806 := a804 & !OHV1_4; +a808 := a804 & OHV1_4; +a810 := a808 & Overtime12_0; +a812 := a808 & !Overtime12_0; +a814 := a792 & !OHV1_3; +a816 := a814 & !OHV1_4; +a818 := a758 & OHV1_3; +a820 := a818 & !OHV1_4; +a822 := !AIGER_NEXT_OHV1_0 & !AIGER_NEXT_OHV1_1; +a824 := a822 & !AIGER_NEXT_OHV1_2; +a826 := a824 & !AIGER_NEXT_OHV1_3; +a828 := a826 & !AIGER_NEXT_OHV1_4; +a830 := a818 & OHV1_4; +a832 := a830 & !a828; +a834 := a832 & !a820; +a836 := AIGER_NEXT_OHV1_1 & AIGER_NEXT_OHV1_2; +a838 := a836 & AIGER_NEXT_OHV1_3; +a840 := a838 & AIGER_NEXT_OHV1_4; +a842 := !a840 & a820; +a844 := !a842 & !a834; +a846 := !a844 & !a816; +a848 := !a828 & a816; +a850 := !a848 & !a846; +a852 := !a850 & !a812; +a854 := a836 & !AIGER_NEXT_OHV1_3; +a856 := a854 & AIGER_NEXT_OHV1_4; +a858 := !a856 & a812; +a860 := !a858 & !a852; +a862 := !a860 & !a810; +a864 := AIGER_NEXT_OHV1_0 & !AIGER_NEXT_OHV1_1; +a866 := a864 & !AIGER_NEXT_OHV1_2; +a868 := !a866 & !AIGER_NEXT_OHV1_3; +a870 := !a836 & AIGER_NEXT_OHV1_3; +a872 := !a870 & !a868; +a874 := a872 & !AIGER_NEXT_OHV1_4; +a876 := !a874 & a810; +a878 := !a876 & !a862; +a880 := !a878 & !a806; +a882 := !a856 & a806; +a884 := !a882 & !a880; +a886 := !a884 & !a802; +a888 := !OHV1_0 & !AIGER_NEXT_OHV1_1; +a890 := !OHV1_1 & !AIGER_NEXT_OHV1_2; +a892 := a890 & !a888; +a894 := !a890 & !AIGER_NEXT_OHV1_1; +a896 := !a894 & !a892; +a898 := !a896 & !OHV1_2; +a900 := OHV1_1 & !AIGER_NEXT_OHV1_1; +a902 := !a900 & AIGER_NEXT_OHV1_2; +a904 := !a902 & OHV1_2; +a906 := !a904 & !a898; +a908 := a906 & !AIGER_NEXT_OHV1_3; +a910 := !a908 & !OHV1_3; +a912 := !a836 & !AIGER_NEXT_OHV1_3; +a914 := !OHV1_1 & AIGER_NEXT_OHV1_1; +a916 := !a914 & !a900; +a918 := a916 & !AIGER_NEXT_OHV1_2; +a920 := !a918 & !OHV1_2; +a922 := a916 & AIGER_NEXT_OHV1_2; +a924 := !a922 & OHV1_2; +a926 := !a924 & !a920; +a928 := !a926 & AIGER_NEXT_OHV1_3; +a930 := !a928 & !a912; +a932 := !a930 & OHV1_3; +a934 := !a932 & !a910; +a936 := a934 & AIGER_NEXT_OHV1_4; +a938 := !a936 & !OHV1_4; +a940 := a926 & AIGER_NEXT_OHV1_3; +a942 := !a940 & !OHV1_3; +a944 := !a922 & !OHV1_2; +a946 := !OHV1_1 & !AIGER_NEXT_OHV1_1; +a948 := !a864 & OHV1_1; +a950 := !a948 & !a946; +a952 := a950 & !AIGER_NEXT_OHV1_2; +a954 := !a952 & OHV1_2; +a956 := !a954 & !a944; +a958 := a956 & !AIGER_NEXT_OHV1_3; +a960 := !a958 & OHV1_3; +a962 := !a960 & !a942; +a964 := !a962 & !AIGER_NEXT_OHV1_4; +a966 := !a854 & AIGER_NEXT_OHV1_4; +a968 := !a966 & !a964; +a970 := !a968 & OHV1_4; +a972 := !a970 & !a938; +a974 := !a972 & a802; +a976 := !a974 & !a886; +a978 := !a976 & a234; +a980 := AIGER_NEXT_OHV1_1 & !AIGER_NEXT_OHV1_2; +a982 := a980 & !AIGER_NEXT_OHV1_3; +a984 := a982 & AIGER_NEXT_OHV1_4; +a986 := !a984 & !a234; +a988 := !a986 & !a978; +a990 := !a988 & !a778; +a992 := !AIGER_NEXT_OHV1_1 & AIGER_NEXT_OHV1_2; +a994 := a992 & AIGER_NEXT_OHV1_3; +a996 := a994 & !AIGER_NEXT_OHV1_4; +a998 := !a996 & a778; +a1000 := !a998 & !a990; +a1002 := !a1000 & !a776; +a1004 := !a982 & !AIGER_NEXT_OHV1_4; +a1006 := !a994 & AIGER_NEXT_OHV1_4; +a1008 := !a1006 & !a1004; +a1010 := !a1008 & a776; +a1012 := !a1010 & !a1002; +a1014 := !a1012 & !a772; +a1016 := !a996 & a772; +a1018 := !a1016 & !a1014; +a1020 := !a1018 & !a768; +a1022 := !a994 & !AIGER_NEXT_OHV1_4; +a1024 := !a888 & !OHV1_1; +a1026 := !a1024 & !a900; +a1028 := a1026 & !AIGER_NEXT_OHV1_2; +a1030 := !a1028 & !OHV1_2; +a1032 := !a1030 & !a924; +a1034 := a1032 & !AIGER_NEXT_OHV1_3; +a1036 := !a1034 & !OHV1_3; +a1038 := !a940 & OHV1_3; +a1040 := !a1038 & !a1036; +a1042 := !a1040 & AIGER_NEXT_OHV1_4; +a1044 := !a1042 & !a1022; +a1046 := !a1044 & !OHV1_4; +a1048 := !a916 & !AIGER_NEXT_OHV1_2; +a1050 := !a1048 & !a836; +a1052 := !a1050 & !OHV1_2; +a1054 := !a914 & AIGER_NEXT_OHV1_2; +a1056 := !a1054 & OHV1_2; +a1058 := !a1056 & !a1052; +a1060 := a1058 & AIGER_NEXT_OHV1_3; +a1062 := !a1060 & !OHV1_3; +a1064 := !a956 & !AIGER_NEXT_OHV1_3; +a1066 := !a992 & AIGER_NEXT_OHV1_3; +a1068 := !a1066 & !a1064; +a1070 := !a1068 & OHV1_3; +a1072 := !a1070 & !a1062; +a1074 := a1072 & !AIGER_NEXT_OHV1_4; +a1076 := !a1074 & OHV1_4; +a1078 := !a1076 & !a1046; +a1080 := !a1078 & a768; +a1082 := !a1080 & !a1020; +a1084 := !a1082 & !a752; +a1086 := !a826 & !AIGER_NEXT_OHV1_4; +a1088 := !AIGER_NEXT_OHV1_1 & !AIGER_NEXT_OHV1_2; +a1090 := a1088 & !AIGER_NEXT_OHV1_3; +a1092 := !a1090 & AIGER_NEXT_OHV1_4; +a1094 := !a1092 & !a1086; +a1096 := !a1094 & a752; +a1098 := !a1096 & !a1084; +a1100 := CO_post_0 & !CO_post_1; +a1102 := H_ODMWna_0 & FehldetektionODMWna_0; +a1104 := a1102 & !a820; +a1106 := a1104 & !a466; +a1108 := !a1106 & MisdetektionODMWna_0; +a1110 := a1108 & CO_post_1; +a1112 := !a1110 & !a1100; +a1114 := H_ODright_0 & FehldetektionODright_0; +a1116 := a1114 & !a226; +a1118 := a1116 & !a240; +a1120 := !a1118 & MisdetektionODright_0; +a1122 := H_ODleft_0 & FehldetektionODleft_0; +a1124 := a1122 & !a232; +a1126 := a1124 & !a248; +a1128 := !a1126 & MisdetektionODleft_0; +a1130 := !a1128 & a1120; +a1132 := !a1130 & a256; +a1134 := !a1132 & a1112; +a1136 := a258 & Ti2_2; +a1138 := !CO_post_0 & AIGER_NEXT_CO_post_0; +a1140 := CO_post_0 & !AIGER_NEXT_CO_post_0; +a1142 := !a1140 & !a1138; +a1144 := a1142 & !AIGER_NEXT_CO_post_1; +a1146 := !a1144 & !CO_post_1; +a1148 := CO_post_1 & !AIGER_NEXT_CO_post_1; +a1150 := !a1148 & !a1146; +a1152 := !a1150 & !a1136; +a1154 := a1136 & !a152; +a1156 := !a1154 & !a1152; +a1158 := !a1156 & !a256; +a1160 := a256 & !AIGER_NEXT_CO_post_1; +a1162 := !a1160 & !a1158; +a1164 := !a1162 & a1134; +a1166 := AIGER_NEXT_CO_post_0 & !AIGER_NEXT_CO_post_1; +a1168 := !a1166 & !a1134; +a1170 := !a1168 & !a1164; +a1172 := a332 & Ti1_2; +a1174 := a1172 & !a330; +a1176 := a1172 & a330; +a1178 := !CO_pre_0 & AIGER_NEXT_CO_pre_0; +a1180 := CO_pre_0 & !AIGER_NEXT_CO_pre_0; +a1182 := !a1180 & !a1178; +a1184 := a1182 & !AIGER_NEXT_CO_pre_1; +a1186 := !a1184 & !CO_pre_1; +a1188 := a1182 & AIGER_NEXT_CO_pre_1; +a1190 := !a1188 & CO_pre_1; +a1192 := !a1190 & !a1186; +a1194 := !a1192 & !a256; +a1196 := a1180 & AIGER_NEXT_CO_pre_1; +a1198 := !a1196 & !CO_pre_1; +a1200 := !a1184 & CO_pre_1; +a1202 := !a1200 & !a1198; +a1204 := !a1202 & a256; +a1206 := !a1204 & !a1194; +a1208 := !a1206 & a330; +a1210 := CO_pre_0 & CO_pre_1; +a1212 := !a1210 & !a256; +a1214 := !a1188 & !CO_pre_1; +a1216 := a1178 & !AIGER_NEXT_CO_pre_1; +a1218 := !a1216 & CO_pre_1; +a1220 := !a1218 & !a1214; +a1222 := !a1220 & a1212; +a1224 := !a1212 & !a1192; +a1226 := !a1224 & !a1222; +a1228 := !a1226 & !a330; +a1230 := !a1228 & !a1208; +a1232 := !a1230 & !a1176; +a1234 := !AIGER_NEXT_CO_pre_0 & !AIGER_NEXT_CO_pre_1; +a1236 := !a1234 & a1176; +a1238 := !a1236 & !a1232; +a1240 := !a1238 & !a1174; +a1242 := !AIGER_NEXT_CO_pre_0 & AIGER_NEXT_CO_pre_1; +a1244 := !a1242 & a1174; +a1246 := !a1244 & !a1240; +a1248 := a1246 & a314; +a1250 := a1248 & a1170; +a1252 := a1250 & a1246; +a1254 := a1252 & a1170; +a1256 := a1254 & a1098; +a1258 := a1256 & a388; +a1260 := a1258 & a1098; +a1262 := a1260 & a744; +a1264 := a1262 & a388; +a1266 := a1264 & a314; +a1268 := a1266 & AIGER_NEXT_Overtime11_0; +a1270 := a1268 & AIGER_NEXT_Overtime12_0; +a1272 := a1270 & AIGER_NEXT_Overtime21_0; +a1274 := a1272 & AIGER_NEXT_Overtime22_0; +a1276 := a1274 & AIGER_NEXT_FehldetektionV_0; +a1278 := a1276 & AIGER_NEXT_FehldetektionN_0; +a1280 := a1278 & AIGER_NEXT_MisdetektionODMWna_0; +a1282 := a1280 & AIGER_NEXT_FehldetektionODMWna_0; +a1284 := a1282 & AIGER_NEXT_H_ODMWna_0; +a1286 := a1284 & AIGER_NEXT_MisdetektionODleft_0; +a1288 := a1286 & AIGER_NEXT_FehldetektionODleft_0; +a1290 := a1288 & AIGER_NEXT_H_ODleft_0; +a1292 := a1290 & AIGER_NEXT_MisdetektionODright_0; +a1294 := a1292 & AIGER_NEXT_FehldetektionODright_0; +a1296 := a1294 & AIGER_NEXT_H_ODright_0; +a1298 := a1296 & AIGER_VALID; +a1300 := !a1298 & AIGER_INITIALIZED; +a1302 := !a1300 & !a220; +a1304 := !a1100 & a830; +a1306 := a1304 & AIGER_VALID; +a1308 := a260 & CO_post_1; +a1310 := a1308 & AIGER_VALID; +a1312 := a254 & !a252; +a1314 := a1312 & AIGER_VALID; +a1316 := !a818 & !a814; +a1318 := !a1316 & !OHV1_4; +a1320 := !a1318 & !a830; +a1322 := !a784 & a780; +a1324 := !a780 & !OHV1_1; +a1326 := !a1324 & !a1322; +a1328 := !a1326 & !OHV1_4; +a1330 := !a758 & !OHV1_3; +a1332 := !OHV1_1 & OHV1_3; +a1334 := !a1332 & !a1330; +a1336 := !a1334 & OHV1_4; +a1338 := !a1336 & !a1328; +a1340 := a1338 & a1320; +a1342 := a1340 & a260; +a1344 := a1342 & AIGER_VALID; +a1346 := AIGER_VALID & !Overtime11_0; +a1348 := !a752 & !a320; +a1350 := a780 & !a746; +a1352 := !a780 & OHV1_1; +a1354 := !a1352 & !a1350; +a1356 := !a1354 & !OHV1_4; +a1358 := OHV1_1 & !OHV1_3; +a1360 := !a316 & OHV1_3; +a1362 := !a1360 & !a1358; +a1364 := !a1362 & OHV1_4; +a1366 := !a1364 & !a1356; +a1368 := a1366 & a1348; +a1370 := a1368 & a334; +a1372 := a1370 & AIGER_VALID; +a1374 := a1320 & a790; +a1376 := a1374 & a260; +a1378 := a1376 & AIGER_VALID; +a1380 := CO_post_0 & CO_post_1; +a1382 := a1380 & AIGER_INITIALIZED; +a1384 := OHV1_0 & OHV1_1; +a1386 := a1384 & a782; +a1388 := !a782 & OHV1_0; +a1390 := !a1388 & !a1386; +a1392 := !a1390 & AIGER_INITIALIZED; +a1394 := OHV2_0 & OHV2_1; +a1396 := a1394 & a428; +a1398 := !a428 & OHV2_0; +a1400 := !a1398 & !a1396; +a1402 := !a1400 & AIGER_INITIALIZED; +a1404 := Ti1_0 & Ti1_1; +a1406 := a1404 & Ti1_2; +a1408 := a1406 & AIGER_INITIALIZED; +a1410 := Ti2_0 & Ti2_1; +a1412 := a1410 & Ti2_2; +a1414 := a1412 & AIGER_INITIALIZED; +--outputs +--bad +SPEC AG !a1306 --b7 +SPEC AG !a1310 --b1 +SPEC AG !a1314 --b2 +SPEC AG !a1344 --b3 +SPEC AG !a1346 --b4 +SPEC AG !a1372 --b5 +SPEC AG !a1378 --b6 +SPEC AG !a1306 --b0 +--constraints +INVAR !a1382 --c0 +INVAR !a1392 --c1 +INVAR !a1402 --c2 +INVAR !a1408 --c3 +INVAR !a1414 --c4 +--justice +--fairness diff --git a/regression/ebmc/elbtunnel/test.desc b/regression/ebmc/elbtunnel/test.desc new file mode 100644 index 000000000..35ea48118 --- /dev/null +++ b/regression/ebmc/elbtunnel/test.desc @@ -0,0 +1,15 @@ +CORE +elbtunnel.aig.smv +--bound 12 +^EXIT=10$ +^SIGNAL=0$ +\[smv::main::spec1\] .* FAILURE +\[smv::main::spec2\] .* SUCCESS +\[smv::main::spec3\] .* FAILURE +\[smv::main::spec4\] .* FAILURE +\[smv::main::spec5\] .* SUCCESS +\[smv::main::spec6\] .* SUCCESS +\[smv::main::spec7\] .* FAILURE +\[smv::main::spec8\] .* FAILURE +-- +^warning: ignoring diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp index 3bfd5674a..baa7610f7 100644 --- a/src/ebmc/ebmc_base.cpp +++ b/src/ebmc/ebmc_base.cpp @@ -134,7 +134,8 @@ int ebmc_baset::finish_bmc(prop_conv_solvert &solver) { disjuncts.push_back(literal_exprt(!l)); auto converted_or = solver.convert(disjunction(disjuncts)); - solver.push({literal_exprt{converted_or}}); + solver.push({literal_exprt(converted_or)}); + solver.set_frozen(converted_or); decision_proceduret::resultt dec_result= solver.dec_solve();