./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:47,712 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:47,813 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:47,819 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:47,819 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:47,845 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:47,845 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:47,846 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:47,846 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:47,846 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:47,846 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:47,847 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:47,847 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:47,847 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:47,847 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:47,847 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:47,847 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:47,848 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:47,849 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:47,849 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:47,849 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:47,849 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:47,849 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:47,850 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:47,850 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:47,850 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:47,851 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:48,189 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:48,197 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:48,200 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:48,201 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:48,201 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:48,202 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2
[2025-04-28 21:21:48,204 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:48,207 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
Unexpected Exception: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2:1270:0: Function c_hbv_main.ATNodeBlock.i_A1_33 is already defined.
[2025-04-28 21:21:48,957 INFO  L344              SmtParser]: Failed while executing SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2
[2025-04-28 21:21:48,958 INFO  L345              SmtParser]: SMTLIBException de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2:1270:0: Function c_hbv_main.ATNodeBlock.i_A1_33 is already defined.
[2025-04-28 21:21:48,958 FATAL L?                        ?]: [Toolchain 1]: Exception during parsing: 
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2:1270:0: Function c_hbv_main.ATNodeBlock.i_A1_33 is already defined.
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:123)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:99)
	at de.uni_freiburg.informatik.ultimate.source.smtparser.SmtParser.processFile(SmtParser.java:338)
	at de.uni_freiburg.informatik.ultimate.source.smtparser.SmtParser.parseAST(SmtParser.java:131)
	at de.uni_freiburg.informatik.ultimate.source.smtparser.SmtParser.parseAST(SmtParser.java:125)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.runParser(ToolchainManager.java:439)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.runParsers(ToolchainManager.java:285)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:142)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Caused by: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2:1270:0: Function c_hbv_main.ATNodeBlock.i_A1_33 is already defined.
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.ExceptionThrowingParseEnvironment.printError(ExceptionThrowingParseEnvironment.java:52)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2892)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1333)
	at com.github.jhoenicke.javacup.runtime.LRParser.parse(LRParser.java:383)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:120)
	... 8 more
The toolchain threw an exception: class de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2:1270:0: Function c_hbv_main.ATNodeBlock.i_A1_33 is already defined.
RESULT: An exception occured during the execution of Ultimate: The toolchain threw an exception
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2:1270:0: Function c_hbv_main.ATNodeBlock.i_A1_33 is already defined.
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:123)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:99)
	at de.uni_freiburg.informatik.ultimate.source.smtparser.SmtParser.processFile(SmtParser.java:338)
	at de.uni_freiburg.informatik.ultimate.source.smtparser.SmtParser.parseAST(SmtParser.java:131)
	at de.uni_freiburg.informatik.ultimate.source.smtparser.SmtParser.parseAST(SmtParser.java:125)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.runParser(ToolchainManager.java:439)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.runParsers(ToolchainManager.java:285)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:142)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Caused by: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec0ea788-9341-4c4c-9c5a-282286c5f939/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-147.smt2:1270:0: Function c_hbv_main.ATNodeBlock.i_A1_33 is already defined.
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.ExceptionThrowingParseEnvironment.printError(ExceptionThrowingParseEnvironment.java:52)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2892)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1333)
	at com.github.jhoenicke.javacup.runtime.LRParser.parse(LRParser.java:383)
	at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:120)
	... 8 more
Received shutdown request...
unknown

