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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:41,988 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:42,047 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_aabe3b08-1e72-4a8f-a9cf-143df8c6be45/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:42,051 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:42,052 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:42,073 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:42,074 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:42,074 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:42,074 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:42,074 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:42,075 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:42,075 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:42,075 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:42,075 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:42,075 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:42,075 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:42,075 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:42,076 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:42,076 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:42,076 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:42,076 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:42,076 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:42,076 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:42,076 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:42,077 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:42,077 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:42,077 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:42,359 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:42,373 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:42,376 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:42,377 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:42,377 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:42,381 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_aabe3b08-1e72-4a8f-a9cf-143df8c6be45/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-021.smt2
[2025-04-28 21:21:42,384 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:42,387 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:42,819 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_aabe3b08-1e72-4a8f-a9cf-143df8c6be45/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-021.smt2
[2025-04-28 21:21:42,823 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:42,825 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:42,826 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:42,826 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:42,826 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:42,829 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,885 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42 Unit
[2025-04-28 21:21:42,885 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:42,886 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:42,886 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:42,886 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:42,902 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,902 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,926 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,926 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,932 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,934 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,936 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,938 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,939 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,961 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:42,962 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:42,962 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:42,962 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:42,963 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,966 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:42,991 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,005 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,011 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,020 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:43,020 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:43,021 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:43,021 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATprecall.split given in one single declaration
[2025-04-28 21:21:43,021 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATprecall.split
[2025-04-28 21:21:43,021 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATprecall.split
[2025-04-28 21:21:43,021 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT_bb given in one single declaration
[2025-04-28 21:21:43,021 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT_bb
[2025-04-28 21:21:43,021 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT_bb
[2025-04-28 21:21:43,021 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:43,021 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:43,021 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:43,022 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:43,022 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:43,022 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:43,126 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:43,128 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:43,439 INFO  L?                        ?]: Removed 223 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:43,439 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:43,454 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:43,454 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:43,454 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:43 BoogieIcfgContainer
[2025-04-28 21:21:43,454 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:43,461 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:43,461 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:43,466 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:43,467 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:42" (1/3) ...
[2025-04-28 21:21:43,468 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3808da2f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:43, skipping insertion in model container
[2025-04-28 21:21:43,469 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (2/3) ...
[2025-04-28 21:21:43,469 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3808da2f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:43, skipping insertion in model container
[2025-04-28 21:21:43,469 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:43" (3/3) ...
[2025-04-28 21:21:43,472 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:43,491 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:43,494 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 5 procedures, 19 locations, 25 edges, 5 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:43,556 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:43,566 INFO  L340      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=None, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@26112c5f, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:43,567 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:43,570 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 19 states, 8 states have (on average 1.25) internal successors, (10), 10 states have internal predecessors, (10), 5 states have call successors, (5), 4 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:43,580 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:43,580 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,581 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,581 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,587 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,587 INFO  L85        PathProgramCache]: Analyzing trace with hash 879156031, now seen corresponding path program 1 times
[2025-04-28 21:21:43,595 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,595 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1105763302]
[2025-04-28 21:21:43,596 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,596 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,647 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:43,794 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:43,794 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,795 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:43,795 INFO  L348             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2025-04-28 21:21:43,806 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:43,864 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:43,864 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,864 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:43,887 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2025-04-28 21:21:43,889 INFO  L340         BasicCegarLoop]: Counterexample is feasible
[2025-04-28 21:21:43,890 INFO  L790   garLoopResultBuilder]: Registering result UNSAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:43,892 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:43,897 INFO  L422         BasicCegarLoop]: Path program histogram: [1]
[2025-04-28 21:21:43,909 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:43,913 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:43 BoogieIcfgContainer
[2025-04-28 21:21:43,913 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:43,914 INFO  L158              Benchmark]: Toolchain (without parser) took 1089.34ms. Allocated memory is still 234.9MB. Free memory was 147.2MB in the beginning and 91.0MB in the end (delta: 56.2MB). Peak memory consumption was 50.3MB. Max. memory is 33.6GB.
[2025-04-28 21:21:43,915 INFO  L158              Benchmark]: SmtParser took 0.36ms. Allocated memory is still 234.9MB. Free memory is still 170.6MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:43,915 INFO  L158              Benchmark]: ChcToBoogie took 59.26ms. Allocated memory is still 234.9MB. Free memory was 147.2MB in the beginning and 143.5MB in the end (delta: 3.7MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:43,915 INFO  L158              Benchmark]: Boogie Preprocessor took 75.13ms. Allocated memory is still 234.9MB. Free memory was 143.5MB in the beginning and 141.2MB in the end (delta: 2.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:43,916 INFO  L158              Benchmark]: RCFGBuilder took 492.95ms. Allocated memory is still 234.9MB. Free memory was 141.2MB in the beginning and 110.0MB in the end (delta: 31.3MB). Peak memory consumption was 33.6MB. Max. memory is 33.6GB.
[2025-04-28 21:21:43,916 INFO  L158              Benchmark]: TraceAbstraction took 452.49ms. Allocated memory is still 234.9MB. Free memory was 109.3MB in the beginning and 91.0MB in the end (delta: 18.3MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:43,918 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.36ms. Allocated memory is still 234.9MB. Free memory is still 170.6MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 59.26ms. Allocated memory is still 234.9MB. Free memory was 147.2MB in the beginning and 143.5MB in the end (delta: 3.7MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 75.13ms. Allocated memory is still 234.9MB. Free memory was 143.5MB in the beginning and 141.2MB in the end (delta: 2.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 492.95ms. Allocated memory is still 234.9MB. Free memory was 141.2MB in the beginning and 110.0MB in the end (delta: 31.3MB). Peak memory consumption was 33.6MB. Max. memory is 33.6GB.
 * TraceAbstraction took 452.49ms. Allocated memory is still 234.9MB. Free memory was 109.3MB in the beginning and 91.0MB in the end (delta: 18.3MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - CounterExampleResult [Unknown line] : the set of constraint Horn clauses is unsatisfiable
    the set of constraint Horn clauses is unsatisfiable
We found a FailurePath: 
[L0]  CALL  call False();
[L0]  CALL  call main.ATprecall.split();
[L0]        assume (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((!((((hbv_main.ATprecall.split_K2_58 || hbv_main.ATprecall.split_A2_76) && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_J2_38) && (!hbv_main.ATprecall.split_A2_76 || !hbv_main.ATprecall.split_K2_58)) && !(hbv_main.ATprecall.split_P_67 && (!hbv_main.ATprecall.split_P_67 || !hbv_main.ATprecall.split_R_74))) && !(hbv_main.ATprecall.split_J2_38 && hbv_main.ATprecall.split_Z1_82 != hbv_main.ATprecall.split_D3_25 + 400 * hbv_main.ATprecall.split_C3_7 + 24)) && !((hbv_main.ATprecall.split_P2_103 <= 0 && hbv_main.ATprecall.split_Z2_17) && 0 < hbv_main.ATprecall.split_D3_25)) && !((hbv_main.ATprecall.split_Z1_82 <= 0 && hbv_main.ATprecall.split_J2_38) && 0 < hbv_main.ATprecall.split_D3_25)) && !((hbv_main.ATprecall.split_N_12 && hbv_main.ATprecall.split_O_13) && hbv_main.ATprecall.split_L_14)) && !(hbv_main.ATprecall.split_D3_25 <= 0 && hbv_main.ATprecall.split_Q3_21)) && !(hbv_main.ATprecall.split_J_50 && 6 + hbv_main.ATprecall.split_C3_7 != hbv_main.ATprecall.split_H_93)) && !((hbv_main.ATprecall.split_X2_26 != hbv_main.ATprecall.split_Y2_27 && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_X3_4)) && !!hbv_main.ATprecall.split_G4_88) && !((hbv_main.ATprecall.split_X3_4 && hbv_main.ATprecall.split_C4_11) && hbv_main.ATprecall.split_W3_60 != hbv_main.ATprecall.split_I3_61)) && !((((hbv_main.ATprecall.split_J3_23 || hbv_main.ATprecall.split_A3_24) && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_X3_4) && (!hbv_main.ATprecall.split_J3_23 || !hbv_main.ATprecall.split_A3_24))) && !(((hbv_main.ATprecall.split_Q_100 || hbv_main.ATprecall.split_C3_7 == 1) && hbv_main.ATprecall.split_P_67) && (!hbv_main.ATprecall.split_Q_100 || hbv_main.ATprecall.split_C3_7 != 1))) && !(hbv_main.ATprecall.split_P_67 && hbv_main.ATprecall.split_V_54 != hbv_main.ATprecall.split_D3_25 + 8 + 400 * hbv_main.ATprecall.split_C3_7)) && !((hbv_main.ATprecall.split_N_12 && hbv_main.ATprecall.split_I1_83 <= 0) && 0 < hbv_main.ATprecall.split_D3_25)) && !(hbv_main.ATprecall.split_X3_4 && 40 + hbv_main.ATprecall.split_D3_25 + 400 * hbv_main.ATprecall.split_C3_7 != hbv_main.ATprecall.split_I3_61)) && !((hbv_main.ATprecall.split_J_50 && (!hbv_main.ATprecall.split_K_78 || hbv_main.ATprecall.split_C3_7 != 4)) && (hbv_main.ATprecall.split_C3_7 == 4 || hbv_main.ATprecall.split_K_78))) && !((!hbv_main.ATprecall.split_P_67 || !hbv_main.ATprecall.split_N_12) && hbv_main.ATprecall.split_N_12)) && !((hbv_main.ATprecall.split_O1_37 != hbv_main.ATprecall.split_I1_83 && hbv_main.ATprecall.split_J2_38) && hbv_main.ATprecall.split_N1_31)) && !((hbv_main.ATprecall.split_C3_7 != 0 || !hbv_main.ATprecall.split_S_73) && (hbv_main.ATprecall.split_S_73 || hbv_main.ATprecall.split_C3_7 == 0))) && !((hbv_main.ATprecall.split_R_74 && hbv_main.ATprecall.split_S_73) && hbv_main.ATprecall.split_P_67)) && !((hbv_main.ATprecall.split_L3_96 != hbv_main.ATprecall.split_G3_86 && hbv_main.ATprecall.split_M3_40) && hbv_main.ATprecall.split_C4_11)) && !(hbv_main.ATprecall.split_T_56 != 3 + hbv_main.ATprecall.split_C3_7 && hbv_main.ATprecall.split_D1_35)) && !((((!hbv_main.ATprecall.split_J3_23 || !hbv_main.ATprecall.split_Y3_44) && (hbv_main.ATprecall.split_Y3_44 || hbv_main.ATprecall.split_J3_23)) && hbv_main.ATprecall.split_X3_4) && hbv_main.ATprecall.split_C4_11)) && !((hbv_main.ATprecall.split_Z2_17 && hbv_main.ATprecall.split_D2_18) && hbv_main.ATprecall.split_F2_105 != hbv_main.ATprecall.split_B2_106)) && !((!hbv_main.ATprecall.split_S_73 && hbv_main.ATprecall.split_D1_35) && hbv_main.ATprecall.split_R_74)) && !(((hbv_main.ATprecall.split_M3_40 && hbv_main.ATprecall.split_C4_11) && (hbv_main.ATprecall.split_Z3_42 || hbv_main.ATprecall.split_N3_43)) && (!hbv_main.ATprecall.split_Z3_42 || !hbv_main.ATprecall.split_N3_43))) && !((hbv_main.ATprecall.split_V_54 <= 0 && hbv_main.ATprecall.split_P_67) && 0 < hbv_main.ATprecall.split_D3_25)) && !((hbv_main.ATprecall.split_A1_53 != hbv_main.ATprecall.split_V_54 && hbv_main.ATprecall.split_S1_30) && hbv_main.ATprecall.split_Z_55)) && !(hbv_main.ATprecall.split_X3_4 && hbv_main.ATprecall.split_B3_97 != 7 + hbv_main.ATprecall.split_C3_7)) && !((hbv_main.ATprecall.split_T3_9 != hbv_main.ATprecall.split_O3_20 && hbv_main.ATprecall.split_Q3_21) && hbv_main.ATprecall.split_R3_22)) && !((hbv_main.ATprecall.split_X_46 <= 0 && hbv_main.ATprecall.split_D1_35) && 0 < hbv_main.ATprecall.split_D3_25)) && !(hbv_main.ATprecall.split_Q3_21 && hbv_main.ATprecall.split_I_92 != 7 + hbv_main.ATprecall.split_C3_7)) && !((hbv_main.ATprecall.split_J_50 && 0 < hbv_main.ATprecall.split_D3_25) && hbv_main.ATprecall.split_N2_6 <= 0)) && !((hbv_main.ATprecall.split_T2_3 && hbv_main.ATprecall.split_X3_4) && hbv_main.ATprecall.split_X2_26 != hbv_main.ATprecall.split_S2_5)) && !((hbv_main.ATprecall.split_V3_84 != hbv_main.ATprecall.split_L3_96 && hbv_main.ATprecall.split_M3_40) && hbv_main.ATprecall.split_C4_11)) && 2 + hbv_main.ATprecall.split_C3_7 == hbv_main.ATprecall.split_C_8) && !((hbv_main.ATprecall.split_Q3_21 && hbv_main.ATprecall.split_R3_22) && hbv_main.ATprecall.split_S3_49)) && !((!hbv_main.ATprecall.split_O_13 && hbv_main.ATprecall.split_N1_31) && hbv_main.ATprecall.split_N_12)) && hbv_main.ATprecall.split_D3_25 + 400 * hbv_main.ATprecall.split_C3_7 == hbv_main.ATprecall.split_D_32) && !((hbv_main.ATprecall.split_F3_19 != hbv_main.ATprecall.split_K3_39 && hbv_main.ATprecall.split_M3_40) && hbv_main.ATprecall.split_C4_11)) && !((hbv_main.ATprecall.split_Y1_98 != hbv_main.ATprecall.split_G2_99 && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_J2_38)) && !((hbv_main.ATprecall.split_Z2_17 && hbv_main.ATprecall.split_X3_4) && hbv_main.ATprecall.split_V2_1 != hbv_main.ATprecall.split_W2_95)) && !((hbv_main.ATprecall.split_W1_109 != hbv_main.ATprecall.split_B2_106 && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_D2_18)) && !(((!hbv_main.ATprecall.split_O_13 || 2 != hbv_main.ATprecall.split_C3_7) && hbv_main.ATprecall.split_N_12) && (2 == hbv_main.ATprecall.split_C3_7 || hbv_main.ATprecall.split_O_13))) && !(6 + hbv_main.ATprecall.split_C3_7 != hbv_main.ATprecall.split_L2_94 && hbv_main.ATprecall.split_Z2_17)) && !(hbv_main.ATprecall.split_J_50 && 32 + hbv_main.ATprecall.split_D3_25 + 400 * hbv_main.ATprecall.split_C3_7 != hbv_main.ATprecall.split_N2_6)) && !((hbv_main.ATprecall.split_Q3_21 && 0 < hbv_main.ATprecall.split_D3_25) && hbv_main.ATprecall.split_G3_86 <= 0)) && !((hbv_main.ATprecall.split_I2_90 != hbv_main.ATprecall.split_H2_91 && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_J2_38)) && !(hbv_main.ATprecall.split_D3_25 <= 0 && hbv_main.ATprecall.split_D1_35)) && !((hbv_main.ATprecall.split_S1_30 && hbv_main.ATprecall.split_Z_55) && hbv_main.ATprecall.split_Y_62 != hbv_main.ATprecall.split_U_72)) && !((hbv_main.ATprecall.split_S1_30 && hbv_main.ATprecall.split_J2_38) && hbv_main.ATprecall.split_Q1_47 != hbv_main.ATprecall.split_P1_48)) && !((hbv_main.ATprecall.split_U3_10 != hbv_main.ATprecall.split_H3_101 && hbv_main.ATprecall.split_X3_4) && hbv_main.ATprecall.split_C4_11)) && !((((!hbv_main.ATprecall.split_A2_76 || !hbv_main.ATprecall.split_M1_80) && hbv_main.ATprecall.split_J2_38) && hbv_main.ATprecall.split_N1_31) && (hbv_main.ATprecall.split_M1_80 || hbv_main.ATprecall.split_A2_76))) && !((hbv_main.ATprecall.split_K1_41 <= 0 && hbv_main.ATprecall.split_S1_30) && 0 < hbv_main.ATprecall.split_D3_25)) && !((hbv_main.ATprecall.split_J_50 && hbv_main.ATprecall.split_L_14) && hbv_main.ATprecall.split_M_66)) && !((hbv_main.ATprecall.split_X1_15 <= 0 && hbv_main.ATprecall.split_L_14) && 0 < hbv_main.ATprecall.split_D3_25)) && !((hbv_main.ATprecall.split_Q3_21 && hbv_main.ATprecall.split_J_50) && hbv_main.ATprecall.split_K_78)) && !((hbv_main.ATprecall.split_J2_38 && (!hbv_main.ATprecall.split_J2_38 || !hbv_main.ATprecall.split_S1_30)) && (!hbv_main.ATprecall.split_J2_38 || !hbv_main.ATprecall.split_N1_31))) && !(hbv_main.ATprecall.split_L_14 && hbv_main.ATprecall.split_G_87 != 5 + hbv_main.ATprecall.split_C3_7)) && !((((!hbv_main.ATprecall.split_Q3_21 || !hbv_main.ATprecall.split_R3_22) && hbv_main.ATprecall.split_C4_11) && (!hbv_main.ATprecall.split_M3_40 || !hbv_main.ATprecall.split_C4_11)) && (!hbv_main.ATprecall.split_X3_4 || !hbv_main.ATprecall.split_C4_11))) && !((hbv_main.ATprecall.split_S1_30 && hbv_main.ATprecall.split_D1_35) && hbv_main.ATprecall.split_B1_33 != hbv_main.ATprecall.split_C1_34)) && !((hbv_main.ATprecall.split_P3_85 != hbv_main.ATprecall.split_G3_86 && hbv_main.ATprecall.split_Q3_21) && hbv_main.ATprecall.split_R3_22)) && !((((!hbv_main.ATprecall.split_A3_24 || !hbv_main.ATprecall.split_Q2_57) && (hbv_main.ATprecall.split_Q2_57 || hbv_main.ATprecall.split_A3_24)) && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_X3_4)) && !((!hbv_main.ATprecall.split_L_14 || !hbv_main.ATprecall.split_N_12) && hbv_main.ATprecall.split_L_14)) && !(32 + hbv_main.ATprecall.split_D3_25 + 400 * hbv_main.ATprecall.split_C3_7 != hbv_main.ATprecall.split_P2_103 && hbv_main.ATprecall.split_Z2_17)) && !((hbv_main.ATprecall.split_H1_68 != hbv_main.ATprecall.split_L1_69 && hbv_main.ATprecall.split_J2_38) && hbv_main.ATprecall.split_N1_31)) && !(hbv_main.ATprecall.split_F4_52 && !hbv_main.ATprecall.split_E4_102)) && !((hbv_main.ATprecall.split_Z2_17 && hbv_main.ATprecall.split_D2_18) && hbv_main.ATprecall.split_X1_15 != hbv_main.ATprecall.split_C2_16)) && !((hbv_main.ATprecall.split_M3_40 && hbv_main.ATprecall.split_N3_43) && hbv_main.ATprecall.split_C4_11)) && !(hbv_main.ATprecall.split_F4_52 && (!hbv_main.ATprecall.split_F4_52 || !hbv_main.ATprecall.split_C4_11))) && !(hbv_main.ATprecall.split_D_32 <= 0 && 0 < hbv_main.ATprecall.split_D3_25)) && !(hbv_main.ATprecall.split_D3_25 <= 0 && hbv_main.ATprecall.split_N_12)) && !(hbv_main.ATprecall.split_C3_7 + 4 != hbv_main.ATprecall.split_F_28 && hbv_main.ATprecall.split_N_12)) && !((!hbv_main.ATprecall.split_J_50 || !hbv_main.ATprecall.split_L_14) && hbv_main.ATprecall.split_J_50)) && !(hbv_main.ATprecall.split_D3_25 <= 0 && hbv_main.ATprecall.split_J_50)) && !((hbv_main.ATprecall.split_F2_105 != hbv_main.ATprecall.split_G2_99 && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_J2_38)) && !(((!hbv_main.ATprecall.split_J2_38 || !hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_Z2_17) && (!hbv_main.ATprecall.split_D2_18 || !hbv_main.ATprecall.split_Z2_17))) && !((!hbv_main.ATprecall.split_J_50 || !hbv_main.ATprecall.split_T2_3) && hbv_main.ATprecall.split_T2_3)) && !((((hbv_main.ATprecall.split_D4_70 || hbv_main.ATprecall.split_E4_102) && hbv_main.ATprecall.split_C4_11) && hbv_main.ATprecall.split_F4_52) && (!hbv_main.ATprecall.split_D4_70 || !hbv_main.ATprecall.split_E4_102))) && !((hbv_main.ATprecall.split_X3_4 && hbv_main.ATprecall.split_C4_11) && hbv_main.ATprecall.split_V3_84 != hbv_main.ATprecall.split_W3_60)) && !((hbv_main.ATprecall.split_N_12 && hbv_main.ATprecall.split_P_67) && hbv_main.ATprecall.split_Q_100)) && !(hbv_main.ATprecall.split_C3_7 + 4 != hbv_main.ATprecall.split_G1_29 && hbv_main.ATprecall.split_S1_30)) && !(hbv_main.ATprecall.split_D3_25 <= 0 && hbv_main.ATprecall.split_P_67)) && !((hbv_main.ATprecall.split_Z2_17 && hbv_main.ATprecall.split_X3_4) && hbv_main.ATprecall.split_W2_95 != hbv_main.ATprecall.split_O2_110)) && !((hbv_main.ATprecall.split_A4_51 && hbv_main.ATprecall.split_C4_11) && hbv_main.ATprecall.split_F4_52)) && !((!hbv_main.ATprecall.split_K_78 && hbv_main.ATprecall.split_T2_3) && hbv_main.ATprecall.split_J_50)) && !(hbv_main.ATprecall.split_D1_35 && hbv_main.ATprecall.split_X_46 != hbv_main.ATprecall.split_D3_25 + 8 + 400 * hbv_main.ATprecall.split_C3_7)) && !((hbv_main.ATprecall.split_F3_19 != hbv_main.ATprecall.split_O3_20 && hbv_main.ATprecall.split_Q3_21) && hbv_main.ATprecall.split_R3_22)) && !((hbv_main.ATprecall.split_E1_81 != hbv_main.ATprecall.split_A1_53 && hbv_main.ATprecall.split_S1_30) && hbv_main.ATprecall.split_Z_55)) && !((((hbv_main.ATprecall.split_Z3_42 || hbv_main.ATprecall.split_S3_49) && hbv_main.ATprecall.split_Q3_21) && hbv_main.ATprecall.split_R3_22) && (!hbv_main.ATprecall.split_S3_49 || !hbv_main.ATprecall.split_Z3_42))) && !((hbv_main.ATprecall.split_J2_38 && hbv_main.ATprecall.split_N1_31) && hbv_main.ATprecall.split_P1_48 != hbv_main.ATprecall.split_L1_69)) && !(hbv_main.ATprecall.split_N_12 && 16 + hbv_main.ATprecall.split_D3_25 + 400 * hbv_main.ATprecall.split_C3_7 != hbv_main.ATprecall.split_I1_83)) && !((hbv_main.ATprecall.split_U1_59 != hbv_main.ATprecall.split_K1_41 && hbv_main.ATprecall.split_S1_30) && hbv_main.ATprecall.split_J2_38)) && !((hbv_main.ATprecall.split_H2_91 != hbv_main.ATprecall.split_C2_16 && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_D2_18)) && !((((hbv_main.ATprecall.split_R1_63 || hbv_main.ATprecall.split_A2_76) && hbv_main.ATprecall.split_S1_30) && hbv_main.ATprecall.split_J2_38) && (!hbv_main.ATprecall.split_R1_63 || !hbv_main.ATprecall.split_A2_76))) && !(!hbv_main.ATprecall.split_Q3_21 && hbv_main.ATprecall.split_R3_22)) && !(hbv_main.ATprecall.split_D3_25 <= 0 && hbv_main.ATprecall.split_L_14)) && !((!hbv_main.ATprecall.split_N1_31 || !hbv_main.ATprecall.split_N_12) && hbv_main.ATprecall.split_N1_31)) && !(6 <= hbv_main.ATprecall.split_C3_7 && hbv_main.ATprecall.split_B_107)) && !(hbv_main.ATprecall.split_V1_77 != 5 + hbv_main.ATprecall.split_C3_7 && hbv_main.ATprecall.split_J2_38)) && !((hbv_main.ATprecall.split_B1_33 != hbv_main.ATprecall.split_Y_62 && hbv_main.ATprecall.split_S1_30) && hbv_main.ATprecall.split_Z_55)) && !((hbv_main.ATprecall.split_V2_1 != hbv_main.ATprecall.split_R2_2 && hbv_main.ATprecall.split_T2_3) && hbv_main.ATprecall.split_X3_4)) && !(hbv_main.ATprecall.split_G4_88 && (!hbv_main.ATprecall.split_F4_52 || !hbv_main.ATprecall.split_G4_88))) && !((hbv_main.ATprecall.split_R1_63 && hbv_main.ATprecall.split_S1_30) && hbv_main.ATprecall.split_J2_38)) && !((((!hbv_main.ATprecall.split_Q2_57 || !hbv_main.ATprecall.split_K2_58) && (hbv_main.ATprecall.split_Q2_57 || hbv_main.ATprecall.split_K2_58)) && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_J2_38)) && !(((hbv_main.ATprecall.split_E3_75 || 5 == hbv_main.ATprecall.split_C3_7) && hbv_main.ATprecall.split_Q3_21) && (5 != hbv_main.ATprecall.split_C3_7 || !hbv_main.ATprecall.split_E3_75))) && !(hbv_main.ATprecall.split_M3_40 && (!hbv_main.ATprecall.split_M3_40 || !hbv_main.ATprecall.split_Q3_21))) && !((hbv_main.ATprecall.split_T2_3 && hbv_main.ATprecall.split_U2_65) && hbv_main.ATprecall.split_X3_4)) && !((hbv_main.ATprecall.split_Q3_21 && hbv_main.ATprecall.split_R3_22) && hbv_main.ATprecall.split_E3_75)) && !((!hbv_main.ATprecall.split_M_66 && hbv_main.ATprecall.split_D2_18) && hbv_main.ATprecall.split_L_14)) && !((hbv_main.ATprecall.split_Q1_47 != hbv_main.ATprecall.split_J1_64 && hbv_main.ATprecall.split_S1_30) && hbv_main.ATprecall.split_J2_38)) && !((((hbv_main.ATprecall.split_U2_65 || hbv_main.ATprecall.split_J3_23) && (!hbv_main.ATprecall.split_J3_23 || !hbv_main.ATprecall.split_U2_65)) && hbv_main.ATprecall.split_T2_3) && hbv_main.ATprecall.split_X3_4)) && !(hbv_main.ATprecall.split_Z_55 && (!hbv_main.ATprecall.split_P_67 || !hbv_main.ATprecall.split_Z_55))) && !!hbv_main.ATprecall.split_B_107) && !(((!hbv_main.ATprecall.split_S1_30 || !hbv_main.ATprecall.split_Z_55) && hbv_main.ATprecall.split_S1_30) && (!hbv_main.ATprecall.split_S1_30 || !hbv_main.ATprecall.split_D1_35))) && !((hbv_main.ATprecall.split_Q3_21 && hbv_main.ATprecall.split_M3_40) && !hbv_main.ATprecall.split_E3_75)) && !(hbv_main.ATprecall.split_Q3_21 && (!hbv_main.ATprecall.split_J_50 || !hbv_main.ATprecall.split_Q3_21))) && !(!hbv_main.ATprecall.split_B_107 && hbv_main.ATprecall.split_C3_7 < 6)) && !((hbv_main.ATprecall.split_R2_2 != hbv_main.ATprecall.split_M2_104 && hbv_main.ATprecall.split_T2_3) && hbv_main.ATprecall.split_X3_4)) && !((hbv_main.ATprecall.split_L_14 && (3 == hbv_main.ATprecall.split_C3_7 || hbv_main.ATprecall.split_M_66)) && (!hbv_main.ATprecall.split_M_66 || 3 != hbv_main.ATprecall.split_C3_7))) && !((hbv_main.ATprecall.split_T3_9 != hbv_main.ATprecall.split_K3_39 && hbv_main.ATprecall.split_M3_40) && hbv_main.ATprecall.split_C4_11)) && !(hbv_main.ATprecall.split_X1_15 != hbv_main.ATprecall.split_D3_25 + 400 * hbv_main.ATprecall.split_C3_7 + 24 && hbv_main.ATprecall.split_L_14)) && !((!hbv_main.ATprecall.split_L_14 || !hbv_main.ATprecall.split_D2_18) && hbv_main.ATprecall.split_D2_18)) && !((((!hbv_main.ATprecall.split_E2_79 || !hbv_main.ATprecall.split_Q2_57) && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_D2_18) && (hbv_main.ATprecall.split_Q2_57 || hbv_main.ATprecall.split_E2_79))) && !(((!hbv_main.ATprecall.split_X3_4 || !hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_X3_4) && (!hbv_main.ATprecall.split_T2_3 || !hbv_main.ATprecall.split_X3_4))) && !((hbv_main.ATprecall.split_F1_45 != hbv_main.ATprecall.split_X_46 && hbv_main.ATprecall.split_S1_30) && hbv_main.ATprecall.split_D1_35)) && !((((!hbv_main.ATprecall.split_D4_70 || !hbv_main.ATprecall.split_B4_71) && hbv_main.ATprecall.split_C4_11) && hbv_main.ATprecall.split_F4_52) && (hbv_main.ATprecall.split_B4_71 || hbv_main.ATprecall.split_D4_70))) && !(((hbv_main.ATprecall.split_X3_4 && hbv_main.ATprecall.split_C4_11) && (!hbv_main.ATprecall.split_Y3_44 || !hbv_main.ATprecall.split_Z3_42)) && (hbv_main.ATprecall.split_Z3_42 || hbv_main.ATprecall.split_Y3_44))) && !((hbv_main.ATprecall.split_T2_3 && hbv_main.ATprecall.split_X3_4) && hbv_main.ATprecall.split_S2_5 != hbv_main.ATprecall.split_N2_6)) && !(16 + hbv_main.ATprecall.split_D3_25 + 400 * hbv_main.ATprecall.split_C3_7 != hbv_main.ATprecall.split_K1_41 && hbv_main.ATprecall.split_S1_30)) && !((hbv_main.ATprecall.split_J2_38 && hbv_main.ATprecall.split_N1_31) && !hbv_main.ATprecall.split_M1_80)) && !(40 + hbv_main.ATprecall.split_D3_25 + 400 * hbv_main.ATprecall.split_C3_7 != hbv_main.ATprecall.split_G3_86 && hbv_main.ATprecall.split_Q3_21)) && !((hbv_main.ATprecall.split_X3_4 && hbv_main.ATprecall.split_C4_11) && hbv_main.ATprecall.split_T3_9 != hbv_main.ATprecall.split_U3_10)) && !((hbv_main.ATprecall.split_Z_55 && hbv_main.ATprecall.split_P_67) && !hbv_main.ATprecall.split_Q_100)) && !((hbv_main.ATprecall.split_S1_30 && hbv_main.ATprecall.split_D1_35) && hbv_main.ATprecall.split_C1_34 != hbv_main.ATprecall.split_W_108)) && !(hbv_main.ATprecall.split_C4_11 && ((!hbv_main.ATprecall.split_B4_71 && !hbv_main.ATprecall.split_Z3_42) || (hbv_main.ATprecall.split_Z3_42 && hbv_main.ATprecall.split_B4_71)))) && !((hbv_main.ATprecall.split_V3_84 != hbv_main.ATprecall.split_P3_85 && hbv_main.ATprecall.split_Q3_21) && hbv_main.ATprecall.split_R3_22)) && !((!hbv_main.ATprecall.split_R_74 || !hbv_main.ATprecall.split_D1_35) && hbv_main.ATprecall.split_D1_35)) && !(hbv_main.ATprecall.split_E_89 != 3 + hbv_main.ATprecall.split_C3_7 && hbv_main.ATprecall.split_P_67)) && !((hbv_main.ATprecall.split_I3_61 <= 0 && hbv_main.ATprecall.split_X3_4) && 0 < hbv_main.ATprecall.split_D3_25)) && !((hbv_main.ATprecall.split_Z1_82 != hbv_main.ATprecall.split_I2_90 && hbv_main.ATprecall.split_Z2_17) && hbv_main.ATprecall.split_J2_38)) && !((hbv_main.ATprecall.split_Z2_17 && hbv_main.ATprecall.split_D2_18) && hbv_main.ATprecall.split_E2_79)) && !((hbv_main.ATprecall.split_Z2_17 && hbv_main.ATprecall.split_X3_4) && hbv_main.ATprecall.split_Y2_27 != hbv_main.ATprecall.split_P2_103)) && !((hbv_main.ATprecall.split_S1_30 && hbv_main.ATprecall.split_D1_35) && hbv_main.ATprecall.split_E1_81 != hbv_main.ATprecall.split_F1_45)) && !((hbv_main.ATprecall.split_T1_36 != hbv_main.ATprecall.split_U1_59 && hbv_main.ATprecall.split_S1_30) && hbv_main.ATprecall.split_J2_38)) && !((hbv_main.ATprecall.split_T1_36 != hbv_main.ATprecall.split_O1_37 && hbv_main.ATprecall.split_J2_38) && hbv_main.ATprecall.split_N1_31);
      VAL   [hbv_main.ATprecall.split_C3_7=0, hbv_main.ATprecall.split_D3_25=1]
