The product-lines collection of benchmarks is composed of three groups: elevator: 94 benchmarks minepump: 325 benchmarks email: 178 benchmarks Next, we give details about our experience with each of the tools we have tried: Ultimate, Loopus, HipTNT+, FuncTion, AProVE, ARMC. ================================================================================ 1. Ultimate ================================================================================ Ultimate: -- correctly returns FALSE for all the minepump benchmarks except minepump_spec5_product64_true.cil.c, for which it returns a "PreprocessorHandler: Not yet implemented" error (the corresponding log is shown below) -- returns an "Unsupported Syntax we don't support this cast." error for all the email benchmarks (one such example is given after the log for minepump_spec5_product64_true.cil.c) -- proves terminating 50 of the elevator benchmarks, times out for 43, and returns an "ExceptionOrErrorResult: IllegalStateException: There should be an returnEdge" error for exactly one (elevator_spec14_productSimulator_false.cil.c), for which we show the log further in this document. Next, we provide the logs for the aforementioned special cases. ------------------------------------------------------------------------------- minepump_spec5_product64_true.cil.c benchmark ------------------------------------------------------------------------------- Calling Ultimate with: ./Ultimate ./AutomizerTermination.xml minepump_spec5_product64_true.cil.c --settings ./svComp-64bit-termination-Automizer.epf .......................................................... Execution finished normally Writing output log to file Ultimate.log Result: UNKNOWN 2015-03-22 05:10:26,125 INFO [UltimateCore.java:207]: Initializing application 2015-03-22 05:10:26,127 INFO [UltimateCore.java:224]: -------------------------------------------------------------------------------- 2015-03-22 05:10:26,130 INFO [PluginFactory.java:62]: -------------------------------------------------------------------------------- 2015-03-22 05:10:26,130 INFO [PluginFactory.java:63]: Detecting plugins... 2015-03-22 05:10:26,131 INFO [PluginFactory.java:287]: 1 IController plugins available 2015-03-22 05:10:26,131 INFO [PluginFactory.java:287]: 3 ISource plugins available 2015-03-22 05:10:26,132 INFO [PluginFactory.java:287]: 1 IOutput plugins available 2015-03-22 05:10:26,132 INFO [PluginFactory.java:287]: 8 IGenerator plugins available 2015-03-22 05:10:26,133 INFO [PluginFactory.java:287]: 2 IAnalysis plugins available 2015-03-22 05:10:26,135 INFO [PluginFactory.java:241]: Loaded controller UltimateCore 2015-03-22 05:10:26,136 INFO [PluginFactory.java:70]: Finished detecting plugins! 2015-03-22 05:10:26,136 INFO [PluginFactory.java:71]: Loading services ... 2015-03-22 05:10:26,143 INFO [PluginFactory.java:272]: 1 IServiceFactory services available 2015-03-22 05:10:26,143 INFO [PluginFactory.java:73]: Finished loading services! 2015-03-22 05:10:26,143 INFO [PluginFactory.java:74]: -------------------------------------------------------------------------------- 2015-03-22 05:10:26,144 INFO [SettingsManager.java:38]: Loading settings from ./svComp-64bit-termination-Automizer.epf 2015-03-22 05:10:26,258 INFO [SettingsManager.java:46]: Loading preferences was successful 2015-03-22 05:10:26,258 INFO [UltimateCore.java:82]: Initializing controller ... 2015-03-22 05:10:26,398 INFO [PersistenceAwareModelManager.java:56]: Repository-Root is: /tmp 2015-03-22 05:10:26,643 INFO [ToolchainManager.java:372]: [Toolchain 1]: Parser CDTParser is usable. 2015-03-22 05:10:26,643 INFO [ToolchainManager.java:200]: [Toolchain 1]: Parser successfully initiated... 2015-03-22 05:10:26,643 INFO [PluginFactory.java:178]: -------------------------------------------------------------------------------- 2015-03-22 05:10:26,643 INFO [PluginFactory.java:179]: Loading all admissible plugins (creating one instance, loading preferences) 2015-03-22 05:10:26,681 INFO [PluginFactory.java:196]: Finished loading 14 admissible plugins (all were admissible) 2015-03-22 05:10:26,681 INFO [PluginFactory.java:198]: -------------------------------------------------------------------------------- 2015-03-22 05:10:26,683 INFO [ToolchainManager.java:180]: [Toolchain 1]: Toolchain data selected. 2015-03-22 05:10:26,684 INFO [PluginConnector.java:249]: Initializing CDTParser... 2015-03-22 05:10:26,684 INFO [PluginConnector.java:254]: CDTParser initialized 2015-03-22 05:10:26,688 INFO [ToolchainManager.java:327]: [Toolchain 1]: Parsing single file: /users/schram/svndeltacheck/branches/termination/regression/svcomp-product-lines/minepump_spec5_product64_true.cil.c 2015-03-22 05:10:26,897 INFO [ToolchainManager.java:219]: ####################### [Toolchain 1] ####################### 2015-03-22 05:10:26,902 INFO [ToolchainWalker.java:61]: Walking toolchain with 5 elements. 2015-03-22 05:10:26,902 INFO [PluginConnector.java:90]: ------------------------CACSL2BoogieTranslator---------------------------- 2015-03-22 05:10:26,903 INFO [PluginConnector.java:249]: Initializing CACSL2BoogieTranslator... 2015-03-22 05:10:26,907 INFO [PluginConnector.java:254]: CACSL2BoogieTranslator initialized 2015-03-22 05:10:26,908 INFO [PluginConnector.java:159]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 22.03 05:10:26" (1/1) ... 2015-03-22 05:10:26,913 INFO [CACSL2BoogieTranslatorObserver.java:85]: Settings: SV_COMP14 2015-03-22 05:10:27,011 WARN [Dispatcher.java:240]: PreprocessorHandler: Not yet implemented: #if 1 2015-03-22 05:10:27,012 WARN [Dispatcher.java:240]: PreprocessorHandler: Not yet implemented: #endif 2015-03-22 05:10:27,013 WARN [Dispatcher.java:240]: PreprocessorHandler: Not yet implemented: #if 1 2015-03-22 05:10:27,013 WARN [Dispatcher.java:240]: PreprocessorHandler: Not yet implemented: #endif 2015-03-22 05:10:27,036 INFO [PostProcessor.java:360]: Settings: Checked method=main 2015-03-22 05:10:27,044 INFO [PluginConnector.java:109]: ------------------------ END CACSL2BoogieTranslator---------------------------- 2015-03-22 05:10:27,044 INFO [ToolchainWalker.java:68]: Toolchain execution was canceled (Timeout or user) 2015-03-22 05:10:27,048 INFO [ResultNotifier.java:103]: RESULT: Ultimate could not prove your program: Toolchain returned no Result. RESULT: Ultimate could not prove your program: Toolchain returned no Result. 2015-03-22 05:10:27,048 INFO [ToolchainManager.java:258]: ####################### End [Toolchain 1] ####################### 2015-03-22 05:10:27,048 INFO [BasicToolchainJob.java:73]: --- Results --- 2015-03-22 05:10:27,049 INFO [BasicToolchainJob.java:75]: * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator: 2015-03-22 05:10:27,049 INFO [BasicToolchainJob.java:89]: - UnsupportedSyntaxResult [Line: 1034]: Unsupported Syntax 2015-03-22 05:10:27,049 INFO [BasicToolchainJob.java:95]: PreprocessorHandler: Not yet implemented: #if 1 2015-03-22 05:10:27,049 INFO [BasicToolchainJob.java:89]: - UnsupportedSyntaxResult [Line: 1111]: Unsupported Syntax 2015-03-22 05:10:27,049 INFO [BasicToolchainJob.java:95]: PreprocessorHandler: Not yet implemented: #endif 2015-03-22 05:10:27,049 INFO [BasicToolchainJob.java:89]: - UnsupportedSyntaxResult [Line: 1116]: Unsupported Syntax 2015-03-22 05:10:27,050 INFO [BasicToolchainJob.java:95]: PreprocessorHandler: Not yet implemented: #if 1 2015-03-22 05:10:27,050 INFO [BasicToolchainJob.java:89]: - UnsupportedSyntaxResult [Line: 1198]: Unsupported Syntax 2015-03-22 05:10:27,050 INFO [BasicToolchainJob.java:95]: PreprocessorHandler: Not yet implemented: #endif 2015-03-22 05:10:27,050 INFO [UltimateCore.java:90]: Preparing to exit Ultimate with return code 0 Closed successfully ------------------------------------------------------------------------------- an email benchmark: all the email benchmarks return the same type of error ------------------------------------------------------------------------------- Checking for termination Rev 12950 Calling Ultimate with: ./Ultimate ./AutomizerTermination.xml email_spec8_product35_false.cil.c --settings ./svComp-64bit-termination-Automizer.epf ................................................. Execution finished normally Writing output log to file Ultimate.log Result: UNKNOWN 2015-03-22 04:35:08,597 INFO [UltimateCore.java:207]: Initializing application 2015-03-22 04:35:08,599 INFO [UltimateCore.java:224]: -------------------------------------------------------------------------------- 2015-03-22 04:35:08,602 INFO [PluginFactory.java:62]: -------------------------------------------------------------------------------- 2015-03-22 04:35:08,602 INFO [PluginFactory.java:63]: Detecting plugins... 2015-03-22 04:35:08,603 INFO [PluginFactory.java:287]: 1 IController plugins available 2015-03-22 04:35:08,603 INFO [PluginFactory.java:287]: 3 ISource plugins available 2015-03-22 04:35:08,604 INFO [PluginFactory.java:287]: 1 IOutput plugins available 2015-03-22 04:35:08,604 INFO [PluginFactory.java:287]: 8 IGenerator plugins available 2015-03-22 04:35:08,605 INFO [PluginFactory.java:287]: 2 IAnalysis plugins available 2015-03-22 04:35:08,608 INFO [PluginFactory.java:241]: Loaded controller UltimateCore 2015-03-22 04:35:08,608 INFO [PluginFactory.java:70]: Finished detecting plugins! 2015-03-22 04:35:08,608 INFO [PluginFactory.java:71]: Loading services ... 2015-03-22 04:35:08,615 INFO [PluginFactory.java:272]: 1 IServiceFactory services available 2015-03-22 04:35:08,615 INFO [PluginFactory.java:73]: Finished loading services! 2015-03-22 04:35:08,615 INFO [PluginFactory.java:74]: -------------------------------------------------------------------------------- 2015-03-22 04:35:08,616 INFO [SettingsManager.java:38]: Loading settings from ./svComp-64bit-termination-Automizer.epf 2015-03-22 04:35:08,728 INFO [SettingsManager.java:46]: Loading preferences was successful 2015-03-22 04:35:08,729 INFO [UltimateCore.java:82]: Initializing controller ... 2015-03-22 04:35:08,869 INFO [PersistenceAwareModelManager.java:56]: Repository-Root is: /tmp 2015-03-22 04:35:09,109 INFO [ToolchainManager.java:372]: [Toolchain 1]: Parser CDTParser is usable. 2015-03-22 04:35:09,109 INFO [ToolchainManager.java:200]: [Toolchain 1]: Parser successfully initiated... 2015-03-22 04:35:09,110 INFO [PluginFactory.java:178]: -------------------------------------------------------------------------------- 2015-03-22 04:35:09,110 INFO [PluginFactory.java:179]: Loading all admissible plugins (creating one instance, loading preferences) 2015-03-22 04:35:09,148 INFO [PluginFactory.java:196]: Finished loading 14 admissible plugins (all were admissible) 2015-03-22 04:35:09,148 INFO [PluginFactory.java:198]: -------------------------------------------------------------------------------- 2015-03-22 04:35:09,150 INFO [ToolchainManager.java:180]: [Toolchain 1]: Toolchain data selected. 2015-03-22 04:35:09,151 INFO [PluginConnector.java:249]: Initializing CDTParser... 2015-03-22 04:35:09,151 INFO [PluginConnector.java:254]: CDTParser initialized 2015-03-22 04:35:09,155 INFO [ToolchainManager.java:327]: [Toolchain 1]: Parsing single file: /users/schram/svndeltacheck/branches/termination/regression/svcomp-product-lines/email_spec8_product35_false.cil.c 2015-03-22 04:35:09,451 INFO [ToolchainManager.java:219]: ####################### [Toolchain 1] ####################### 2015-03-22 04:35:09,455 INFO [ToolchainWalker.java:61]: Walking toolchain with 5 elements. 2015-03-22 04:35:09,456 INFO [PluginConnector.java:90]: ------------------------CACSL2BoogieTranslator---------------------------- 2015-03-22 04:35:09,456 INFO [PluginConnector.java:249]: Initializing CACSL2BoogieTranslator... 2015-03-22 04:35:09,460 INFO [PluginConnector.java:254]: CACSL2BoogieTranslator initialized 2015-03-22 04:35:09,461 INFO [PluginConnector.java:159]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 22.03 04:35:09" (1/1) ... 2015-03-22 04:35:09,466 INFO [CACSL2BoogieTranslatorObserver.java:85]: Settings: SV_COMP14 2015-03-22 04:35:09,663 WARN [CACSL2BoogieTranslatorObserver.java:149]: Unsupported Syntax we don't support this cast. 2015-03-22 04:35:09,663 WARN [PluginConnector.java:178]: CACSL2BoogieTranslator did return invalid model for observer de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.CACSL2BoogieTranslatorObserver@7b55d5d0, skipping insertion in model container 2015-03-22 04:35:09,663 INFO [PluginConnector.java:109]: ------------------------ END CACSL2BoogieTranslator---------------------------- 2015-03-22 04:35:09,664 INFO [ToolchainWalker.java:68]: Toolchain execution was canceled (Timeout or user) 2015-03-22 04:35:09,668 INFO [ResultNotifier.java:103]: RESULT: Ultimate could not prove your program: Toolchain returned no Result. RESULT: Ultimate could not prove your program: Toolchain returned no Result. 2015-03-22 04:35:09,668 INFO [ToolchainManager.java:258]: ####################### End [Toolchain 1] ####################### 2015-03-22 04:35:09,668 INFO [BasicToolchainJob.java:73]: --- Results --- 2015-03-22 04:35:09,669 INFO [BasicToolchainJob.java:75]: * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator: 2015-03-22 04:35:09,669 INFO [BasicToolchainJob.java:89]: - UnsupportedSyntaxResult [Line: 563]: Unsupported Syntax 2015-03-22 04:35:09,669 INFO [BasicToolchainJob.java:95]: we don't support this cast. 2015-03-22 04:35:09,670 INFO [UltimateCore.java:90]: Preparing to exit Ultimate with return code 0 Closed successfully ------------------------------------------------------------------------------- elevator_spec14_productSimulator_false.cil.c benchmark ------------------------------------------------------------------------------- Calling Ultimate with: ./Ultimate ./AutomizerTermination.xml elevator_spec14_productSimulator_false.cil.c --settings ./svComp-64bit-termination-Automizer.epf .......................................................................................................................................................................................................................................................................................................................................... Execution finished normally Writing output log to file Ultimate.log Result: UNKNOWN 2015-03-21 14:54:19,896 INFO [UltimateCore.java:207]: Initializing application 2015-03-21 14:54:19,897 INFO [UltimateCore.java:224]: -------------------------------------------------------------------------------- 2015-03-21 14:54:19,900 INFO [PluginFactory.java:62]: -------------------------------------------------------------------------------- 2015-03-21 14:54:19,900 INFO [PluginFactory.java:63]: Detecting plugins... 2015-03-21 14:54:19,901 INFO [PluginFactory.java:287]: 1 IController plugins available 2015-03-21 14:54:19,902 INFO [PluginFactory.java:287]: 3 ISource plugins available 2015-03-21 14:54:19,902 INFO [PluginFactory.java:287]: 1 IOutput plugins available 2015-03-21 14:54:19,903 INFO [PluginFactory.java:287]: 8 IGenerator plugins available 2015-03-21 14:54:19,903 INFO [PluginFactory.java:287]: 2 IAnalysis plugins available 2015-03-21 14:54:19,906 INFO [PluginFactory.java:241]: Loaded controller UltimateCore 2015-03-21 14:54:19,906 INFO [PluginFactory.java:70]: Finished detecting plugins! 2015-03-21 14:54:19,906 INFO [PluginFactory.java:71]: Loading services ... 2015-03-21 14:54:19,913 INFO [PluginFactory.java:272]: 1 IServiceFactory services available 2015-03-21 14:54:19,913 INFO [PluginFactory.java:73]: Finished loading services! 2015-03-21 14:54:19,913 INFO [PluginFactory.java:74]: -------------------------------------------------------------------------------- 2015-03-21 14:54:19,915 INFO [SettingsManager.java:38]: Loading settings from ./svComp-64bit-termination-Automizer.epf 2015-03-21 14:54:20,026 INFO [SettingsManager.java:46]: Loading preferences was successful 2015-03-21 14:54:20,026 INFO [UltimateCore.java:82]: Initializing controller ... 2015-03-21 14:54:20,166 INFO [PersistenceAwareModelManager.java:56]: Repository-Root is: /tmp 2015-03-21 14:54:20,408 INFO [ToolchainManager.java:372]: [Toolchain 1]: Parser CDTParser is usable. 2015-03-21 14:54:20,408 INFO [ToolchainManager.java:200]: [Toolchain 1]: Parser successfully initiated... 2015-03-21 14:54:20,408 INFO [PluginFactory.java:178]: -------------------------------------------------------------------------------- 2015-03-21 14:54:20,408 INFO [PluginFactory.java:179]: Loading all admissible plugins (creating one instance, loading preferences) 2015-03-21 14:54:20,446 INFO [PluginFactory.java:196]: Finished loading 14 admissible plugins (all were admissible) 2015-03-21 14:54:20,446 INFO [PluginFactory.java:198]: -------------------------------------------------------------------------------- 2015-03-21 14:54:20,448 INFO [ToolchainManager.java:180]: [Toolchain 1]: Toolchain data selected. 2015-03-21 14:54:20,449 INFO [PluginConnector.java:249]: Initializing CDTParser... 2015-03-21 14:54:20,450 INFO [PluginConnector.java:254]: CDTParser initialized 2015-03-21 14:54:20,454 INFO [ToolchainManager.java:327]: [Toolchain 1]: Parsing single file: /users/schram/svndeltacheck/branches/termination/regression/svcomp-product-lines/elevator_spec14_productSimulator_false.cil.c 2015-03-21 14:54:20,762 INFO [ToolchainManager.java:219]: ####################### [Toolchain 1] ####################### 2015-03-21 14:54:20,766 INFO [ToolchainWalker.java:61]: Walking toolchain with 5 elements. 2015-03-21 14:54:20,767 INFO [PluginConnector.java:90]: ------------------------CACSL2BoogieTranslator---------------------------- 2015-03-21 14:54:20,767 INFO [PluginConnector.java:249]: Initializing CACSL2BoogieTranslator... 2015-03-21 14:54:20,772 INFO [PluginConnector.java:254]: CACSL2BoogieTranslator initialized 2015-03-21 14:54:20,773 INFO [PluginConnector.java:159]: Executing the observer CACSL2BoogieTranslatorObserver from plugin CACSL2BoogieTranslator for "CDTParser AST 21.03 02:54:20" (1/1) ... 2015-03-21 14:54:20,777 INFO [CACSL2BoogieTranslatorObserver.java:85]: Settings: SV_COMP14 2015-03-21 14:54:21,034 INFO [PostProcessor.java:360]: Settings: Checked method=main 2015-03-21 14:54:21,047 INFO [PluginConnector.java:109]: ------------------------ END CACSL2BoogieTranslator---------------------------- 2015-03-21 14:54:21,047 INFO [PluginConnector.java:90]: ------------------------Boogie Preprocessor---------------------------- 2015-03-21 14:54:21,047 INFO [PluginConnector.java:249]: Initializing Boogie Preprocessor... 2015-03-21 14:54:21,047 INFO [PluginConnector.java:254]: Boogie Preprocessor initialized 2015-03-21 14:54:21,061 INFO [PluginConnector.java:159]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 21.03 02:54:21" (1/1) ... 2015-03-21 14:54:21,081 INFO [PluginConnector.java:159]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 21.03 02:54:21" (1/1) ... 2015-03-21 14:54:21,081 INFO [PluginConnector.java:159]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 21.03 02:54:21" (1/1) ... 2015-03-21 14:54:21,097 INFO [PluginConnector.java:159]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 21.03 02:54:21" (1/1) ... 2015-03-21 14:54:21,107 INFO [PluginConnector.java:159]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 21.03 02:54:21" (1/1) ... 2015-03-21 14:54:21,113 INFO [PluginConnector.java:159]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 21.03 02:54:21" (1/1) ... 2015-03-21 14:54:21,120 INFO [PluginConnector.java:109]: ------------------------ END Boogie Preprocessor---------------------------- 2015-03-21 14:54:21,120 INFO [PluginConnector.java:90]: ------------------------RCFGBuilder---------------------------- 2015-03-21 14:54:21,121 INFO [PluginConnector.java:249]: Initializing RCFGBuilder... 2015-03-21 14:54:21,121 INFO [PluginConnector.java:254]: RCFGBuilder initialized 2015-03-21 14:54:21,122 INFO [PluginConnector.java:159]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator AST 21.03 02:54:21" (1/1) ... 2015-03-21 14:54:21,139 INFO [MonitoredProcess.java:118]: Starting monitored process with z3 SMTLIB2_COMPLIANT=true -memory:2500 -smt2 -in -t:12000 (exit command is (exit)) 2015-03-21 14:54:21,162 INFO [BoogieDeclarations.java:130]: Found implementation of procedure __utac_acc__Specification14_spec__1 2015-03-21 14:54:21,162 INFO [BoogieDeclarations.java:130]: Found implementation of procedure getWeight 2015-03-21 14:54:21,162 INFO [BoogieDeclarations.java:130]: Found implementation of procedure getOrigin 2015-03-21 14:54:21,163 INFO [BoogieDeclarations.java:130]: Found implementation of procedure getDestination 2015-03-21 14:54:21,163 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isFloorCalling 2015-03-21 14:54:21,163 INFO [BoogieDeclarations.java:130]: Found implementation of procedure resetCallOnFloor 2015-03-21 14:54:21,163 INFO [BoogieDeclarations.java:130]: Found implementation of procedure callOnFloor 2015-03-21 14:54:21,163 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isPersonOnFloor 2015-03-21 14:54:21,164 INFO [BoogieDeclarations.java:130]: Found implementation of procedure initPersonOnFloor 2015-03-21 14:54:21,164 INFO [BoogieDeclarations.java:130]: Found implementation of procedure removePersonFromFloor 2015-03-21 14:54:21,164 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isTopFloor 2015-03-21 14:54:21,164 INFO [BoogieDeclarations.java:130]: Found implementation of procedure select_one 2015-03-21 14:54:21,165 INFO [BoogieDeclarations.java:130]: Found implementation of procedure select_features 2015-03-21 14:54:21,165 INFO [BoogieDeclarations.java:130]: Found implementation of procedure select_helpers 2015-03-21 14:54:21,165 INFO [BoogieDeclarations.java:130]: Found implementation of procedure valid_product 2015-03-21 14:54:21,165 INFO [BoogieDeclarations.java:130]: Found implementation of procedure bobCall 2015-03-21 14:54:21,165 INFO [BoogieDeclarations.java:130]: Found implementation of procedure bigMacCall 2015-03-21 14:54:21,166 INFO [BoogieDeclarations.java:130]: Found implementation of procedure threeTS 2015-03-21 14:54:21,166 INFO [BoogieDeclarations.java:130]: Found implementation of procedure cleanup 2015-03-21 14:54:21,166 INFO [BoogieDeclarations.java:130]: Found implementation of procedure setup 2015-03-21 14:54:21,166 INFO [BoogieDeclarations.java:130]: Found implementation of procedure runTest 2015-03-21 14:54:21,166 INFO [BoogieDeclarations.java:130]: Found implementation of procedure main 2015-03-21 14:54:21,167 INFO [BoogieDeclarations.java:130]: Found implementation of procedure test 2015-03-21 14:54:21,167 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isBlocked__before__overloaded 2015-03-21 14:54:21,167 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isBlocked__role__overloaded 2015-03-21 14:54:21,167 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isBlocked 2015-03-21 14:54:21,168 INFO [BoogieDeclarations.java:130]: Found implementation of procedure enterElevator__before__weight 2015-03-21 14:54:21,168 INFO [BoogieDeclarations.java:130]: Found implementation of procedure enterElevator__role__weight 2015-03-21 14:54:21,168 INFO [BoogieDeclarations.java:130]: Found implementation of procedure enterElevator 2015-03-21 14:54:21,168 INFO [BoogieDeclarations.java:130]: Found implementation of procedure leaveElevator__before__weight 2015-03-21 14:54:21,168 INFO [BoogieDeclarations.java:130]: Found implementation of procedure leaveElevator__role__weight 2015-03-21 14:54:21,169 INFO [BoogieDeclarations.java:130]: Found implementation of procedure leaveElevator__before__empty 2015-03-21 14:54:21,169 INFO [BoogieDeclarations.java:130]: Found implementation of procedure leaveElevator__role__empty 2015-03-21 14:54:21,169 INFO [BoogieDeclarations.java:130]: Found implementation of procedure leaveElevator 2015-03-21 14:54:21,169 INFO [BoogieDeclarations.java:130]: Found implementation of procedure pressInLiftFloorButton 2015-03-21 14:54:21,170 INFO [BoogieDeclarations.java:130]: Found implementation of procedure resetFloorButton 2015-03-21 14:54:21,170 INFO [BoogieDeclarations.java:130]: Found implementation of procedure getCurrentFloorID 2015-03-21 14:54:21,170 INFO [BoogieDeclarations.java:130]: Found implementation of procedure areDoorsOpen 2015-03-21 14:54:21,170 INFO [BoogieDeclarations.java:130]: Found implementation of procedure buttonForFloorIsPressed 2015-03-21 14:54:21,171 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isEmpty 2015-03-21 14:54:21,171 INFO [BoogieDeclarations.java:130]: Found implementation of procedure anyStopRequested 2015-03-21 14:54:21,171 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isIdle 2015-03-21 14:54:21,171 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedInDirection__before__twothirdsfull 2015-03-21 14:54:21,171 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedInDirection__role__twothirdsfull 2015-03-21 14:54:21,172 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedInDirection__before__executivefloor 2015-03-21 14:54:21,172 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedInDirection__role__executivefloor 2015-03-21 14:54:21,172 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedInDirection 2015-03-21 14:54:21,172 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isAnyLiftButtonPressed 2015-03-21 14:54:21,173 INFO [BoogieDeclarations.java:130]: Found implementation of procedure continueInDirection 2015-03-21 14:54:21,173 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedAtCurrentFloor__before__twothirdsfull 2015-03-21 14:54:21,173 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedAtCurrentFloor__role__twothirdsfull 2015-03-21 14:54:21,173 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedAtCurrentFloor__before__executivefloor 2015-03-21 14:54:21,174 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedAtCurrentFloor__role__executivefloor 2015-03-21 14:54:21,174 INFO [BoogieDeclarations.java:130]: Found implementation of procedure stopRequestedAtCurrentFloor 2015-03-21 14:54:21,174 INFO [BoogieDeclarations.java:130]: Found implementation of procedure getReverseHeading 2015-03-21 14:54:21,174 INFO [BoogieDeclarations.java:130]: Found implementation of procedure processWaitingOnFloor 2015-03-21 14:54:21,174 INFO [BoogieDeclarations.java:130]: Found implementation of procedure timeShift__before__overloaded 2015-03-21 14:54:21,175 INFO [BoogieDeclarations.java:130]: Found implementation of procedure timeShift__role__overloaded 2015-03-21 14:54:21,175 INFO [BoogieDeclarations.java:130]: Found implementation of procedure timeShift 2015-03-21 14:54:21,175 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isExecutiveFloorCalling 2015-03-21 14:54:21,175 INFO [BoogieDeclarations.java:130]: Found implementation of procedure isExecutiveFloor 2015-03-21 14:54:21,176 INFO [BoogieDeclarations.java:130]: Found implementation of procedure __automaton_fail 2015-03-21 14:54:21,176 INFO [BoogieDeclarations.java:130]: Found implementation of procedure ULTIMATE.init 2015-03-21 14:54:21,176 INFO [BoogieDeclarations.java:130]: Found implementation of procedure ULTIMATE.start 2015-03-21 14:54:21,176 INFO [BoogieDeclarations.java:122]: Found specification of procedure ~free 2015-03-21 14:54:21,176 INFO [BoogieDeclarations.java:122]: Found specification of procedure ~malloc 2015-03-21 14:54:21,177 INFO [BoogieDeclarations.java:122]: Found specification of procedure __VERIFIER_nondet_int 2015-03-21 14:54:21,177 INFO [BoogieDeclarations.java:122]: Found specification of procedure __automaton_fail 2015-03-21 14:54:21,177 INFO [BoogieDeclarations.java:122]: Found specification of procedure areDoorsOpen 2015-03-21 14:54:21,177 INFO [BoogieDeclarations.java:122]: Found specification of procedure getCurrentFloorID 2015-03-21 14:54:21,178 INFO [BoogieDeclarations.java:122]: Found specification of procedure isExecutiveFloorCalling 2015-03-21 14:54:21,178 INFO [BoogieDeclarations.java:122]: Found specification of procedure isExecutiveFloor 2015-03-21 14:54:21,178 INFO [BoogieDeclarations.java:122]: Found specification of procedure __utac_acc__Specification14_spec__1 2015-03-21 14:54:21,178 INFO [BoogieDeclarations.java:122]: Found specification of procedure getWeight 2015-03-21 14:54:21,179 INFO [BoogieDeclarations.java:122]: Found specification of procedure getOrigin 2015-03-21 14:54:21,179 INFO [BoogieDeclarations.java:122]: Found specification of procedure getDestination 2015-03-21 14:54:21,179 INFO [BoogieDeclarations.java:122]: Found specification of procedure isFloorCalling 2015-03-21 14:54:21,179 INFO [BoogieDeclarations.java:122]: Found specification of procedure resetCallOnFloor 2015-03-21 14:54:21,179 INFO [BoogieDeclarations.java:122]: Found specification of procedure callOnFloor 2015-03-21 14:54:21,180 INFO [BoogieDeclarations.java:122]: Found specification of procedure isPersonOnFloor 2015-03-21 14:54:21,180 INFO [BoogieDeclarations.java:122]: Found specification of procedure initPersonOnFloor 2015-03-21 14:54:21,180 INFO [BoogieDeclarations.java:122]: Found specification of procedure removePersonFromFloor 2015-03-21 14:54:21,180 INFO [BoogieDeclarations.java:122]: Found specification of procedure isTopFloor 2015-03-21 14:54:21,180 INFO [BoogieDeclarations.java:122]: Found specification of procedure timeShift 2015-03-21 14:54:21,181 INFO [BoogieDeclarations.java:122]: Found specification of procedure isBlocked 2015-03-21 14:54:21,181 INFO [BoogieDeclarations.java:122]: Found specification of procedure select_one 2015-03-21 14:54:21,181 INFO [BoogieDeclarations.java:122]: Found specification of procedure select_features 2015-03-21 14:54:21,181 INFO [BoogieDeclarations.java:122]: Found specification of procedure select_helpers 2015-03-21 14:54:21,182 INFO [BoogieDeclarations.java:122]: Found specification of procedure valid_product 2015-03-21 14:54:21,182 INFO [BoogieDeclarations.java:122]: Found specification of procedure bobCall 2015-03-21 14:54:21,182 INFO [BoogieDeclarations.java:122]: Found specification of procedure bigMacCall 2015-03-21 14:54:21,182 INFO [BoogieDeclarations.java:122]: Found specification of procedure threeTS 2015-03-21 14:54:21,182 INFO [BoogieDeclarations.java:122]: Found specification of procedure isIdle 2015-03-21 14:54:21,183 INFO [BoogieDeclarations.java:122]: Found specification of procedure cleanup 2015-03-21 14:54:21,183 INFO [BoogieDeclarations.java:122]: Found specification of procedure setup 2015-03-21 14:54:21,183 INFO [BoogieDeclarations.java:122]: Found specification of procedure test 2015-03-21 14:54:21,183 INFO [BoogieDeclarations.java:122]: Found specification of procedure runTest 2015-03-21 14:54:21,183 INFO [BoogieDeclarations.java:122]: Found specification of procedure main 2015-03-21 14:54:21,184 INFO [BoogieDeclarations.java:122]: Found specification of procedure enterElevator 2015-03-21 14:54:21,184 INFO [BoogieDeclarations.java:122]: Found specification of procedure isEmpty 2015-03-21 14:54:21,184 INFO [BoogieDeclarations.java:122]: Found specification of procedure isAnyLiftButtonPressed 2015-03-21 14:54:21,184 INFO [BoogieDeclarations.java:122]: Found specification of procedure buttonForFloorIsPressed 2015-03-21 14:54:21,184 INFO [BoogieDeclarations.java:122]: Found specification of procedure isBlocked__before__overloaded 2015-03-21 14:54:21,185 INFO [BoogieDeclarations.java:122]: Found specification of procedure isBlocked__role__overloaded 2015-03-21 14:54:21,185 INFO [BoogieDeclarations.java:122]: Found specification of procedure enterElevator__before__weight 2015-03-21 14:54:21,185 INFO [BoogieDeclarations.java:122]: Found specification of procedure enterElevator__role__weight 2015-03-21 14:54:21,185 INFO [BoogieDeclarations.java:122]: Found specification of procedure leaveElevator__before__weight 2015-03-21 14:54:21,185 INFO [BoogieDeclarations.java:122]: Found specification of procedure leaveElevator__role__weight 2015-03-21 14:54:21,186 INFO [BoogieDeclarations.java:122]: Found specification of procedure leaveElevator__before__empty 2015-03-21 14:54:21,186 INFO [BoogieDeclarations.java:122]: Found specification of procedure leaveElevator__role__empty 2015-03-21 14:54:21,186 INFO [BoogieDeclarations.java:122]: Found specification of procedure leaveElevator 2015-03-21 14:54:21,186 INFO [BoogieDeclarations.java:122]: Found specification of procedure pressInLiftFloorButton 2015-03-21 14:54:21,186 INFO [BoogieDeclarations.java:122]: Found specification of procedure resetFloorButton 2015-03-21 14:54:21,187 INFO [BoogieDeclarations.java:122]: Found specification of procedure anyStopRequested 2015-03-21 14:54:21,187 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedInDirection__before__twothirdsfull 2015-03-21 14:54:21,187 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedInDirection__role__twothirdsfull 2015-03-21 14:54:21,187 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedInDirection__before__executivefloor 2015-03-21 14:54:21,187 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedInDirection__role__executivefloor 2015-03-21 14:54:21,188 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedInDirection 2015-03-21 14:54:21,188 INFO [BoogieDeclarations.java:122]: Found specification of procedure continueInDirection 2015-03-21 14:54:21,188 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedAtCurrentFloor__before__twothirdsfull 2015-03-21 14:54:21,188 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedAtCurrentFloor__role__twothirdsfull 2015-03-21 14:54:21,188 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedAtCurrentFloor__before__executivefloor 2015-03-21 14:54:21,189 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedAtCurrentFloor__role__executivefloor 2015-03-21 14:54:21,189 INFO [BoogieDeclarations.java:122]: Found specification of procedure stopRequestedAtCurrentFloor 2015-03-21 14:54:21,189 INFO [BoogieDeclarations.java:122]: Found specification of procedure getReverseHeading 2015-03-21 14:54:21,189 INFO [BoogieDeclarations.java:122]: Found specification of procedure processWaitingOnFloor 2015-03-21 14:54:21,189 INFO [BoogieDeclarations.java:122]: Found specification of procedure timeShift__before__overloaded 2015-03-21 14:54:21,190 INFO [BoogieDeclarations.java:122]: Found specification of procedure timeShift__role__overloaded 2015-03-21 14:54:21,190 INFO [BoogieDeclarations.java:122]: Found specification of procedure ULTIMATE.init 2015-03-21 14:54:21,190 INFO [BoogieDeclarations.java:122]: Found specification of procedure ULTIMATE.start 2015-03-21 14:54:23,409 INFO [PluginConnector.java:109]: ------------------------ END RCFGBuilder---------------------------- 2015-03-21 14:54:23,409 INFO [PluginConnector.java:90]: ------------------------BlockEncoding---------------------------- 2015-03-21 14:54:23,409 INFO [PluginConnector.java:249]: Initializing BlockEncoding... 2015-03-21 14:54:23,411 INFO [PluginConnector.java:254]: BlockEncoding initialized 2015-03-21 14:54:23,411 INFO [PluginConnector.java:159]: Executing the observer BlockEncodingObserver from plugin BlockEncoding for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 21.03 02:54:23" (1/1) ... 2015-03-21 14:54:23,413 INFO [BlockEncoder.java:61]: Start BlockEncoding on RCFG 2015-03-21 14:54:23,417 INFO [BlockEncoder.java:169]: Start processing function: cleanup 2015-03-21 14:54:23,421 INFO [BlockEncoder.java:169]: Start processing function: isExecutiveFloor 2015-03-21 14:54:23,421 INFO [BlockEncoder.java:169]: Start processing function: isIdle 2015-03-21 14:54:23,422 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedInDirection__role__twothirdsfull 2015-03-21 14:54:23,422 INFO [BlockEncoder.java:169]: Start processing function: test 2015-03-21 14:54:23,423 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedAtCurrentFloor__role__executivefloor 2015-03-21 14:54:23,423 INFO [BlockEncoder.java:169]: Start processing function: bigMacCall 2015-03-21 14:54:23,424 INFO [BlockEncoder.java:169]: Start processing function: leaveElevator__role__weight 2015-03-21 14:54:23,424 INFO [BlockEncoder.java:169]: Start processing function: isTopFloor 2015-03-21 14:54:23,424 INFO [BlockEncoder.java:169]: Start processing function: isEmpty 2015-03-21 14:54:23,426 INFO [BlockEncoder.java:169]: Start processing function: leaveElevator__before__weight 2015-03-21 14:54:23,427 INFO [BlockEncoder.java:169]: Start processing function: isBlocked__role__overloaded 2015-03-21 14:54:23,427 INFO [BlockEncoder.java:169]: Start processing function: enterElevator__role__weight 2015-03-21 14:54:23,428 INFO [BlockEncoder.java:169]: Start processing function: continueInDirection 2015-03-21 14:54:23,429 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedInDirection__before__twothirdsfull 2015-03-21 14:54:23,441 INFO [BlockEncoder.java:169]: Start processing function: ULTIMATE.init 2015-03-21 14:54:23,441 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedAtCurrentFloor__before__twothirdsfull 2015-03-21 14:54:23,442 INFO [BlockEncoder.java:169]: Start processing function: getCurrentFloorID 2015-03-21 14:54:23,442 INFO [BlockEncoder.java:169]: Start processing function: resetCallOnFloor 2015-03-21 14:54:23,443 INFO [BlockEncoder.java:169]: Start processing function: __utac_acc__Specification14_spec__1 2015-03-21 14:54:23,444 INFO [BlockEncoder.java:169]: Start processing function: isBlocked 2015-03-21 14:54:23,445 INFO [BlockEncoder.java:169]: Start processing function: initPersonOnFloor 2015-03-21 14:54:23,453 INFO [BlockEncoder.java:169]: Start processing function: select_one 2015-03-21 14:54:23,454 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedAtCurrentFloor__before__executivefloor 2015-03-21 14:54:23,455 INFO [BlockEncoder.java:169]: Start processing function: select_features 2015-03-21 14:54:23,455 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedAtCurrentFloor 2015-03-21 14:54:23,456 INFO [BlockEncoder.java:169]: Start processing function: leaveElevator 2015-03-21 14:54:23,457 INFO [BlockEncoder.java:169]: Start processing function: runTest 2015-03-21 14:54:23,457 INFO [BlockEncoder.java:169]: Start processing function: __automaton_fail 2015-03-21 14:54:23,457 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedInDirection 2015-03-21 14:54:23,458 INFO [BlockEncoder.java:169]: Start processing function: timeShift 2015-03-21 14:54:23,459 INFO [BlockEncoder.java:169]: Start processing function: getWeight 2015-03-21 14:54:23,461 INFO [BlockEncoder.java:169]: Start processing function: callOnFloor 2015-03-21 14:54:23,462 INFO [BlockEncoder.java:169]: Start processing function: getOrigin 2015-03-21 14:54:23,464 INFO [BlockEncoder.java:169]: Start processing function: leaveElevator__role__empty 2015-03-21 14:54:23,465 INFO [BlockEncoder.java:169]: Start processing function: pressInLiftFloorButton 2015-03-21 14:54:23,466 INFO [BlockEncoder.java:169]: Start processing function: isExecutiveFloorCalling 2015-03-21 14:54:23,466 INFO [BlockEncoder.java:169]: Start processing function: setup 2015-03-21 14:54:23,466 INFO [BlockEncoder.java:169]: Start processing function: valid_product 2015-03-21 14:54:23,467 INFO [BlockEncoder.java:169]: Start processing function: timeShift__before__overloaded 2015-03-21 14:54:23,471 INFO [BlockEncoder.java:169]: Start processing function: isBlocked__before__overloaded 2015-03-21 14:54:23,471 INFO [BlockEncoder.java:169]: Start processing function: enterElevator 2015-03-21 14:54:23,471 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedAtCurrentFloor__role__twothirdsfull 2015-03-21 14:54:23,471 INFO [BlockEncoder.java:169]: Start processing function: bobCall 2015-03-21 14:54:23,472 INFO [BlockEncoder.java:169]: Start processing function: enterElevator__before__weight 2015-03-21 14:54:23,473 INFO [BlockEncoder.java:169]: Start processing function: processWaitingOnFloor 2015-03-21 14:54:23,475 INFO [BlockEncoder.java:169]: Start processing function: removePersonFromFloor 2015-03-21 14:54:23,483 INFO [BlockEncoder.java:169]: Start processing function: isPersonOnFloor 2015-03-21 14:54:23,488 INFO [BlockEncoder.java:169]: Start processing function: isFloorCalling 2015-03-21 14:54:23,489 INFO [BlockEncoder.java:169]: Start processing function: resetFloorButton 2015-03-21 14:54:23,491 INFO [BlockEncoder.java:169]: Start processing function: ULTIMATE.start 2015-03-21 14:54:23,491 INFO [BlockEncoder.java:169]: Start processing function: select_helpers 2015-03-21 14:54:23,492 INFO [BlockEncoder.java:169]: Start processing function: main 2015-03-21 14:54:23,492 INFO [BlockEncoder.java:169]: Start processing function: leaveElevator__before__empty 2015-03-21 14:54:23,492 INFO [BlockEncoder.java:169]: Start processing function: threeTS 2015-03-21 14:54:23,493 INFO [BlockEncoder.java:169]: Start processing function: timeShift__role__overloaded 2015-03-21 14:54:23,493 INFO [BlockEncoder.java:169]: Start processing function: buttonForFloorIsPressed 2015-03-21 14:54:23,494 INFO [BlockEncoder.java:169]: Start processing function: areDoorsOpen 2015-03-21 14:54:23,494 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedInDirection__before__executivefloor 2015-03-21 14:54:23,495 INFO [BlockEncoder.java:169]: Start processing function: stopRequestedInDirection__role__executivefloor 2015-03-21 14:54:23,495 INFO [BlockEncoder.java:169]: Start processing function: getDestination 2015-03-21 14:54:23,496 INFO [BlockEncoder.java:169]: Start processing function: isAnyLiftButtonPressed 2015-03-21 14:54:23,498 INFO [BlockEncoder.java:169]: Start processing function: getReverseHeading 2015-03-21 14:54:23,498 INFO [BlockEncoder.java:169]: Start processing function: anyStopRequested 2015-03-21 14:54:23,501 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,501 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,508 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,511 WARN [MinimizeCallReturnVisitor.java:345]: Node at this point should only have Return and Summary as incoming edges! 2015-03-21 14:54:23,512 WARN [MinimizeCallReturnVisitor.java:345]: Node at this point should only have Return and Summary as incoming edges! 2015-03-21 14:54:23,531 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,536 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,541 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,542 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,542 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,542 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,543 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,543 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,545 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,545 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,548 ERROR [TestMinimizationVisitor.java:49]: Sequential Minimization is possible -> so Minimization is not complete 2015-03-21 14:54:23,548 INFO [TestMinimizationVisitor.java:50]: Node: enterElevatorFINAL 2015-03-21 14:54:23,549 INFO [TestMinimizationVisitor.java:51]: Incoming Edges: [CompositeEdge] 2015-03-21 14:54:23,549 INFO [TestMinimizationVisitor.java:52]: Outgoing Edges: [assume true;] 2015-03-21 14:54:23,551 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,551 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,553 ERROR [TestMinimizationVisitor.java:49]: Sequential Minimization is possible -> so Minimization is not complete 2015-03-21 14:54:23,553 INFO [TestMinimizationVisitor.java:50]: Node: leaveElevator__before__emptyFINAL 2015-03-21 14:54:23,553 INFO [TestMinimizationVisitor.java:51]: Incoming Edges: [CompositeEdge] 2015-03-21 14:54:23,553 INFO [TestMinimizationVisitor.java:52]: Outgoing Edges: [assume true;] 2015-03-21 14:54:23,567 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,567 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,567 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,568 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,568 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,568 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,569 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,569 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,570 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,571 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,572 ERROR [TestMinimizationVisitor.java:49]: Sequential Minimization is possible -> so Minimization is not complete 2015-03-21 14:54:23,572 INFO [TestMinimizationVisitor.java:50]: Node: enterElevatorFINAL 2015-03-21 14:54:23,572 INFO [TestMinimizationVisitor.java:51]: Incoming Edges: [CompositeEdge] 2015-03-21 14:54:23,573 INFO [TestMinimizationVisitor.java:52]: Outgoing Edges: [assume true;] 2015-03-21 14:54:23,573 INFO [MinimizeLoopVisitor.java:169]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,574 INFO [TestMinimizationVisitor.java:113]: Found Parallel Nodes, should not happen 2015-03-21 14:54:23,575 ERROR [TestMinimizationVisitor.java:49]: Sequential Minimization is possible -> so Minimization is not complete 2015-03-21 14:54:23,575 INFO [TestMinimizationVisitor.java:50]: Node: leaveElevator__before__emptyFINAL 2015-03-21 14:54:23,575 INFO [TestMinimizationVisitor.java:51]: Incoming Edges: [CompositeEdge] 2015-03-21 14:54:23,575 INFO [TestMinimizationVisitor.java:52]: Outgoing Edges: [assume true;] 2015-03-21 14:54:23,578 WARN [MinimizeCallReturnVisitor.java:345]: Node at this point should only have Return and Summary as incoming edges! 2015-03-21 14:54:23,579 ERROR [ToolchainWalker.java:135]: The Plugin de.uni_freiburg.informatik.ultimate.plugins.generator.blockencoding has thrown an Exception! java.lang.IllegalStateException: There should be an returnEdge at de.uni_freiburg.informatik.ultimate.blockencoding.algorithm.MinimizeCallReturnVisitor.minimizeCallReturnEdge(MinimizeCallReturnVisitor.java:326) at de.uni_freiburg.informatik.ultimate.blockencoding.algorithm.MinimizeCallReturnVisitor.internalVisitNode(MinimizeCallReturnVisitor.java:148) at de.uni_freiburg.informatik.ultimate.blockencoding.algorithm.MinimizeCallReturnVisitor.visitNode(MinimizeCallReturnVisitor.java:62) at de.uni_freiburg.informatik.ultimate.blockencoding.algorithm.BlockEncoder.startMinimization(BlockEncoder.java:122) at de.uni_freiburg.informatik.ultimate.plugins.generator.blockencoding.BlockEncodingObserver.process(BlockEncodingObserver.java:27) at de.uni_freiburg.informatik.ultimate.access.walker.CFGWalker.runObserver(CFGWalker.java:78) at de.uni_freiburg.informatik.ultimate.access.walker.BaseWalker.runObserver(BaseWalker.java:62) at de.uni_freiburg.informatik.ultimate.access.walker.BaseWalker.run(BaseWalker.java:55) at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:141) at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:126) at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:106) at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:127) at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:74) at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:236) at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.runToolchainDefault(DefaultToolchainJob.java:199) at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.BasicToolchainJob.run(BasicToolchainJob.java:152) at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54) 2015-03-21 14:54:23,582 INFO [ResultNotifier.java:103]: RESULT: Ultimate could not prove your program: Toolchain returned no Result. RESULT: Ultimate could not prove your program: Toolchain returned no Result. 2015-03-21 14:54:23,582 INFO [ToolchainManager.java:258]: ####################### End [Toolchain 1] ####################### 2015-03-21 14:54:23,582 FATAL [DefaultToolchainJob.java:202]: The toolchain threw an exception: null 2015-03-21 14:54:23,582 FATAL [DefaultToolchainJob.java:203]: de.uni_freiburg.informatik.ultimate.plugins.generator.blockencoding: java.lang.IllegalStateException: There should be an returnEdge 2015-03-21 14:54:23,583 INFO [BasicToolchainJob.java:73]: --- Results --- 2015-03-21 14:54:23,584 INFO [BasicToolchainJob.java:75]: * Results from UltimateCore: 2015-03-21 14:54:23,584 INFO [BasicToolchainJob.java:89]: - ExceptionOrErrorResult: IllegalStateException: There should be an returnEdge 2015-03-21 14:54:23,584 INFO [BasicToolchainJob.java:95]: de.uni_freiburg.informatik.ultimate.plugins.generator.blockencoding: IllegalStateException: There should be an returnEdge: de.uni_freiburg.informatik.ultimate.blockencoding.algorithm.MinimizeCallReturnVisitor.minimizeCallReturnEdge(MinimizeCallReturnVisitor.java:326) 2015-03-21 14:54:23,586 INFO [UltimateCore.java:90]: Preparing to exit Ultimate with return code 0 Closed successfully ================================================================================ 2. Loopus ================================================================================ Loopus could not compute ranking functions for any of the product-lines benchmarks. Next, we provide one example from each category. ------------------------------------------------------------------------------- an elevator benchmark ------------------------------------------------------------------------------- command line: clang -g -emit-llvm -c elevator_spec13_product21_true-unreach-call.cil.c loopus -zT 120 elevator_spec13_product21_true-unreach-call.cil.o -zPrintRankingFunction Function cleanup line 67 (× i -1 ) Function randomSequenceOfActions line 91 (× counter -1 ) Function existInLiftCallsInDirection line 403 (× i -1 ) line 412 FAILED to compute RF line 412 FAILED to compute RF Function spec1 line 35 (× i -1 ) Function spec14 line 57 (× i -1 ) Function __utac__exception__cf_handler_free line 49 FAILED to compute RF Function __utac__exception__cf_handler_reset line 64 FAILED to compute RF Function __utac__error_stack_mgt line 98 count3 ------------------------------------------------------------------------------- an email benchmark ------------------------------------------------------------------------------- Command line: clang -g -emit-llvm -c email_spec0_product05_true-unreach-call.cil.c loopus -zT 120 email_spec0_product05_true-unreach-call.cil.o -zPrintRankingFunction Function test line 14 (× splverifierCounter -1 ) Function __utac__exception__cf_handler_free line 49 FAILED to compute RF Function __utac__exception__cf_handler_reset line 64 FAILED to compute RF Function __utac__error_stack_mgt line 98 count3 ------------------------------------------------------------------------------ a minepump benchmark ------------------------------------------------------------------------------- Command line: clang -g -emit-llvm -c minepump_spec1_product01_true-unreach-call.cil.c loopus -zT 120 minepump_spec1_product01_true-unreach-call.cil.o -zPrintRankingFunction Function cleanup line 22 (× i -1 ) Function test line 3 FAILED to compute RF Function __utac__exception__cf_handler_free line 49 FAILED to compute RF Function __utac__exception__cf_handler_reset line 64 FAILED to compute RF Function __utac__error_stack_mgt line 98 count3 ================================================================================ 3. HipTNT+ ================================================================================ We have used the online verifier, and obtained the error message: Error: Failure("TRUNG TODO: handle TFun later! Maybe it's function pointer case?") The authors confirmed that they can't handle function pointers, which are used in the product-lines benchmarks. ================================================================================ 4. FuncTion ================================================================================ When using FuncTion, we obtained parsing errors. The authors confirmed that the tool can't handle structs, which are used in the product-lines benchmarks. ================================================================================ 5. AProVE ================================================================================ Whenver running AProVE on the product-lines benchmarks, we've obtained parsing errors of the type described below. The authors of AProVE confirmed that the cause of the problem is the fact that AProVE is not yet able to handle structs (as also mentioned in the section „Limitations“ on http://aprove.informatik.rwth-aachen.de/eval/Pointer/). Elevator.c:376:10: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(__cil_tmp6); ^~~~~~~~~~ Elevator.c:378:12: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(__cil_tmp7); ^~~~~~~~~~ Elevator.c:379:12: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(__cil_tmp8); ^~~~~~~~~~ Elevator.c:379:10: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(__cil_tmp9); ^~~~~~~~~~ Elevator.c:381:10: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(__cil_tmp11); ^~~~~~~~~~~ Elevator.c:383:12: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(__cil_tmp12); ^~~~~~~~~~~ Elevator.c:384:12: warning: format string is not a string literal (potentially insecure) [-Wformat-sec urity] printf(__cil_tmp13); ^~~~~~~~~~~ Elevator.c:384:10: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(__cil_tmp14); ^~~~~~~~~~~ Elevator.c:390:10: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(__cil_tmp20); ^~~~~~~~~~~ Elevator.c:396:10: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(__cil_tmp26); ^~~~~~~~~~~ 10 warnings generated. line 5:51 mismatched input ')*' expecting ')' line 5:100 mismatched input ')*' expecting ')' line 5:132 mismatched input ')*' expecting ')' line 7:49 mismatched input ')*' expecting ')' line 62:16 no viable alternative at input 'unnamed_addr' line 63:17 no viable alternative at input 'unnamed_addr' line 64:17 no viable alternative at input 'unnamed_addr' line 65:17 no viable alternative at input 'unnamed_addr' line 66:17 no viable alternative at input 'unnamed_addr' line 67:17 no viable alternative at input 'unnamed_addr' line 68:17 no viable alternative at input 'unnamed_addr' line 69:17 no viable alternative at input 'unnamed_addr' line 70:17 no viable alternative at input 'unnamed_addr' line 71:17 no viable alternative at input 'unnamed_addr' line 72:18 no viable alternative at input 'unnamed_addr' line 73:18 no viable alternative at input 'unnamed_addr' line 76:18 no viable alternative at input 'unnamed_addr' line 77:18 no viable alternative at input 'unnamed_addr' line 78:18 no viable alternative at input 'unnamed_addr' line 79:18 no viable alternative at input 'unnamed_addr' line 5443:76 mismatched input ')*' expecting ')' line 5445:27 mismatched input ')*' expecting ')' line 5458:32 mismatched input ')*' expecting ')' line 5464:21 mismatched input ')*' expecting ')' line 5464:50 mismatched input ')*' expecting ')' line 5475:54 no viable alternative at input '(' line 5476:21 mismatched input ')*' expecting ')' line 5476:43 mismatched input ')*' expecting ')' line 5477:26 mismatched input ')*' expecting ')' line 5478:26 mismatched input ')*' expecting ')' line 5479:21 mismatched input ')*' expecting ')' line 5479:42 mismatched input ')*' expecting ')' line 5637:37 mismatched input ')*' expecting ')' line 5644:32 mismatched input ')*' expecting ')' line 5689:55 no viable alternative at input '(' line 5690:21 mismatched input ')*' expecting ')' line 5690:43 mismatched input ')*' expecting ')' line 5691:26 mismatched input ')*' expecting ')' line 5692:26 mismatched input ')*' expecting ')' line 5693:21 mismatched input ')*' expecting ')' line 5693:42 mismatched input ')*' expecting ')' line 5706:26 mismatched input ')*' expecting ')' Aborted 1414698111Exec. 2, CToLLVM with some error. Reason: java.lang.NullPointerException. aprove.InputModules.Programs.llvm.parseStructures.dataTypes.StructureType.convertToBasicType(StructureType.java:48) aprove.InputModules.Programs.llvm.parseStructures.LLVMParseModule.createBasicStructure(LLVMParseModule.java:55) aprove.InputModules.Programs.llvm.Translator.translate(Translator.java:132) aprove.InputModules.Programs.llvm.Translator.translate(Translator.java:113) aprove.Framework.Input.Translator$Skeleton.translate(Translator.java:91) aprove.InputModules.Programs.c.CToLLVMProcessor.process(CToLLVMProcessor.java:62) aprove.Strategies.ExecutableStrategies.Executor.execute(Executor.java:326) aprove.Strategies.ExecutableStrategies.Executor$Runner.wrappedRun(Executor.java:377) aprove.Strategies.Abortions.PooledJob.run(PooledJob.java:98) aprove.Strategies.Util.PrioritizableThreadPool$Worker.run(PrioritizableThreadPool.java:273) java.lang.Thread.run(Thread.java:745) java.lang.NullPointerException at aprove.InputModules.Programs.llvm.parseStructures.dataTypes.StructureType.convertToBasicType(StructureType.java:48) at aprove.InputModules.Programs.llvm.parseStructures.LLVMParseModule.createBasicStructure(LLVMParseModule.java:55) at aprove.InputModules.Programs.llvm.Translator.translate(Translator.java:132) at aprove.InputModules.Programs.llvm.Translator.translate(Translator.java:113) at aprove.Framework.Input.Translator$Skeleton.translate(Translator.java:91) at aprove.InputModules.Programs.c.CToLLVMProcessor.process(CToLLVMProcessor.java:62) at aprove.Strategies.ExecutableStrategies.Executor.execute(Executor.java:326) at aprove.Strategies.ExecutableStrategies.Executor$Runner.wrappedRun(Executor.java:377) at aprove.Strategies.Abortions.PooledJob.run(PooledJob.java:98) at aprove.Strategies.Util.PrioritizableThreadPool$Worker.run(PrioritizableThreadPool.java:273) at java.lang.Thread.run(Thread.java:745) MAYBE ================================================================================ 6. ARMC ================================================================================ ARMC cannot handle procedures. Thus, we need to use HSF(c) -- qarmc. However, HSF(c)'s frontend only generates Horn clauses from a proof rule for safety and, in order to use it for termination, we would need to manually instrument the Horn clauses.