./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/operators/delete_function.sol_4_no_adts_000.smt2 .


--------------------------------------------------------------------------------


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:26:37,140 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:26:37,192 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_72e78e0d-c12c-48e3-b1be-55f402589792/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:26:37,196 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:26:37,196 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:26:37,215 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:26:37,216 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:26:37,216 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:26:37,216 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:26:37,216 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:26:37,217 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:26:37,217 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:26:37,217 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:26:37,217 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:26:37,217 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:26:37,217 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:26:37,217 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:26:37,217 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:26:37,217 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:37,218 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:26:37,218 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:26:37,218 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:26:37,218 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:26:37,218 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:26:37,218 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:26:37,219 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:26:37,219 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:26:37,427 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:26:37,434 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:26:37,437 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:26:37,438 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:26:37,438 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:26:37,439 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_72e78e0d-c12c-48e3-b1be-55f402589792/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/operators/delete_function.sol_4_no_adts_000.smt2
[2025-05-07 17:26:37,440 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:26:37,443 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:26:37,771 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_72e78e0d-c12c-48e3-b1be-55f402589792/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/operators/delete_function.sol_4_no_adts_000.smt2
[2025-05-07 17:26:37,774 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:26:37,775 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:26:37,776 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:26:37,776 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:26:37,776 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:26:37,779 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:37" (1/1) ...
[2025-05-07 17:26:37,828 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:37 Unit
[2025-05-07 17:26:37,828 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:26:37,829 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:26:37,829 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:26:37,829 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:26:37,845 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:37" (1/1) ...
[2025-05-07 17:26:37,845 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:37" (1/1) ...
[2025-05-07 17:26:37,873 FATAL L?                        ?]: The Plugin de.uni_freiburg.informatik.ultimate.boogie.preprocessor has thrown an exception:
java.lang.IllegalStateException: Unknown expression node null
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.typecheckExpression(TypeChecker.java:325)
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.typecheckExpression(TypeChecker.java:195)
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.typecheckExpression(TypeChecker.java:195)
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.typecheckExpression(TypeChecker.java:195)
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.typecheckExpression(TypeChecker.java:195)
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.typecheckStatement(TypeChecker.java:669)
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.typecheckBlock(TypeChecker.java:856)
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.processBody(TypeChecker.java:967)
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.processImplementation(TypeChecker.java:1043)
	at de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.process(TypeChecker.java:1130)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.DFSTreeWalker.runObserver(DFSTreeWalker.java:65)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.runObserver(BaseWalker.java:93)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.run(BaseWalker.java:86)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:166)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:155)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:127)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:233)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:227)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:144)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:106)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:319)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
[2025-05-07 17:26:37,877 INFO  L158              Benchmark]: Toolchain (without parser) took 101.84ms. Allocated memory is still 234.9MB. Free memory was 134.7MB in the beginning and 127.8MB in the end (delta: 7.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:37,878 INFO  L158              Benchmark]: SmtParser took 0.23ms. Allocated memory is still 234.9MB. Free memory is still 173.6MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:37,878 INFO  L158              Benchmark]: ChcToBoogie took 52.39ms. Allocated memory is still 234.9MB. Free memory was 134.7MB in the beginning and 130.2MB in the end (delta: 4.5MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:37,878 INFO  L158              Benchmark]: Boogie Preprocessor took 47.31ms. Allocated memory is still 234.9MB. Free memory was 130.1MB in the beginning and 127.8MB in the end (delta: 2.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:37,880 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.23ms. Allocated memory is still 234.9MB. Free memory is still 173.6MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 52.39ms. Allocated memory is still 234.9MB. Free memory was 134.7MB in the beginning and 130.2MB in the end (delta: 4.5MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 47.31ms. Allocated memory is still 234.9MB. Free memory was 130.1MB in the beginning and 127.8MB in the end (delta: 2.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.boogie.preprocessor:
  - ExceptionOrErrorResult: IllegalStateException: Unknown expression node null
    de.uni_freiburg.informatik.ultimate.boogie.preprocessor: IllegalStateException: Unknown expression node null: de.uni_freiburg.informatik.ultimate.boogie.preprocessor.TypeChecker.typecheckExpression(TypeChecker.java:325)
RESULT: Ultimate could not prove your program: Toolchain returned no result.
Received shutdown request...
unknown