[L0]  CALL  call main.AT_bb(hbv_main.ATprecall.split_C3_7, hbv_main.ATprecall.split_A_111, hbv_main.ATprecall.split_D3_25);
      VAL   [hhv_main.AT_bb_F_0=0, hhv_main.AT_bb_H_2=1]
[L0]        assume ((((!((hbv_main.AT_bb_C_2 && hbv_main.AT_bb_D_1) && hbv_main.AT_bb_A_5 != hbv_main.AT_bb_B_4) && !((hbv_main.AT_bb_C_2 && hbv_main.AT_bb_D_1) && hbv_main.AT_bb_E_3 != 0)) && !!hbv_main.AT_bb_C_2) && !((hbv_main.AT_bb_C_2 && hbv_main.AT_bb_D_1) && hbv_main.AT_bb_B_4 != hhv_main.AT_bb_G_1)) && !((hbv_main.AT_bb_C_2 && hbv_main.AT_bb_D_1) && hhv_main.AT_bb_F_0 != hbv_main.AT_bb_E_3)) && !((!hbv_main.AT_bb_D_1 || !hbv_main.AT_bb_C_2) && hbv_main.AT_bb_C_2);
      VAL   [hhv_main.AT_bb_F_0=0, hhv_main.AT_bb_H_2=1]
