[     0.002] (INFO) [37mWrite simplified version of 'old' to output_1/old_Main_simplified.st[0m [[33mmodularization.kt:253[0m]
[     0.026] (INFO) [37mMaintain frames in old[0m [[33mmodularization.kt:256[0m]
[     0.439] (INFO) [37mWrite complete SMV file of 'old' to output_1/old_Main_simplified.smv[0m [[33mmodularization.kt:261[0m]
[     0.542] (INFO) [37mWrite simplified version of 'new' to output_1/new_Main_simplified.st[0m [[33mmodularization.kt:253[0m]
[     0.548] (INFO) [37mMaintain frames in new[0m [[33mmodularization.kt:256[0m]
[     0.896] (INFO) [37mWrite complete SMV file of 'new' to output_1/new_Main_simplified.smv[0m [[33mmodularization.kt:261[0m]
[     0.976] (INFO) [37mTop level relation: Sensor_CraneDown = Sensor_CraneDown & Sensor_CraneOnConveyor = Sensor_CraneOnConveyor & Sensor_CraneOnMagazin = Sensor_CraneOnMagazin & Sensor_CranePosition = Sensor_CranePosition & Sensor_CraneSucked = Sensor_CraneSucked & Sensor_CraneUp = Sensor_CraneUp & Sensor_MagazinEmergencyStop = Sensor_MagazinEmergencyStop & Sensor_MagazinSwitchManuellAutomatic = Sensor_MagazinSwitchManuellAutomatic & Sensor_SliderMovedOut = Sensor_SliderMovedOut & Sensor_SliderNotMovedOut = Sensor_SliderNotMovedOut & Sensor_StartButtonMagazin = Sensor_StartButtonMagazin & Sensor_WorkpieceReady = Sensor_WorkpieceReady & Sensor_CranePositionStamp = Sensor_CranePositionStamp & Sensor_CraneSucked = Sensor_CraneSucked & Sensor_CraneUp = Sensor_CraneUp & Sensor_MagazinCapacitiveSensor = Sensor_MagazinCapacitiveSensor & Sensor_MagazinOpticalSensor = Sensor_MagazinOpticalSensor & Sensor_StampEmergencyStop = Sensor_StampEmergencyStop & Sensor_StampLowered = Sensor_StampLowered & Sensor_StampSliderFilled = Sensor_StampSliderFilled & Sensor_StampSliderSensorMovedIn = Sensor_StampSliderSensorMovedIn & Sensor_StampSliderSensorMovedOut = Sensor_StampSliderSensorMovedOut & Sensor_StampStartButton = Sensor_StampStartButton & Sensor_StampSwitchManuellAutomatic = Sensor_StampSwitchManuellAutomatic & Sensor_StampUp = Sensor_StampUp[0m [[33mapp.kt:89[0m]
[     0.976] (INFO) [37mTop level conditon: old.Sensor_MagazinCapacitiveSensor = TRUE[0m [[33mapp.kt:90[0m]
[     0.976] (INFO) [37mProof for perfect equality? false[0m [[33mapp.kt:91[0m]
[     0.976] (INFO) [37mOnly equalities? true[0m [[33mapp.kt:92[0m]
[     0.983] (INFO) [37mCall sites for the old program: Main[0m [[33mmodularization.kt:195[0m]
[     0.983] (INFO) [37mMain.Mag.0 in line @193:8, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.983] (INFO) [37mMain.Crane.0 in line @357:8, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.984] (INFO) [37mMain.Crane.TimeDelay_Timer.0 in line @488:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.984] (INFO) [37mMain.Crane.Timer1.0 in line @674:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.984] (INFO) [37mMain.Crane.Timer1.1 in line @702:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.984] (INFO) [37mMain.Stamp.0 in line @834:8, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.984] (INFO) [37mMain.Stamp.Timer.0 in line @1027:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.984] (INFO) [37mMain.Stamp.Timer.1 in line @1059:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.984] (INFO) [37mCall sites for the new program: Main[0m [[33mmodularization.kt:199[0m]
[     0.984] (INFO) [37mMain.Mag.0 in line @193:8, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.985] (INFO) [37mMain.Crane.0 in line @357:8, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.985] (INFO) [37mMain.Crane.TimeDelay_Timer.0 in line @490:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.985] (INFO) [37mMain.Crane.Timer1.0 in line @679:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.985] (INFO) [37mMain.Crane.Timer1.1 in line @826:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.985] (INFO) [37mMain.Stamp.0 in line @958:8, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.985] (INFO) [37mMain.Stamp.Timer.0 in line @1151:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.986] (INFO) [37mMain.Stamp.Timer.1 in line @1183:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.987] (INFO) [37mMatched Main.Crane.0 to Main.Crane.0[0m [[33mmodularization.kt:206[0m]
[     0.987] (INFO) [37m	Is perfect?: false[0m [[33mmodularization.kt:207[0m]
[     0.987] (INFO) [37m	Context: old.Crane$MagazinCapacitiveSensor = TRUE[0m [[33mmodularization.kt:208[0m]
[     0.989] (INFO) [37m	Input-Relation: old.Crane$CraneDown = new.Crane$CraneDown & old.Crane$CraneOnConveyor = new.Crane$CraneOnConveyor & old.Crane$CraneOnMagazin = new.Crane$CraneOnMagazin & old.Crane$CranePositionStamp = new.Crane$CranePositionStamp & old.Crane$CraneSucked = new.Crane$CraneSucked & old.Crane$CraneUp = new.Crane$CraneUp & old.Crane$MagazinCapacitiveSensor = new.Crane$MagazinCapacitiveSensor & old.Crane$SFCReset = new.Crane$SFCReset & old.Crane$SliderMovedOut = new.Crane$SliderMovedOut & old.Crane$SliderNotMovedOut = new.Crane$SliderNotMovedOut & old.Crane$StampLowered = new.Crane$StampLowered & old.Crane$StampSliderFilled = new.Crane$StampSliderFilled & old.Crane$StartButtonMagazin = new.Crane$StartButtonMagazin & old.Crane$StartVar = new.Crane$StartVar & old.Crane$WorkpieceReady = new.Crane$WorkpieceReady[0m [[33mmodularization.kt:209[0m]
[     0.990] (INFO) [37m	Output-Relation: old.Crane$CraneLower = new.Crane$CraneLower & old.Crane$CraneTurnClockwise = new.Crane$CraneTurnClockwise & old.Crane$CraneTurnCounterclockwise = new.Crane$CraneTurnCounterclockwise & old.Crane$MagazinVacuumOff = new.Crane$MagazinVacuumOff & old.Crane$MagazinVacuumOn = new.Crane$MagazinVacuumOn & old.Crane$StartCommandCrane = new.Crane$StartCommandCrane[0m [[33mmodularization.kt:210[0m]
[     0.990] (INFO) [37mMatched Main.Stamp.0 to Main.Stamp.0[0m [[33mmodularization.kt:206[0m]
[     0.990] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.990] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.991] (INFO) [37m	Input-Relation: old.Stamp$CraneDown = new.Stamp$CraneDown & old.Stamp$CraneOnConveyor = new.Stamp$CraneOnConveyor & old.Stamp$CranePositionStamp = new.Stamp$CranePositionStamp & old.Stamp$CraneSucked = new.Stamp$CraneSucked & old.Stamp$CraneUp = new.Stamp$CraneUp & old.Stamp$SFCReset = new.Stamp$SFCReset & old.Stamp$StampLowered = new.Stamp$StampLowered & old.Stamp$StampSliderFilled = new.Stamp$StampSliderFilled & old.Stamp$StampSliderSensorMovedIn = new.Stamp$StampSliderSensorMovedIn & old.Stamp$StampSliderSensorMovedOut = new.Stamp$StampSliderSensorMovedOut & old.Stamp$StampStartButton = new.Stamp$StampStartButton & old.Stamp$StampUp = new.Stamp$StampUp & old.Stamp$StartVar = new.Stamp$StartVar[0m [[33mmodularization.kt:209[0m]
[     0.992] (INFO) [37m	Output-Relation: old.Stamp$StampGreenLamp = new.Stamp$StampGreenLamp & old.Stamp$StampPressure = new.Stamp$StampPressure & old.Stamp$StampPusher = new.Stamp$StampPusher & old.Stamp$StampSliderMovedIn = new.Stamp$StampSliderMovedIn & old.Stamp$StampSliderMovedOut = new.Stamp$StampSliderMovedOut & old.Stamp$StampWhiteLamp = new.Stamp$StampWhiteLamp & old.Stamp$StartCommandStamp = new.Stamp$StartCommandStamp[0m [[33mmodularization.kt:210[0m]
[     0.992] (INFO) [37mMatched Main.Mag.0 to Main.Mag.0[0m [[33mmodularization.kt:206[0m]
[     0.992] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.992] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.993] (INFO) [37m	Input-Relation: old.Mag$CraneDown = new.Mag$CraneDown & old.Mag$CraneOnConveyor = new.Mag$CraneOnConveyor & old.Mag$CraneOnMagazin = new.Mag$CraneOnMagazin & old.Mag$CraneSucked = new.Mag$CraneSucked & old.Mag$CraneUp = new.Mag$CraneUp & old.Mag$SFCReset = new.Mag$SFCReset & old.Mag$SliderMovedOut = new.Mag$SliderMovedOut & old.Mag$SliderNotMovedOut = new.Mag$SliderNotMovedOut & old.Mag$StartButtonMagazin = new.Mag$StartButtonMagazin & old.Mag$StartVar = new.Mag$StartVar & old.Mag$WorkpieceReady = new.Mag$WorkpieceReady[0m [[33mmodularization.kt:209[0m]
[     0.993] (INFO) [37m	Output-Relation: old.Mag$CraneLower = new.Mag$CraneLower & old.Mag$CraneTurnClockwise = new.Mag$CraneTurnClockwise & old.Mag$CraneTurnCounterclockwise = new.Mag$CraneTurnCounterclockwise & old.Mag$MagazinGreenLamp = new.Mag$MagazinGreenLamp & old.Mag$MagazinSlider = new.Mag$MagazinSlider & old.Mag$MagazinVacuumOff = new.Mag$MagazinVacuumOff & old.Mag$MagazinVacuumOn = new.Mag$MagazinVacuumOn & old.Mag$MagazinWhiteLamp = new.Mag$MagazinWhiteLamp & old.Mag$StartCommandMagazin = new.Mag$StartCommandMagazin[0m [[33mmodularization.kt:210[0m]
[     0.994] (INFO) [37mMatched Main.Stamp.Timer.0 to Main.Stamp.Timer.0[0m [[33mmodularization.kt:206[0m]
[     0.994] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.994] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.995] (INFO) [37m	Input-Relation: old.Stamp$Timer$IN = new.Stamp$Timer$IN & old.Stamp$Timer$PT = new.Stamp$Timer$PT[0m [[33mmodularization.kt:209[0m]
[     0.995] (INFO) [37m	Output-Relation: old.Stamp$Timer$ET = new.Stamp$Timer$ET & old.Stamp$Timer$Q = new.Stamp$Timer$Q[0m [[33mmodularization.kt:210[0m]
[     0.995] (INFO) [37mMatched Main.Crane.Timer1.0 to Main.Crane.Timer1.0[0m [[33mmodularization.kt:206[0m]
[     0.995] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.995] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.995] (INFO) [37m	Input-Relation: old.Crane$Timer1$IN = new.Crane$Timer1$IN & old.Crane$Timer1$PT = new.Crane$Timer1$PT[0m [[33mmodularization.kt:209[0m]
[     0.996] (INFO) [37m	Output-Relation: old.Crane$Timer1$ET = new.Crane$Timer1$ET & old.Crane$Timer1$Q = new.Crane$Timer1$Q[0m [[33mmodularization.kt:210[0m]
[     0.996] (INFO) [37mMatched Main.Crane.TimeDelay_Timer.0 to Main.Crane.TimeDelay_Timer.0[0m [[33mmodularization.kt:206[0m]
[     0.996] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.996] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.996] (INFO) [37m	Input-Relation: old.Crane$TimeDelay_Timer$IN = new.Crane$TimeDelay_Timer$IN & old.Crane$TimeDelay_Timer$PT = new.Crane$TimeDelay_Timer$PT[0m [[33mmodularization.kt:209[0m]
[     0.997] (INFO) [37m	Output-Relation: old.Crane$TimeDelay_Timer$ET = new.Crane$TimeDelay_Timer$ET & old.Crane$TimeDelay_Timer$Q = new.Crane$TimeDelay_Timer$Q[0m [[33mmodularization.kt:210[0m]
[     0.997] (INFO) [37mOutput folder: output_1[0m [[33mapp.kt:118[0m]
[     0.997] (INFO) [37mStart with the proof[0m [[33mapp.kt:119[0m]
[     1.007] (INFO) [37mproofEquivalence(Main,Main):  Main.0: (LoC:759) (Vars: [75] (22) => (30))[0m [[33mstrategy.kt:71[0m]
[     1.013] (INFO) [37mproofEquivalence(Main,Main):  Main.0: (LoC:846) (Vars: [75] (22) => (32))[0m [[33mstrategy.kt:72[0m]
[     1.014] (INFO) [37mcheckCache(Main,Main):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     1.014] (INFO) [37mproofBodyEquivalenceSource(Main,Main):  Frame Main is *not* syntactical equivalent to  Main[0m [[33mstrategy.kt:341[0m]
[     1.015] (INFO) [37mproofBodyEquivalenceSSA(Main,Main):  not suitable for frames Main and Main[0m [[33mstrategy.kt:354[0m]
[     1.015] (INFO) [37mproofBodyEquivalenceSMT(Main,Main):  Proof equivalence of frames Main and Main[0m [[33mstrategy.kt:377[0m]
[     1.015] (INFO) [37mproofBodyEquivalenceSMT(Main,Main):  Translate Main to SMT[0m [[33mstrategy.kt:379[0m]
[     1.077] (INFO) [37mproofBodyEquivalenceSMT(Main,Main):  Translate Main to SMT[0m [[33mstrategy.kt:384[0m]
[     1.116] (INFO) [37mproofBodyEquivalenceSMT(Main,Main):  Create assertion[0m [[33mstrategy.kt:387[0m]
[     1.116] (INFO) [37mproofBodyEquivalenceSMT(Main,Main):  Write SMT problem into output_1/Main_Main_equiv.smt[0m [[33mstrategy.kt:416[0m]
[     1.117] (INFO) [37mproofBodyEquivalenceSMT(Main,Main):  Run z3 for Main_Main_equiv.smt[0m [[33mstrategy.kt:422[0m]
[     1.163] (INFO) [37mproofBodyEquivalenceSMT(Main,Main):  Result of z3 is false for Main_Main_equiv.smt[0m [[33mstrategy.kt:425[0m]
[     1.178] (INFO) [37mproofBodyEquivalenceWithAbstractionBody(Main,Main):  Add new regression verification contract[0m [[33mstrategy.kt:275[0m]
[     1.178] (INFO) [37mFrame Main_abstracted.0 to Main_abstracted.0[0m [[33mstrategy.kt:276[0m]
[     1.178] (INFO) [37m	Context: old.Sensor_MagazinCapacitiveSensor = TRUE[0m [[33mstrategy.kt:277[0m]
[     1.179] (INFO) [37m	Input-Relation: old.Sensor_CraneDown = new.Sensor_CraneDown & old.Sensor_CraneOnConveyor = new.Sensor_CraneOnConveyor & old.Sensor_CraneOnMagazin = new.Sensor_CraneOnMagazin & old.Sensor_CranePosition = new.Sensor_CranePosition & old.Sensor_CraneSucked = new.Sensor_CraneSucked & old.Sensor_CraneUp = new.Sensor_CraneUp & old.Sensor_MagazinEmergencyStop = new.Sensor_MagazinEmergencyStop & old.Sensor_MagazinSwitchManuellAutomatic = new.Sensor_MagazinSwitchManuellAutomatic & old.Sensor_SliderMovedOut = new.Sensor_SliderMovedOut & old.Sensor_SliderNotMovedOut = new.Sensor_SliderNotMovedOut & old.Sensor_StartButtonMagazin = new.Sensor_StartButtonMagazin & old.Sensor_WorkpieceReady = new.Sensor_WorkpieceReady & old.Sensor_CranePositionStamp = new.Sensor_CranePositionStamp & old.Sensor_CraneSucked = new.Sensor_CraneSucked & old.Sensor_CraneUp = new.Sensor_CraneUp & old.Sensor_MagazinCapacitiveSensor = new.Sensor_MagazinCapacitiveSensor & old.Sensor_MagazinOpticalSensor = new.Sensor_MagazinOpticalSensor & old.Sensor_StampEmergencyStop = new.Sensor_StampEmergencyStop & old.Sensor_StampLowered = new.Sensor_StampLowered & old.Sensor_StampSliderFilled = new.Sensor_StampSliderFilled & old.Sensor_StampSliderSensorMovedIn = new.Sensor_StampSliderSensorMovedIn & old.Sensor_StampSliderSensorMovedOut = new.Sensor_StampSliderSensorMovedOut & old.Sensor_StampStartButton = new.Sensor_StampStartButton & old.Sensor_StampSwitchManuellAutomatic = new.Sensor_StampSwitchManuellAutomatic & old.Sensor_StampUp = new.Sensor_StampUp & old.Main$Crane$0$Crane$CraneLower__random = new.Main$Crane$0$Crane$CraneLower__random & old.Main$Crane$0$Crane$CraneTurnClockwise__random = new.Main$Crane$0$Crane$CraneTurnClockwise__random & old.Main$Crane$0$Crane$CraneTurnCounterclockwise__random = new.Main$Crane$0$Crane$CraneTurnCounterclockwise__random & old.Main$Crane$0$Crane$MagazinVacuumOff__random = new.Main$Crane$0$Crane$MagazinVacuumOff__random & old.Main$Crane$0$Crane$MagazinVacuumOn__random = new.Main$Crane$0$Crane$MagazinVacuumOn__random & old.Main$Crane$0$Crane$StartCommandCrane__random = new.Main$Crane$0$Crane$StartCommandCrane__random & old.Main$Stamp$0$Stamp$StampGreenLamp__random = new.Main$Stamp$0$Stamp$StampGreenLamp__random & old.Main$Stamp$0$Stamp$StampPressure__random = new.Main$Stamp$0$Stamp$StampPressure__random & old.Main$Stamp$0$Stamp$StampPusher__random = new.Main$Stamp$0$Stamp$StampPusher__random & old.Main$Stamp$0$Stamp$StampSliderMovedIn__random = new.Main$Stamp$0$Stamp$StampSliderMovedIn__random & old.Main$Stamp$0$Stamp$StampSliderMovedOut__random = new.Main$Stamp$0$Stamp$StampSliderMovedOut__random & old.Main$Stamp$0$Stamp$StampWhiteLamp__random = new.Main$Stamp$0$Stamp$StampWhiteLamp__random & old.Main$Stamp$0$Stamp$StartCommandStamp__random = new.Main$Stamp$0$Stamp$StartCommandStamp__random & old.Main$Mag$0$Mag$CraneLower__random = new.Main$Mag$0$Mag$CraneLower__random & old.Main$Mag$0$Mag$CraneTurnClockwise__random = new.Main$Mag$0$Mag$CraneTurnClockwise__random & old.Main$Mag$0$Mag$CraneTurnCounterclockwise__random = new.Main$Mag$0$Mag$CraneTurnCounterclockwise__random & old.Main$Mag$0$Mag$MagazinGreenLamp__random = new.Main$Mag$0$Mag$MagazinGreenLamp__random & old.Main$Mag$0$Mag$MagazinSlider__random = new.Main$Mag$0$Mag$MagazinSlider__random & old.Main$Mag$0$Mag$MagazinVacuumOff__random = new.Main$Mag$0$Mag$MagazinVacuumOff__random & old.Main$Mag$0$Mag$MagazinVacuumOn__random = new.Main$Mag$0$Mag$MagazinVacuumOn__random & old.Main$Mag$0$Mag$MagazinWhiteLamp__random = new.Main$Mag$0$Mag$MagazinWhiteLamp__random & old.Main$Mag$0$Mag$StartCommandMagazin__random = new.Main$Mag$0$Mag$StartCommandMagazin__random & old.Stamp$Timer$ET = new.Stamp$Timer$ET & old.Stamp$Timer$Q = new.Stamp$Timer$Q & old.Crane$Timer1$ET = new.Crane$Timer1$ET & old.Crane$Timer1$Q = new.Crane$Timer1$Q & old.Crane$TimeDelay_Timer$ET = new.Crane$TimeDelay_Timer$ET & old.Crane$TimeDelay_Timer$Q = new.Crane$TimeDelay_Timer$Q[0m [[33mstrategy.kt:278[0m]
[     1.180] (INFO) [37m	Output-Relation: old.Actuator_CraneLower = new.Actuator_CraneLower & old.Actuator_CraneTurnClockwise = new.Actuator_CraneTurnClockwise & old.Actuator_CraneTurnCounterclockwise = new.Actuator_CraneTurnCounterclockwise & old.Actuator_MagazinGreenLamp = new.Actuator_MagazinGreenLamp & old.Actuator_MagazinSlider = new.Actuator_MagazinSlider & old.Actuator_MagazinVacuumOff = new.Actuator_MagazinVacuumOff & old.Actuator_MagazinVacuumOn = new.Actuator_MagazinVacuumOn & old.Actuator_MagazinWhiteLamp = new.Actuator_MagazinWhiteLamp & old.Actuator_AnalogCranePressure = new.Actuator_AnalogCranePressure & old.Actuator_StampGreenLamp = new.Actuator_StampGreenLamp & old.Actuator_StampPusher = new.Actuator_StampPusher & old.Actuator_StampSliderMovedIn = new.Actuator_StampSliderMovedIn & old.Actuator_StampSliderMovedOut = new.Actuator_StampSliderMovedOut & old.Actuator_StampWhiteLamp = new.Actuator_StampWhiteLamp & old.Main$Crane_ccnt = new.Main$Crane_ccnt & old.Main$Crane$0$Crane$CraneDown__input = new.Main$Crane$0$Crane$CraneDown__input & old.Main$Crane$0$Crane$CraneOnConveyor__input = new.Main$Crane$0$Crane$CraneOnConveyor__input & old.Main$Crane$0$Crane$CraneOnMagazin__input = new.Main$Crane$0$Crane$CraneOnMagazin__input & old.Main$Crane$0$Crane$CranePositionStamp__input = new.Main$Crane$0$Crane$CranePositionStamp__input & old.Main$Crane$0$Crane$CraneSucked__input = new.Main$Crane$0$Crane$CraneSucked__input & old.Main$Crane$0$Crane$CraneUp__input = new.Main$Crane$0$Crane$CraneUp__input & old.Main$Crane$0$Crane$MagazinCapacitiveSensor__input = new.Main$Crane$0$Crane$MagazinCapacitiveSensor__input & old.Main$Crane$0$Crane$SFCReset__input = new.Main$Crane$0$Crane$SFCReset__input & old.Main$Crane$0$Crane$SliderMovedOut__input = new.Main$Crane$0$Crane$SliderMovedOut__input & old.Main$Crane$0$Crane$SliderNotMovedOut__input = new.Main$Crane$0$Crane$SliderNotMovedOut__input & old.Main$Crane$0$Crane$StampLowered__input = new.Main$Crane$0$Crane$StampLowered__input & old.Main$Crane$0$Crane$StampSliderFilled__input = new.Main$Crane$0$Crane$StampSliderFilled__input & old.Main$Crane$0$Crane$StartButtonMagazin__input = new.Main$Crane$0$Crane$StartButtonMagazin__input & old.Main$Crane$0$Crane$StartVar__input = new.Main$Crane$0$Crane$StartVar__input & old.Main$Crane$0$Crane$WorkpieceReady__input = new.Main$Crane$0$Crane$WorkpieceReady__input & old.Main$Stamp_ccnt = new.Main$Stamp_ccnt & old.Main$Stamp$0$Stamp$CraneDown__input = new.Main$Stamp$0$Stamp$CraneDown__input & old.Main$Stamp$0$Stamp$CraneOnConveyor__input = new.Main$Stamp$0$Stamp$CraneOnConveyor__input & old.Main$Stamp$0$Stamp$CranePositionStamp__input = new.Main$Stamp$0$Stamp$CranePositionStamp__input & old.Main$Stamp$0$Stamp$CraneSucked__input = new.Main$Stamp$0$Stamp$CraneSucked__input & old.Main$Stamp$0$Stamp$CraneUp__input = new.Main$Stamp$0$Stamp$CraneUp__input & old.Main$Stamp$0$Stamp$SFCReset__input = new.Main$Stamp$0$Stamp$SFCReset__input & old.Main$Stamp$0$Stamp$StampLowered__input = new.Main$Stamp$0$Stamp$StampLowered__input & old.Main$Stamp$0$Stamp$StampSliderFilled__input = new.Main$Stamp$0$Stamp$StampSliderFilled__input & old.Main$Stamp$0$Stamp$StampSliderSensorMovedIn__input = new.Main$Stamp$0$Stamp$StampSliderSensorMovedIn__input & old.Main$Stamp$0$Stamp$StampSliderSensorMovedOut__input = new.Main$Stamp$0$Stamp$StampSliderSensorMovedOut__input & old.Main$Stamp$0$Stamp$StampStartButton__input = new.Main$Stamp$0$Stamp$StampStartButton__input & old.Main$Stamp$0$Stamp$StampUp__input = new.Main$Stamp$0$Stamp$StampUp__input & old.Main$Stamp$0$Stamp$StartVar__input = new.Main$Stamp$0$Stamp$StartVar__input & old.Main$Mag_ccnt = new.Main$Mag_ccnt & old.Main$Mag$0$Mag$CraneDown__input = new.Main$Mag$0$Mag$CraneDown__input & old.Main$Mag$0$Mag$CraneOnConveyor__input = new.Main$Mag$0$Mag$CraneOnConveyor__input & old.Main$Mag$0$Mag$CraneOnMagazin__input = new.Main$Mag$0$Mag$CraneOnMagazin__input & old.Main$Mag$0$Mag$CraneSucked__input = new.Main$Mag$0$Mag$CraneSucked__input & old.Main$Mag$0$Mag$CraneUp__input = new.Main$Mag$0$Mag$CraneUp__input & old.Main$Mag$0$Mag$SFCReset__input = new.Main$Mag$0$Mag$SFCReset__input & old.Main$Mag$0$Mag$SliderMovedOut__input = new.Main$Mag$0$Mag$SliderMovedOut__input & old.Main$Mag$0$Mag$SliderNotMovedOut__input = new.Main$Mag$0$Mag$SliderNotMovedOut__input & old.Main$Mag$0$Mag$StartButtonMagazin__input = new.Main$Mag$0$Mag$StartButtonMagazin__input & old.Main$Mag$0$Mag$StartVar__input = new.Main$Mag$0$Mag$StartVar__input & old.Main$Mag$0$Mag$WorkpieceReady__input = new.Main$Mag$0$Mag$WorkpieceReady__input & old.Main$Stamp$Timer_ccnt = new.Main$Stamp$Timer_ccnt & old.Stamp$Timer$IN = new.Stamp$Timer$IN & old.Stamp$Timer$PT = new.Stamp$Timer$PT & old.Main$Crane$Timer1_ccnt = new.Main$Crane$Timer1_ccnt & old.Crane$Timer1$IN = new.Crane$Timer1$IN & old.Crane$Timer1$PT = new.Crane$Timer1$PT & old.Main$Crane$TimeDelay_Timer_ccnt = new.Main$Crane$TimeDelay_Timer_ccnt & old.Crane$TimeDelay_Timer$IN = new.Crane$TimeDelay_Timer$IN & old.Crane$TimeDelay_Timer$PT = new.Crane$TimeDelay_Timer$PT[0m [[33mstrategy.kt:279[0m]
[     1.180] (INFO) [37mproofBodyEquivalenceWithAbstractionBody(Main,Main):  Recursion for proofing abstracted body[0m [[33mstrategy.kt:282[0m]
[     1.181] (INFO) [37mproofEquivalence(Main_abstracted,Main_abstracted):  Main_abstracted.0: (LoC:147) (Vars: [75] (22) => (30))[0m [[33mstrategy.kt:71[0m]
[     1.183] (INFO) [37mproofEquivalence(Main_abstracted,Main_abstracted):  Main_abstracted.0: (LoC:147) (Vars: [75] (22) => (32))[0m [[33mstrategy.kt:72[0m]
[     1.183] (INFO) [37mcheckCache(Main_abstracted,Main_abstracted):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     1.183] (INFO) [37mproofBodyEquivalenceSource(Main_abstracted,Main_abstracted):  Frame Main_abstracted is *not* syntactical equivalent to  Main_abstracted[0m [[33mstrategy.kt:341[0m]
[     1.184] (INFO) [37mproofBodyEquivalenceSSA(Main_abstracted,Main_abstracted):  not suitable for frames Main_abstracted and Main_abstracted[0m [[33mstrategy.kt:354[0m]
[     1.184] (INFO) [37mproofBodyEquivalenceSMT(Main_abstracted,Main_abstracted):  Proof equivalence of frames Main_abstracted and Main_abstracted[0m [[33mstrategy.kt:377[0m]
[     1.184] (INFO) [37mproofBodyEquivalenceSMT(Main_abstracted,Main_abstracted):  Translate Main_abstracted to SMT[0m [[33mstrategy.kt:379[0m]
[     1.199] (INFO) [37mproofBodyEquivalenceSMT(Main_abstracted,Main_abstracted):  Translate Main_abstracted to SMT[0m [[33mstrategy.kt:384[0m]
[     1.212] (INFO) [37mproofBodyEquivalenceSMT(Main_abstracted,Main_abstracted):  Create assertion[0m [[33mstrategy.kt:387[0m]
[     1.215] (INFO) [37mproofBodyEquivalenceSMT(Main_abstracted,Main_abstracted):  Write SMT problem into output_1/Main_abstracted_Main_abstracted_equiv.smt[0m [[33mstrategy.kt:416[0m]
[     1.215] (INFO) [37mproofBodyEquivalenceSMT(Main_abstracted,Main_abstracted):  Run z3 for Main_abstracted_Main_abstracted_equiv.smt[0m [[33mstrategy.kt:422[0m]
[     1.243] (INFO) [37mproofBodyEquivalenceSMT(Main_abstracted,Main_abstracted):  Result of z3 is false for Main_abstracted_Main_abstracted_equiv.smt[0m [[33mstrategy.kt:425[0m]
[     1.243] (INFO) [37mproofBodyEquivalenceWithAbstraction(Main_abstracted,Main_abstracted):  declined, recursion protection triggered[0m [[33mstrategy.kt:195[0m]
[     1.252] (INFO) [37mproofBodyEquivalenceClassic(Main_abstracted,Main_abstracted):  Starting proof: output_1/Main_abstracted_Main_abstracted.smv, output_1/Main_abstracted_Main_abstracted.log[0m [[33mstrategy.kt:163[0m]
[     1.262] (INFO) [37mrunNuXmv: Run solver on output_1/Main_abstracted_Main_abstracted.smv[0m [[33mstrategy.kt:486[0m]
[     1.262] (INFO) [37mCreate nuXmv command file `output_1/ic3.xmv'[0m [[33mstrategy.kt:505[0m]
[     1.263] (INFO) [37m/home/weigl/share/nuXmv-1.1.1-Linux/bin/nuXmv -int /home/weigl/work/verifaps-lib/aps-rvt/examples/ppumod/03_05/output_1/Main_abstracted_Main_abstracted.smv[0m [[33mstrategy.kt:819[0m]
[     4.089] (INFO) [37mrunNuXmv: Solver finished for output_1/Main_abstracted_Main_abstracted.smv with edu.kit.iti.formal.smv.NuXMVOutput$Verified@36328d33[0m [[33mstrategy.kt:490[0m]
[     4.089] (INFO) [37mproofBodyEquivalenceClassic(Main_abstracted,Main_abstracted):  Equality proven[0m [[33mstrategy.kt:168[0m]
[     4.089] (INFO) [37mproofEquivalence(Main_abstracted,Main_abstracted):  Timings: {cache=0, cmc=2846, mod=0, smt=59, src=0, ssa=1}[0m [[33mstrategy.kt:96[0m]
[     4.090] (INFO) [37mproofBodyEquivalenceWithAbstractionSubFrames(Main,Main):  Proving sub-frames: Crane=Crane, Stamp=Stamp, Mag=Mag, Timer=Timer, Timer1=Timer1, TimeDelay_Timer=TimeDelay_Timer[0m [[33mstrategy.kt:300[0m]
[     4.092] (INFO) [37mproofEquivalence(Main.Crane,Main.Crane):  Main.Crane.0: (LoC:361) (Vars: [15] (15) => (6))[0m [[33mstrategy.kt:71[0m]
[     4.094] (INFO) [37mproofEquivalence(Main.Crane,Main.Crane):  Main.Crane.0: (LoC:449) (Vars: [16] (15) => (7))[0m [[33mstrategy.kt:72[0m]
[     4.094] (INFO) [37mcheckCache(Main.Crane,Main.Crane):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     4.094] (INFO) [37mproofBodyEquivalenceSource(Main.Crane,Main.Crane):  Frame Main.Crane is *not* syntactical equivalent to  Main.Crane[0m [[33mstrategy.kt:341[0m]
[     4.094] (INFO) [37mproofBodyEquivalenceSSA(Main.Crane,Main.Crane):  not suitable for frames Main.Crane and Main.Crane[0m [[33mstrategy.kt:354[0m]
[     4.094] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane,Main.Crane):  Proof equivalence of frames Main.Crane and Main.Crane[0m [[33mstrategy.kt:377[0m]
[     4.094] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane,Main.Crane):  Translate Main.Crane to SMT[0m [[33mstrategy.kt:379[0m]
[     4.128] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane,Main.Crane):  Translate Main.Crane to SMT[0m [[33mstrategy.kt:384[0m]
[     4.169] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane,Main.Crane):  Create assertion[0m [[33mstrategy.kt:387[0m]
[     4.169] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane,Main.Crane):  Write SMT problem into output_1/Main.Crane_Main.Crane_equiv.smt[0m [[33mstrategy.kt:416[0m]
[     4.169] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane,Main.Crane):  Run z3 for Main.Crane_Main.Crane_equiv.smt[0m [[33mstrategy.kt:422[0m]
[     4.195] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane,Main.Crane):  Result of z3 is false for Main.Crane_Main.Crane_equiv.smt[0m [[33mstrategy.kt:425[0m]
[     4.214] (INFO) [37mproofBodyEquivalenceWithAbstractionBody(Main.Crane,Main.Crane):  Add new regression verification contract[0m [[33mstrategy.kt:275[0m]
[     4.214] (INFO) [37mFrame Main.Crane_abstracted.0 to Main.Crane_abstracted.0[0m [[33mstrategy.kt:276[0m]
[     4.214] (INFO) [37m	Context: old.Crane$MagazinCapacitiveSensor = TRUE[0m [[33mstrategy.kt:277[0m]
[     4.215] (INFO) [37m	Input-Relation: old.Main$Crane_ccnt = new.Main$Crane_ccnt & old.Crane$CraneDown = new.Crane$CraneDown & old.Crane$CraneOnConveyor = new.Crane$CraneOnConveyor & old.Crane$CraneOnMagazin = new.Crane$CraneOnMagazin & old.Crane$CranePositionStamp = new.Crane$CranePositionStamp & old.Crane$CraneSucked = new.Crane$CraneSucked & old.Crane$CraneUp = new.Crane$CraneUp & old.Crane$MagazinCapacitiveSensor = new.Crane$MagazinCapacitiveSensor & old.Crane$SFCReset = new.Crane$SFCReset & old.Crane$SliderMovedOut = new.Crane$SliderMovedOut & old.Crane$SliderNotMovedOut = new.Crane$SliderNotMovedOut & old.Crane$StampLowered = new.Crane$StampLowered & old.Crane$StampSliderFilled = new.Crane$StampSliderFilled & old.Crane$StartButtonMagazin = new.Crane$StartButtonMagazin & old.Crane$StartVar = new.Crane$StartVar & old.Crane$WorkpieceReady = new.Crane$WorkpieceReady & old.Main$Crane$Timer1$1$Crane$Timer1$ET__random = new.Main$Crane$Timer1$1$Crane$Timer1$ET__random & old.Main$Crane$Timer1$1$Crane$Timer1$Q__random = new.Main$Crane$Timer1$1$Crane$Timer1$Q__random & old.Main$Crane$TimeDelay_Timer$0$Crane$TimeDelay_Timer$ET__random = new.Main$Crane$TimeDelay_Timer$0$Crane$TimeDelay_Timer$ET__random & old.Main$Crane$TimeDelay_Timer$0$Crane$TimeDelay_Timer$Q__random = new.Main$Crane$TimeDelay_Timer$0$Crane$TimeDelay_Timer$Q__random[0m [[33mstrategy.kt:278[0m]
[     4.215] (INFO) [37m	Output-Relation: old.Main$Crane_ccnt = new.Main$Crane_ccnt & old.Crane$CraneDown = new.Crane$CraneDown & old.Crane$CraneOnConveyor = new.Crane$CraneOnConveyor & old.Crane$CraneOnMagazin = new.Crane$CraneOnMagazin & old.Crane$CranePositionStamp = new.Crane$CranePositionStamp & old.Crane$CraneSucked = new.Crane$CraneSucked & old.Crane$CraneUp = new.Crane$CraneUp & old.Crane$MagazinCapacitiveSensor = new.Crane$MagazinCapacitiveSensor & old.Crane$SFCReset = new.Crane$SFCReset & old.Crane$SliderMovedOut = new.Crane$SliderMovedOut & old.Crane$SliderNotMovedOut = new.Crane$SliderNotMovedOut & old.Crane$StampLowered = new.Crane$StampLowered & old.Crane$StampSliderFilled = new.Crane$StampSliderFilled & old.Crane$StartButtonMagazin = new.Crane$StartButtonMagazin & old.Crane$StartVar = new.Crane$StartVar & old.Crane$WorkpieceReady = new.Crane$WorkpieceReady & old.Main$Crane$Timer1_ccnt = new.Main$Crane$Timer1_ccnt & old.Main$Crane$Timer1$1$Crane$Timer1$IN__input = new.Main$Crane$Timer1$1$Crane$Timer1$IN__input & old.Main$Crane$Timer1$1$Crane$Timer1$PT__input = new.Main$Crane$Timer1$1$Crane$Timer1$PT__input & old.Main$Crane$TimeDelay_Timer_ccnt = new.Main$Crane$TimeDelay_Timer_ccnt & old.Main$Crane$TimeDelay_Timer$0$Crane$TimeDelay_Timer$IN__input = new.Main$Crane$TimeDelay_Timer$0$Crane$TimeDelay_Timer$IN__input & old.Main$Crane$TimeDelay_Timer$0$Crane$TimeDelay_Timer$PT__input = new.Main$Crane$TimeDelay_Timer$0$Crane$TimeDelay_Timer$PT__input[0m [[33mstrategy.kt:279[0m]
[     4.215] (INFO) [37mproofBodyEquivalenceWithAbstractionBody(Main.Crane,Main.Crane):  Recursion for proofing abstracted body[0m [[33mstrategy.kt:282[0m]
[     4.217] (INFO) [37mproofEquivalence(Main.Crane_abstracted,Main.Crane_abstracted):  Main.Crane_abstracted.0: (LoC:340) (Vars: [15] (15) => (6))[0m [[33mstrategy.kt:71[0m]
[     4.220] (INFO) [37mproofEquivalence(Main.Crane_abstracted,Main.Crane_abstracted):  Main.Crane_abstracted.0: (LoC:428) (Vars: [16] (15) => (7))[0m [[33mstrategy.kt:72[0m]
[     4.220] (INFO) [37mcheckCache(Main.Crane_abstracted,Main.Crane_abstracted):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     4.220] (INFO) [37mproofBodyEquivalenceSource(Main.Crane_abstracted,Main.Crane_abstracted):  Frame Main.Crane_abstracted is *not* syntactical equivalent to  Main.Crane_abstracted[0m [[33mstrategy.kt:341[0m]
[     4.221] (INFO) [37mproofBodyEquivalenceSSA(Main.Crane_abstracted,Main.Crane_abstracted):  not suitable for frames Main.Crane_abstracted and Main.Crane_abstracted[0m [[33mstrategy.kt:354[0m]
[     4.221] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane_abstracted,Main.Crane_abstracted):  Proof equivalence of frames Main.Crane_abstracted and Main.Crane_abstracted[0m [[33mstrategy.kt:377[0m]
[     4.221] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane_abstracted,Main.Crane_abstracted):  Translate Main.Crane_abstracted to SMT[0m [[33mstrategy.kt:379[0m]
[     4.265] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane_abstracted,Main.Crane_abstracted):  Translate Main.Crane_abstracted to SMT[0m [[33mstrategy.kt:384[0m]
[     4.311] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane_abstracted,Main.Crane_abstracted):  Create assertion[0m [[33mstrategy.kt:387[0m]
[     4.311] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane_abstracted,Main.Crane_abstracted):  Write SMT problem into output_1/Main.Crane_abstracted_Main.Crane_abstracted_equiv.smt[0m [[33mstrategy.kt:416[0m]
[     4.312] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane_abstracted,Main.Crane_abstracted):  Run z3 for Main.Crane_abstracted_Main.Crane_abstracted_equiv.smt[0m [[33mstrategy.kt:422[0m]
[     4.336] (INFO) [37mproofBodyEquivalenceSMT(Main.Crane_abstracted,Main.Crane_abstracted):  Result of z3 is false for Main.Crane_abstracted_Main.Crane_abstracted_equiv.smt[0m [[33mstrategy.kt:425[0m]
[     4.336] (INFO) [37mproofBodyEquivalenceWithAbstraction(Main.Crane_abstracted,Main.Crane_abstracted):  declined, recursion protection triggered[0m [[33mstrategy.kt:195[0m]
[     4.353] (INFO) [37mproofBodyEquivalenceClassic(Main.Crane_abstracted,Main.Crane_abstracted):  Starting proof: output_1/Main.Crane_abstracted_Main.Crane_abstracted.smv, output_1/Main.Crane_abstracted_Main.Crane_abstracted.log[0m [[33mstrategy.kt:163[0m]
[     4.378] (INFO) [37mrunNuXmv: Run solver on output_1/Main.Crane_abstracted_Main.Crane_abstracted.smv[0m [[33mstrategy.kt:486[0m]
[     4.379] (INFO) [37m/home/weigl/share/nuXmv-1.1.1-Linux/bin/nuXmv -int /home/weigl/work/verifaps-lib/aps-rvt/examples/ppumod/03_05/output_1/Main.Crane_abstracted_Main.Crane_abstracted.smv[0m [[33mstrategy.kt:819[0m]
[     6.323] (INFO) [37mrunNuXmv: Solver finished for output_1/Main.Crane_abstracted_Main.Crane_abstracted.smv with edu.kit.iti.formal.smv.NuXMVOutput$Verified@36328d33[0m [[33mstrategy.kt:490[0m]
[     6.323] (INFO) [37mproofBodyEquivalenceClassic(Main.Crane_abstracted,Main.Crane_abstracted):  Equality proven[0m [[33mstrategy.kt:168[0m]
[     6.323] (INFO) [37mproofEquivalence(Main.Crane_abstracted,Main.Crane_abstracted):  Timings: {cache=0, cmc=1987, mod=0, smt=115, src=1, ssa=0}[0m [[33mstrategy.kt:96[0m]
[     6.323] (INFO) [37mproofBodyEquivalenceWithAbstractionSubFrames(Main.Crane,Main.Crane):  Proving sub-frames: Timer1=Timer1, TimeDelay_Timer=TimeDelay_Timer[0m [[33mstrategy.kt:300[0m]
[     6.324] (INFO) [37mproofEquivalence(Main.Crane.Timer1,Main.Crane.Timer1):  Main.Crane.Timer1.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:71[0m]
[     6.324] (INFO) [37mproofEquivalence(Main.Crane.Timer1,Main.Crane.Timer1):  Main.Crane.Timer1.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:72[0m]
[     6.324] (INFO) [37mcheckCache(Main.Crane.Timer1,Main.Crane.Timer1):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     6.324] (INFO) [37mproofBodyEquivalenceSource(Main.Crane.Timer1,Main.Crane.Timer1):  Frame Main.Crane.Timer1 is syntactical equivalent to  Main.Crane.Timer1 [0m [[33mstrategy.kt:339[0m]
[     6.324] (INFO) [37mproofEquivalence(Main.Crane.Timer1,Main.Crane.Timer1):  Timings: {cache=0, src=0}[0m [[33mstrategy.kt:96[0m]
[     6.324] (INFO) [37mproofEquivalence(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Main.Crane.TimeDelay_Timer.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:71[0m]
[     6.324] (INFO) [37mproofEquivalence(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Main.Crane.TimeDelay_Timer.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:72[0m]
[     6.324] (INFO) [37mcheckCache(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     6.325] (INFO) [37mproofBodyEquivalenceSource(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Frame Main.Crane.TimeDelay_Timer is syntactical equivalent to  Main.Crane.TimeDelay_Timer [0m [[33mstrategy.kt:339[0m]
[     6.325] (INFO) [37mproofEquivalence(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Timings: {cache=1, src=0}[0m [[33mstrategy.kt:96[0m]
[     6.325] (INFO) [37mproofBodyEquivalenceWithAbstractionSubFrames(Main.Crane,Main.Crane):  proved equality of subframes[0m [[33mstrategy.kt:318[0m]
[     6.325] (INFO) [37mproofBodyEquivalenceWithAbstraction(Main.Crane,Main.Crane):  Equality proven[0m [[33mstrategy.kt:221[0m]
[     6.325] (INFO) [37mproofEquivalence(Main.Crane,Main.Crane):  Timings: {cache=0, mod=2130, smt=101, src=0, ssa=0}[0m [[33mstrategy.kt:96[0m]
[     6.326] (INFO) [37mproofEquivalence(Main.Stamp,Main.Stamp):  Main.Stamp.0: (LoC:201) (Vars: [8] (13) => (7))[0m [[33mstrategy.kt:71[0m]
[     6.326] (INFO) [37mproofEquivalence(Main.Stamp,Main.Stamp):  Main.Stamp.0: (LoC:201) (Vars: [8] (13) => (7))[0m [[33mstrategy.kt:72[0m]
[     6.327] (INFO) [37mcheckCache(Main.Stamp,Main.Stamp):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     6.327] (INFO) [37mproofBodyEquivalenceSource(Main.Stamp,Main.Stamp):  Frame Main.Stamp is *not* syntactical equivalent to  Main.Stamp[0m [[33mstrategy.kt:341[0m]
[     6.371] (INFO) [37mproofBodyEquivalenceSSA(Main.Stamp,Main.Stamp):  Frame Main.Stamp is equivalent to  Main.Stamp in SSA-form [0m [[33mstrategy.kt:365[0m]
[     6.371] (INFO) [37mproofEquivalence(Main.Stamp,Main.Stamp):  Timings: {cache=0, src=0, ssa=44}[0m [[33mstrategy.kt:96[0m]
[     6.372] (INFO) [37mproofEquivalence(Main.Mag,Main.Mag):  Main.Mag.0: (LoC:120) (Vars: [2] (11) => (9))[0m [[33mstrategy.kt:71[0m]
[     6.372] (INFO) [37mproofEquivalence(Main.Mag,Main.Mag):  Main.Mag.0: (LoC:120) (Vars: [2] (11) => (9))[0m [[33mstrategy.kt:72[0m]
[     6.372] (INFO) [37mcheckCache(Main.Mag,Main.Mag):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     6.373] (INFO) [37mproofBodyEquivalenceSource(Main.Mag,Main.Mag):  Frame Main.Mag is syntactical equivalent to  Main.Mag [0m [[33mstrategy.kt:339[0m]
[     6.373] (INFO) [37mproofEquivalence(Main.Mag,Main.Mag):  Timings: {cache=0, src=1}[0m [[33mstrategy.kt:96[0m]
[     6.373] (INFO) [37mproofEquivalence(Main.Stamp.Timer,Main.Stamp.Timer):  Main.Stamp.Timer.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:71[0m]
[     6.373] (INFO) [37mproofEquivalence(Main.Stamp.Timer,Main.Stamp.Timer):  Main.Stamp.Timer.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:72[0m]
[     6.373] (INFO) [37mcheckCache(Main.Stamp.Timer,Main.Stamp.Timer):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     6.374] (INFO) [37mproofBodyEquivalenceSource(Main.Stamp.Timer,Main.Stamp.Timer):  Frame Main.Stamp.Timer is syntactical equivalent to  Main.Stamp.Timer [0m [[33mstrategy.kt:339[0m]
[     6.374] (INFO) [37mproofEquivalence(Main.Stamp.Timer,Main.Stamp.Timer):  Timings: {cache=0, src=1}[0m [[33mstrategy.kt:96[0m]
[     6.374] (INFO) [37mproofEquivalence(Main.Crane.Timer1,Main.Crane.Timer1):  Main.Crane.Timer1.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:71[0m]
[     6.374] (INFO) [37mproofEquivalence(Main.Crane.Timer1,Main.Crane.Timer1):  Main.Crane.Timer1.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:72[0m]
[     6.374] (INFO) [37mcheckCache(Main.Crane.Timer1,Main.Crane.Timer1):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     6.374] (INFO) [37mproofBodyEquivalenceSource(Main.Crane.Timer1,Main.Crane.Timer1):  Frame Main.Crane.Timer1 is syntactical equivalent to  Main.Crane.Timer1 [0m [[33mstrategy.kt:339[0m]
[     6.374] (INFO) [37mproofEquivalence(Main.Crane.Timer1,Main.Crane.Timer1):  Timings: {cache=0, src=0}[0m [[33mstrategy.kt:96[0m]
[     6.375] (INFO) [37mproofEquivalence(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Main.Crane.TimeDelay_Timer.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:71[0m]
[     6.375] (INFO) [37mproofEquivalence(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Main.Crane.TimeDelay_Timer.0: (LoC:13) (Vars: [0] (2) => (2))[0m [[33mstrategy.kt:72[0m]
[     6.375] (INFO) [37mcheckCache(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Cache miss equiv. proof of null with null[0m [[33mstrategy.kt:116[0m]
[     6.375] (INFO) [37mproofBodyEquivalenceSource(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Frame Main.Crane.TimeDelay_Timer is syntactical equivalent to  Main.Crane.TimeDelay_Timer [0m [[33mstrategy.kt:339[0m]
[     6.375] (INFO) [37mproofEquivalence(Main.Crane.TimeDelay_Timer,Main.Crane.TimeDelay_Timer):  Timings: {cache=0, src=0}[0m [[33mstrategy.kt:96[0m]
[     6.376] (INFO) [37mproofBodyEquivalenceWithAbstractionSubFrames(Main,Main):  proved equality of subframes[0m [[33mstrategy.kt:318[0m]
[     6.376] (INFO) [37mproofBodyEquivalenceWithAbstraction(Main,Main):  Equality proven[0m [[33mstrategy.kt:221[0m]
[     6.376] (INFO) [37mproofEquivalence(Main,Main):  Timings: {cache=0, mod=5213, smt=148, src=0, ssa=0}[0m [[33mstrategy.kt:96[0m]
[     6.376] (INFO) [37mProof result: true[0m [[33mmodularization.kt:219[0m]