[L0]  CALL  call main.ATentry(hbv_main.AT_bb_A_5);
[L0]  RET   call main.ATentry(hbv_main.AT_bb_A_5);
      VAL   [hhv_main.AT_bb_F_0=0, hhv_main.AT_bb_H_2=1]
[L0]  RET   call main.AT_bb(hbv_main.ATprecall.split_C3_7, hbv_main.ATprecall.split_A_111, hbv_main.ATprecall.split_D3_25);
      VAL   [hbv_main.ATprecall.split_C3_7=0, hbv_main.ATprecall.split_D3_25=1]
[L0]  RET   call main.ATprecall.split();
[L0]  RET   call False();
[L0]        assert false;

  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 5 procedures, 19 locations, 25 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 0.4s, OverallIterations: 1, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: , PredicateUnifierStatistics: No data available, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=19occurred in iteration=0, InterpolantAutomatonStates: 0, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 0.0s InterpolantComputationTime, 15 NumberOfCodeBlocks, 15 NumberOfCodeBlocksAsserted, 1 NumberOfCheckSat, 0 ConstructedInterpolants, 0 QuantifiedInterpolants, 0 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 0 InterpolantComputations, 0 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
RESULT: Ultimate proved your program to be incorrect!
[2025-04-28 21:21:43,936 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
unsat
