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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:09,824 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:09,918 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9546b508-18e5-44cc-b180-a1c4f8120c15/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:09,926 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:09,927 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:09,950 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:09,951 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:09,951 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:09,951 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:09,951 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:09,952 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:09,952 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:09,952 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:09,952 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:09,952 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:09,952 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:09,952 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:09,953 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:09,953 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:09,953 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:09,953 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:09,953 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:09,953 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:09,953 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:09,953 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:09,954 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:09,954 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:10,265 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:10,277 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:10,280 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:10,283 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:10,284 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:10,286 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9546b508-18e5-44cc-b180-a1c4f8120c15/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-011.smt2
[2025-04-28 21:21:10,288 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:10,291 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:10,698 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9546b508-18e5-44cc-b180-a1c4f8120c15/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-011.smt2
[2025-04-28 21:21:10,702 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:10,705 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:10,706 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:10,706 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:10,707 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:10,710 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,762 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10 Unit
[2025-04-28 21:21:10,762 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:10,764 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:10,764 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:10,765 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:10,787 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,787 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,828 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,828 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,842 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,843 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,849 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,851 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,855 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,884 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:10,885 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:10,885 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:10,885 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:10,890 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (1/1) ...
[2025-04-28 21:21:10,892 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:10,909 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:10,925 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:10,929 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:10,941 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:10,941 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:10,941 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:10,941 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATprecall.split given in one single declaration
[2025-04-28 21:21:10,942 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATprecall.split
[2025-04-28 21:21:10,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATprecall.split
[2025-04-28 21:21:10,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT_bb3 given in one single declaration
[2025-04-28 21:21:10,942 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT_bb3
[2025-04-28 21:21:10,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT_bb3
[2025-04-28 21:21:10,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT.lr.ph.us given in one single declaration
[2025-04-28 21:21:10,942 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT.lr.ph.us
[2025-04-28 21:21:10,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT.lr.ph.us
[2025-04-28 21:21:10,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT_bb1 given in one single declaration
[2025-04-28 21:21:10,942 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT_bb1
[2025-04-28 21:21:10,943 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT_bb1
[2025-04-28 21:21:10,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT.lr.ph5.us given in one single declaration
[2025-04-28 21:21:10,943 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT.lr.ph5.us
[2025-04-28 21:21:10,943 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT.lr.ph5.us
[2025-04-28 21:21:10,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:10,943 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:10,943 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:10,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:10,943 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:10,944 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:11,055 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:11,057 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:11,344 INFO  L?                        ?]: Removed 136 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:11,344 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:11,359 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:11,359 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:11,359 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:11 BoogieIcfgContainer
[2025-04-28 21:21:11,360 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:11,364 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:11,364 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:11,368 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:11,369 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:10" (1/3) ...
[2025-04-28 21:21:11,370 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4053b3b7 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:11, skipping insertion in model container
[2025-04-28 21:21:11,370 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:10" (2/3) ...
[2025-04-28 21:21:11,370 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4053b3b7 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:11, skipping insertion in model container
[2025-04-28 21:21:11,371 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:11" (3/3) ...
[2025-04-28 21:21:11,372 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:11,392 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:11,396 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 8 procedures, 35 locations, 56 edges, 8 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:11,449 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:11,470 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;@70cd7e12, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:11,470 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:11,477 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 35 states, 14 states have (on average 1.4285714285714286) internal successors, (20), 20 states have internal predecessors, (20), 12 states have call successors, (12), 7 states have call predecessors, (12), 7 states have return successors, (12), 7 states have call predecessors, (12), 12 states have call successors, (12)
[2025-04-28 21:21:11,487 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:11,487 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:11,488 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:11,489 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:11,495 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:11,496 INFO  L85        PathProgramCache]: Analyzing trace with hash 1874170286, now seen corresponding path program 1 times
[2025-04-28 21:21:11,506 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:11,506 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [134997603]
[2025-04-28 21:21:11,507 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:11,507 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:11,550 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:11,588 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:11,589 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:11,589 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:12,048 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:12,050 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:12,051 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [134997603]
[2025-04-28 21:21:12,051 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [134997603] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:12,052 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:12,055 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:12,056 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [240279927]
[2025-04-28 21:21:12,057 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:12,061 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:12,061 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:12,085 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:12,086 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:12,088 INFO  L87              Difference]: Start difference. First operand  has 35 states, 14 states have (on average 1.4285714285714286) internal successors, (20), 20 states have internal predecessors, (20), 12 states have call successors, (12), 7 states have call predecessors, (12), 7 states have return successors, (12), 7 states have call predecessors, (12), 12 states have call successors, (12) Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:12,158 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:12,158 INFO  L93              Difference]: Finished difference Result 35 states and 43 transitions.
[2025-04-28 21:21:12,159 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:12,161 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 19
[2025-04-28 21:21:12,161 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:12,208 INFO  L225             Difference]: With dead ends: 35
[2025-04-28 21:21:12,208 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:12,210 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:12,215 INFO  L437           NwaCegarLoop]: 39 mSDtfsCounter, 1 mSDsluCounter, 68 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 107 SdHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:12,219 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 107 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:12,242 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:12,296 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:21:12,298 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 13 states have (on average 1.3076923076923077) internal successors, (17), 17 states have internal predecessors, (17), 11 states have call successors, (11), 7 states have call predecessors, (11), 7 states have return successors, (11), 7 states have call predecessors, (11), 11 states have call successors, (11)
[2025-04-28 21:21:12,306 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 39 transitions.
[2025-04-28 21:21:12,308 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 39 transitions. Word has length 19
[2025-04-28 21:21:12,308 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:12,308 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 39 transitions.
[2025-04-28 21:21:12,308 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:12,308 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 39 transitions.
[2025-04-28 21:21:12,311 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 28
[2025-04-28 21:21:12,311 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:12,311 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:12,311 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:12,311 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:12,313 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:12,313 INFO  L85        PathProgramCache]: Analyzing trace with hash -1049984459, now seen corresponding path program 1 times
[2025-04-28 21:21:12,313 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:12,313 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [855214186]
[2025-04-28 21:21:12,313 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:12,313 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:12,331 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 27 statements into 1 equivalence classes.
[2025-04-28 21:21:12,389 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:12,390 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:12,390 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:12,390 INFO  L348             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2025-04-28 21:21:12,405 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 27 statements into 1 equivalence classes.
[2025-04-28 21:21:12,446 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:12,447 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:12,447 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:12,484 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2025-04-28 21:21:12,485 INFO  L340         BasicCegarLoop]: Counterexample is feasible
[2025-04-28 21:21:12,487 INFO  L790   garLoopResultBuilder]: Registering result UNSAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:12,500 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:12,504 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1]
[2025-04-28 21:21:12,522 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:12,531 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:12 BoogieIcfgContainer
[2025-04-28 21:21:12,531 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:12,532 INFO  L158              Benchmark]: Toolchain (without parser) took 1827.79ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 153.4MB in the beginning and 127.1MB in the end (delta: 26.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:12,532 INFO  L158              Benchmark]: SmtParser took 1.77ms. Allocated memory is still 234.9MB. Free memory is still 171.5MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:12,532 INFO  L158              Benchmark]: ChcToBoogie took 56.88ms. Allocated memory is still 234.9MB. Free memory was 153.4MB in the beginning and 151.1MB in the end (delta: 2.3MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:12,533 INFO  L158              Benchmark]: Boogie Preprocessor took 120.13ms. Allocated memory is still 234.9MB. Free memory was 151.1MB in the beginning and 148.2MB in the end (delta: 2.8MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:12,533 INFO  L158              Benchmark]: RCFGBuilder took 475.98ms. Allocated memory is still 234.9MB. Free memory was 148.2MB in the beginning and 127.2MB in the end (delta: 21.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:12,533 INFO  L158              Benchmark]: TraceAbstraction took 1166.88ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 126.6MB in the beginning and 127.1MB in the end (delta: -488.4kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:12,535 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 1.77ms. Allocated memory is still 234.9MB. Free memory is still 171.5MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 56.88ms. Allocated memory is still 234.9MB. Free memory was 153.4MB in the beginning and 151.1MB in the end (delta: 2.3MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 120.13ms. Allocated memory is still 234.9MB. Free memory was 151.1MB in the beginning and 148.2MB in the end (delta: 2.8MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 475.98ms. Allocated memory is still 234.9MB. Free memory was 148.2MB in the beginning and 127.2MB in the end (delta: 21.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 1166.88ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 126.6MB in the beginning and 127.1MB in the end (delta: -488.4kB). There was no memory consumed. 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_J_3 == hbv_main.ATprecall.split_H_6[hbv_main.ATprecall.split_I_7] && !(!hbv_main.ATprecall.split_L_5 && !hbv_main.ATprecall.split_N_14)) && !(hbv_main.ATprecall.split_L_5 && hbv_main.ATprecall.split_K_4 <= hbv_main.ATprecall.split_J_3)) && !(hbv_main.ATprecall.split_G_8 <= 0)) && hbv_main.ATprecall.split_F_11 * 4 + hbv_main.ATprecall.split_G_8 == hbv_main.ATprecall.split_I_7) && !(0 < hbv_main.ATprecall.split_G_8 && hbv_main.ATprecall.split_I_7 <= 0)) && hbv_main.ATprecall.split_F_11 == hbv_main.ATprecall.split_E_9 + hbv_main.ATprecall.split_D_10) && !((((hbv_main.ATprecall.split_P_13 || hbv_main.ATprecall.split_Q_2) && (!hbv_main.ATprecall.split_P_13 || !hbv_main.ATprecall.split_Q_2)) && hbv_main.ATprecall.split_O_15) && hbv_main.ATprecall.split_R_1)) && !(!hbv_main.ATprecall.split_L_5 && hbv_main.ATprecall.split_J_3 < hbv_main.ATprecall.split_K_4)) && !(hbv_main.ATprecall.split_S_12 && (!hbv_main.ATprecall.split_S_12 || !hbv_main.ATprecall.split_R_1))) && !(hbv_main.ATprecall.split_R_1 && !hbv_main.ATprecall.split_Q_2)) && !((hbv_main.ATprecall.split_O_15 && hbv_main.ATprecall.split_M_16) && hbv_main.ATprecall.split_R_1)) && !(hbv_main.ATprecall.split_N_14 && hbv_main.ATprecall.split_L_5)) && !!hbv_main.ATprecall.split_S_12) && !((!hbv_main.ATprecall.split_O_15 || !hbv_main.ATprecall.split_R_1) && hbv_main.ATprecall.split_R_1)) && !((((!hbv_main.ATprecall.split_P_13 || !hbv_main.ATprecall.split_N_14) && (hbv_main.ATprecall.split_N_14 || hbv_main.ATprecall.split_P_13)) && hbv_main.ATprecall.split_O_15) && hbv_main.ATprecall.split_R_1);
      VAL   [hbv_main.ATprecall.split_D_10=0, hbv_main.ATprecall.split_E_9=1, hbv_main.ATprecall.split_G_8=1, hbv_main.ATprecall.split_K_4=0]
[L0]  CALL  call main.AT_bb3(hbv_main.ATprecall.split_A_17, hbv_main.ATprecall.split_B_18, hbv_main.ATprecall.split_D_10, hbv_main.ATprecall.split_C_19, hbv_main.ATprecall.split_E_9, hbv_main.ATprecall.split_G_8, hbv_main.ATprecall.split_H_6, hbv_main.ATprecall.split_K_4);
      VAL   [hhv_main.AT_bb3_E_0=1, hhv_main.AT_bb3_F_1=0, hhv_main.AT_bb3_G_2=0, hhv_main.AT_bb3_H_3=1, hhv_main.AT_bb3_I_4=1, hhv_main.AT_bb3_J_5=1, hhv_main.AT_bb3_L_7=0]
[L0]        assume ((((!((hbv_main.AT_bb3_B_2 && hbv_main.AT_bb3_C_3) && hhv_main.AT_bb3_G_2 != hbv_main.AT_bb3_D_4) && !!hbv_main.AT_bb3_B_2) && !(((((hhv_main.AT_bb3_F_1 < 0 || hhv_main.AT_bb3_F_1 < hhv_main.AT_bb3_E_0) || hhv_main.AT_bb3_E_0 < 0) && (0 <= hhv_main.AT_bb3_F_1 || (hhv_main.AT_bb3_F_1 < hhv_main.AT_bb3_E_0 && hhv_main.AT_bb3_E_0 < 0))) || hbv_main.AT_bb3_A_1) && (((hhv_main.AT_bb3_F_1 < 0 && (hhv_main.AT_bb3_E_0 <= hhv_main.AT_bb3_F_1 || 0 <= hhv_main.AT_bb3_E_0)) || !hbv_main.AT_bb3_A_1) || ((hhv_main.AT_bb3_E_0 <= hhv_main.AT_bb3_F_1 && 0 <= hhv_main.AT_bb3_F_1) && 0 <= hhv_main.AT_bb3_E_0)))) && !!hbv_main.AT_bb3_A_1) && !((!hbv_main.AT_bb3_B_2 || !hbv_main.AT_bb3_C_3) && hbv_main.AT_bb3_B_2)) && !((hbv_main.AT_bb3_B_2 && hbv_main.AT_bb3_C_3) && hbv_main.AT_bb3_D_4 != 0);
      VAL   [hhv_main.AT_bb3_E_0=1, hhv_main.AT_bb3_F_1=0, hhv_main.AT_bb3_G_2=0, hhv_main.AT_bb3_H_3=1, hhv_main.AT_bb3_I_4=1, hhv_main.AT_bb3_J_5=1, hhv_main.AT_bb3_L_7=0]
[L0]  CALL  call main.AT.lr.ph.us(hhv_main.AT_bb3_E_0, hhv_main.AT_bb3_F_1, hhv_main.AT_bb3_H_3, hhv_main.AT_bb3_J_5, hhv_main.AT_bb3_K_6, hhv_main.AT_bb3_L_7);
      VAL   [hhv_main.AT.lr.ph.us_Q_0=1, hhv_main.AT.lr.ph.us_R_1=0, hhv_main.AT.lr.ph.us_S_2=1, hhv_main.AT.lr.ph.us_T_3=1, hhv_main.AT.lr.ph.us_V_5=0]
[L0]        assume ((((((((((((((((((((((((((((((((if hbv_main.AT.lr.ph.us_G_18 then hbv_main.AT.lr.ph.us_H_17 else hbv_main.AT.lr.ph.us_A_16) == hbv_main.AT.lr.ph.us_M_25 && !((hbv_main.AT.lr.ph.us_N_5 && hbv_main.AT.lr.ph.us_O_6) && hbv_main.AT.lr.ph.us_D1_7)) && !((hhv_main.AT.lr.ph.us_R_1 != hbv_main.AT.lr.ph.us_K_12 && hbv_main.AT.lr.ph.us_C1_4) && hbv_main.AT.lr.ph.us_D1_7)) && !(hhv_main.AT.lr.ph.us_T_3 <= 0)) && !((hbv_main.AT.lr.ph.us_H_13 != hbv_main.AT.lr.ph.us_U_14 && hbv_main.AT.lr.ph.us_Y_15) && hbv_main.AT.lr.ph.us_L_3)) && !!hbv_main.AT.lr.ph.us_C1_4) && !((((0 <= hbv_main.AT.lr.ph.us_K_31 || (hhv_main.AT.lr.ph.us_S_2 < 0 && hbv_main.AT.lr.ph.us_K_31 < hhv_main.AT.lr.ph.us_S_2)) && ((hhv_main.AT.lr.ph.us_S_2 < 0 || hbv_main.AT.lr.ph.us_K_31 < 0) || hbv_main.AT.lr.ph.us_K_31 < hhv_main.AT.lr.ph.us_S_2)) || hbv_main.AT.lr.ph.us_L_28) && ((((hhv_main.AT.lr.ph.us_S_2 <= hbv_main.AT.lr.ph.us_K_31 && 0 <= hhv_main.AT.lr.ph.us_S_2) && 0 <= hbv_main.AT.lr.ph.us_K_31) || !hbv_main.AT.lr.ph.us_L_28) || ((hhv_main.AT.lr.ph.us_S_2 <= hbv_main.AT.lr.ph.us_K_31 || 0 <= hhv_main.AT.lr.ph.us_S_2) && hbv_main.AT.lr.ph.us_K_31 < 0)))) && !((!hbv_main.AT.lr.ph.us_L_3 || !hbv_main.AT.lr.ph.us_N_22) && hbv_main.AT.lr.ph.us_L_3)) && hbv_main.AT.lr.ph.us_E_10 == hbv_main.AT.lr.ph.us_J_29 + hbv_main.AT.lr.ph.us_C_30) && !((hbv_main.AT.lr.ph.us_N_22 && hbv_main.AT.lr.ph.us_L_3) && hbv_main.AT.lr.ph.us_O_20 != hbv_main.AT.lr.ph.us_M_25)) && !(((hhv_main.AT.lr.ph.us_S_2 != 0 || !hbv_main.AT.lr.ph.us_O_6) && hbv_main.AT.lr.ph.us_N_5) && (hhv_main.AT.lr.ph.us_S_2 == 0 || hbv_main.AT.lr.ph.us_O_6))) && !((hbv_main.AT.lr.ph.us_Y_15 && hbv_main.AT.lr.ph.us_L_3) && hbv_main.AT.lr.ph.us_U_14 != hbv_main.AT.lr.ph.us_S_21)) && hbv_main.AT.lr.ph.us_B_8 == hbv_main.AT.lr.ph.us_A_9) && !((hbv_main.AT.lr.ph.us_Y_15 && hbv_main.AT.lr.ph.us_J_2) && hbv_main.AT.lr.ph.us_L_3)) && !((!hbv_main.AT.lr.ph.us_Y_15 || !hbv_main.AT.lr.ph.us_N_5) && hbv_main.AT.lr.ph.us_N_5)) && !(!hbv_main.AT.lr.ph.us_G_18 && hbv_main.AT.lr.ph.us_A_16 < hbv_main.AT.lr.ph.us_H_17)) && hbv_main.AT.lr.ph.us_J_29 + 1 == hbv_main.AT.lr.ph.us_K_31) && !((hbv_main.AT.lr.ph.us_Z_19 != hbv_main.AT.lr.ph.us_H_13 && hbv_main.AT.lr.ph.us_N_5) && hbv_main.AT.lr.ph.us_Y_15)) && hbv_main.AT.lr.ph.us_E_27[hbv_main.AT.lr.ph.us_D_11 := hbv_main.AT.lr.ph.us_H_17] == hbv_main.AT.lr.ph.us_V_24) && !(hbv_main.AT.lr.ph.us_D1_7 && (!hbv_main.AT.lr.ph.us_N_5 || !hbv_main.AT.lr.ph.us_D1_7))) && !((!hbv_main.AT.lr.ph.us_C1_4 || !hbv_main.AT.lr.ph.us_D1_7) && hbv_main.AT.lr.ph.us_C1_4)) && !(((((0 <= hbv_main.AT.lr.ph.us_Q_1 || (hhv_main.AT.lr.ph.us_Q_0 < 0 && hbv_main.AT.lr.ph.us_Q_1 < hhv_main.AT.lr.ph.us_Q_0)) && ((hbv_main.AT.lr.ph.us_Q_1 < 0 || hhv_main.AT.lr.ph.us_Q_0 < 0) || hbv_main.AT.lr.ph.us_Q_1 < hhv_main.AT.lr.ph.us_Q_0)) || hbv_main.AT.lr.ph.us_J_2) && hbv_main.AT.lr.ph.us_L_3) && ((((0 <= hbv_main.AT.lr.ph.us_Q_1 && 0 <= hhv_main.AT.lr.ph.us_Q_0) && hhv_main.AT.lr.ph.us_Q_0 <= hbv_main.AT.lr.ph.us_Q_1) || !hbv_main.AT.lr.ph.us_J_2) || (hbv_main.AT.lr.ph.us_Q_1 < 0 && (0 <= hhv_main.AT.lr.ph.us_Q_0 || hhv_main.AT.lr.ph.us_Q_0 <= hbv_main.AT.lr.ph.us_Q_1))))) && !((hbv_main.AT.lr.ph.us_K_12 != 0 && hbv_main.AT.lr.ph.us_C1_4) && hbv_main.AT.lr.ph.us_D1_7)) && !((hbv_main.AT.lr.ph.us_O_20 != hbv_main.AT.lr.ph.us_S_21 && hbv_main.AT.lr.ph.us_N_22) && hbv_main.AT.lr.ph.us_L_3)) && !((hhv_main.AT.lr.ph.us_U_4 != hbv_main.AT.lr.ph.us_X_23 && hbv_main.AT.lr.ph.us_N_5) && hbv_main.AT.lr.ph.us_Y_15)) && !((hbv_main.AT.lr.ph.us_X_23 != hbv_main.AT.lr.ph.us_V_24 && hbv_main.AT.lr.ph.us_N_5) && hbv_main.AT.lr.ph.us_Y_15)) && !((!hbv_main.AT.lr.ph.us_L_3 || !hbv_main.AT.lr.ph.us_Y_15) && hbv_main.AT.lr.ph.us_Y_15)) && !((hhv_main.AT.lr.ph.us_V_5 != hbv_main.AT.lr.ph.us_Z_19 && hbv_main.AT.lr.ph.us_N_5) && hbv_main.AT.lr.ph.us_Y_15)) && !(hbv_main.AT.lr.ph.us_G_18 && hbv_main.AT.lr.ph.us_H_17 <= hbv_main.AT.lr.ph.us_A_16)) && !((hbv_main.AT.lr.ph.us_N_22 && hbv_main.AT.lr.ph.us_L_28) && hbv_main.AT.lr.ph.us_L_3)) && !(0 < hhv_main.AT.lr.ph.us_T_3 && hbv_main.AT.lr.ph.us_D_11 <= 0)) && hhv_main.AT.lr.ph.us_T_3 + hbv_main.AT.lr.ph.us_E_10 * 4 == hbv_main.AT.lr.ph.us_D_11) && !(hbv_main.AT.lr.ph.us_L_3 && hbv_main.AT.lr.ph.us_Q_1 != hbv_main.AT.lr.ph.us_P_26 + 1);
      VAL   [hbv_main.AT.lr.ph.us_A_16=-1, hbv_main.AT.lr.ph.us_B_8=7, hbv_main.AT.lr.ph.us_C_30=0, hbv_main.AT.lr.ph.us_J_29=0, hbv_main.AT.lr.ph.us_P_26=0, hhv_main.AT.lr.ph.us_Q_0=1, hhv_main.AT.lr.ph.us_R_1=0, hhv_main.AT.lr.ph.us_S_2=1, hhv_main.AT.lr.ph.us_T_3=1, hhv_main.AT.lr.ph.us_V_5=0]
[L0]  CALL  call main.AT_bb1(hhv_main.AT.lr.ph.us_Q_0, hhv_main.AT.lr.ph.us_S_2, hhv_main.AT.lr.ph.us_T_3, hbv_main.AT.lr.ph.us_P_26, hbv_main.AT.lr.ph.us_B_8, hbv_main.AT.lr.ph.us_J_29, hbv_main.AT.lr.ph.us_C_30, hbv_main.AT.lr.ph.us_E_27, hbv_main.AT.lr.ph.us_A_16);
      VAL   [hhv_main.AT_bb1_H_0=1, hhv_main.AT_bb1_I_1=1, hhv_main.AT_bb1_J_2=1, hhv_main.AT_bb1_K_3=0, hhv_main.AT_bb1_L_4=7, hhv_main.AT_bb1_M_5=0, hhv_main.AT_bb1_N_6=0, hhv_main.AT_bb1_P_8=-1]
[L0]        assume ((((((!((hbv_main.AT_bb1_F_1 && hbv_main.AT_bb1_E_2) && hhv_main.AT_bb1_O_7 != hbv_main.AT_bb1_C_6) && !!hbv_main.AT_bb1_E_2) && !((hbv_main.AT_bb1_A_7 != hbv_main.AT_bb1_C_6 && hbv_main.AT_bb1_F_1) && hbv_main.AT_bb1_E_2)) && !((hhv_main.AT_bb1_M_5 != hbv_main.AT_bb1_G_3 && hbv_main.AT_bb1_F_1) && hbv_main.AT_bb1_E_2)) && !((hbv_main.AT_bb1_F_1 && hbv_main.AT_bb1_E_2) && hbv_main.AT_bb1_D_4 != hbv_main.AT_bb1_B_5)) && !((hbv_main.AT_bb1_F_1 && hbv_main.AT_bb1_E_2) && hbv_main.AT_bb1_D_4 != hhv_main.AT_bb1_P_8)) && !((hbv_main.AT_bb1_G_3 != 0 && hbv_main.AT_bb1_F_1) && hbv_main.AT_bb1_E_2)) && !(hbv_main.AT_bb1_E_2 && (!hbv_main.AT_bb1_F_1 || !hbv_main.AT_bb1_E_2));
      VAL   [hbv_main.AT_bb1_B_5=-1, hhv_main.AT_bb1_H_0=1, hhv_main.AT_bb1_I_1=1, hhv_main.AT_bb1_J_2=1, hhv_main.AT_bb1_K_3=0, hhv_main.AT_bb1_L_4=7, hhv_main.AT_bb1_M_5=0, hhv_main.AT_bb1_N_6=0, hhv_main.AT_bb1_P_8=-1]
[L0]  CALL  call main.AT.lr.ph5.us(hhv_main.AT_bb1_H_0, hhv_main.AT_bb1_I_1, hhv_main.AT_bb1_J_2, hhv_main.AT_bb1_K_3, hbv_main.AT_bb1_A_7, hbv_main.AT_bb1_B_5, hhv_main.AT_bb1_L_4);
      VAL   [hhv_main.AT.lr.ph5.us_P_0=1, hhv_main.AT.lr.ph5.us_Q_1=1, hhv_main.AT.lr.ph5.us_R_2=1, hhv_main.AT.lr.ph5.us_S_3=0, hhv_main.AT.lr.ph5.us_U_5=-1, hhv_main.AT.lr.ph5.us_V_6=7]
[L0]        assume ((((((((((((((((!((hbv_main.AT.lr.ph5.us_O_2 != hhv_main.AT.lr.ph5.us_S_3 && hbv_main.AT.lr.ph5.us_N_3) && hbv_main.AT.lr.ph5.us_M_1) && !((!hbv_main.AT.lr.ph5.us_G_5 || !hbv_main.AT.lr.ph5.us_E_14) && hbv_main.AT.lr.ph5.us_G_5)) && !((hbv_main.AT.lr.ph5.us_N_3 && hbv_main.AT.lr.ph5.us_M_1) && hbv_main.AT.lr.ph5.us_L_11 != hhv_main.AT.lr.ph5.us_U_5)) && hbv_main.AT.lr.ph5.us_C_9 == hbv_main.AT.lr.ph5.us_B_10) && !((hbv_main.AT.lr.ph5.us_O_2 != 0 && hbv_main.AT.lr.ph5.us_N_3) && hbv_main.AT.lr.ph5.us_M_1)) && !((hbv_main.AT.lr.ph5.us_N_3 && hbv_main.AT.lr.ph5.us_M_1) && hbv_main.AT.lr.ph5.us_I_6 != hbv_main.AT.lr.ph5.us_K_7)) && !(((hhv_main.AT.lr.ph5.us_Q_1 == 0 || hbv_main.AT.lr.ph5.us_H_4) && hbv_main.AT.lr.ph5.us_G_5) && (hhv_main.AT.lr.ph5.us_Q_1 != 0 || !hbv_main.AT.lr.ph5.us_H_4))) && !((hbv_main.AT.lr.ph5.us_F_13 && hbv_main.AT.lr.ph5.us_G_5) && hbv_main.AT.lr.ph5.us_E_14)) && !((hhv_main.AT.lr.ph5.us_T_4 != hbv_main.AT.lr.ph5.us_K_7 && hbv_main.AT.lr.ph5.us_N_3) && hbv_main.AT.lr.ph5.us_M_1)) && !((hbv_main.AT.lr.ph5.us_L_11 != hbv_main.AT.lr.ph5.us_J_12 && hbv_main.AT.lr.ph5.us_N_3) && hbv_main.AT.lr.ph5.us_M_1)) && !(hbv_main.AT.lr.ph5.us_M_1 && (!hbv_main.AT.lr.ph5.us_M_1 || !hbv_main.AT.lr.ph5.us_N_3))) && hbv_main.AT.lr.ph5.us_C_9 == hbv_main.AT.lr.ph5.us_A_15) && !!hbv_main.AT.lr.ph5.us_M_1) && hbv_main.AT.lr.ph5.us_D_8 == hhv_main.AT.lr.ph5.us_V_6) && !((hbv_main.AT.lr.ph5.us_F_13 || hhv_main.AT.lr.ph5.us_P_0 == 0) && (!hbv_main.AT.lr.ph5.us_F_13 || hhv_main.AT.lr.ph5.us_P_0 != 0))) && !(hbv_main.AT.lr.ph5.us_N_3 && (!hbv_main.AT.lr.ph5.us_G_5 || !hbv_main.AT.lr.ph5.us_N_3))) && !((hbv_main.AT.lr.ph5.us_H_4 && hbv_main.AT.lr.ph5.us_N_3) && hbv_main.AT.lr.ph5.us_G_5)) && !(hhv_main.AT.lr.ph5.us_R_2 <= 0);
      VAL   [hbv_main.AT.lr.ph5.us_C_9=6, hhv_main.AT.lr.ph5.us_P_0=1, hhv_main.AT.lr.ph5.us_Q_1=1, hhv_main.AT.lr.ph5.us_R_2=1, hhv_main.AT.lr.ph5.us_S_3=0, hhv_main.AT.lr.ph5.us_U_5=-1, hhv_main.AT.lr.ph5.us_V_6=7]
[L0]  CALL  call main.ATentry(hhv_main.AT.lr.ph5.us_V_6, hbv_main.AT.lr.ph5.us_C_9);
[L0]  RET   call main.ATentry(hhv_main.AT.lr.ph5.us_V_6, hbv_main.AT.lr.ph5.us_C_9);
      VAL   [hbv_main.AT.lr.ph5.us_C_9=6, hhv_main.AT.lr.ph5.us_P_0=1, hhv_main.AT.lr.ph5.us_Q_1=1, hhv_main.AT.lr.ph5.us_R_2=1, hhv_main.AT.lr.ph5.us_S_3=0, hhv_main.AT.lr.ph5.us_U_5=-1, hhv_main.AT.lr.ph5.us_V_6=7]
[L0]  RET   call main.AT.lr.ph5.us(hhv_main.AT_bb1_H_0, hhv_main.AT_bb1_I_1, hhv_main.AT_bb1_J_2, hhv_main.AT_bb1_K_3, hbv_main.AT_bb1_A_7, hbv_main.AT_bb1_B_5, hhv_main.AT_bb1_L_4);
      VAL   [hbv_main.AT_bb1_B_5=-1, hhv_main.AT_bb1_H_0=1, hhv_main.AT_bb1_I_1=1, hhv_main.AT_bb1_J_2=1, hhv_main.AT_bb1_K_3=0, hhv_main.AT_bb1_L_4=7, hhv_main.AT_bb1_M_5=0, hhv_main.AT_bb1_N_6=0, hhv_main.AT_bb1_P_8=-1]
[L0]  RET   call main.AT_bb1(hhv_main.AT.lr.ph.us_Q_0, hhv_main.AT.lr.ph.us_S_2, hhv_main.AT.lr.ph.us_T_3, hbv_main.AT.lr.ph.us_P_26, hbv_main.AT.lr.ph.us_B_8, hbv_main.AT.lr.ph.us_J_29, hbv_main.AT.lr.ph.us_C_30, hbv_main.AT.lr.ph.us_E_27, hbv_main.AT.lr.ph.us_A_16);
      VAL   [hbv_main.AT.lr.ph.us_A_16=-1, hbv_main.AT.lr.ph.us_B_8=7, hbv_main.AT.lr.ph.us_C_30=0, hbv_main.AT.lr.ph.us_J_29=0, hbv_main.AT.lr.ph.us_P_26=0, hhv_main.AT.lr.ph.us_Q_0=1, hhv_main.AT.lr.ph.us_R_1=0, hhv_main.AT.lr.ph.us_S_2=1, hhv_main.AT.lr.ph.us_T_3=1, hhv_main.AT.lr.ph.us_V_5=0]
[L0]  RET   call main.AT.lr.ph.us(hhv_main.AT_bb3_E_0, hhv_main.AT_bb3_F_1, hhv_main.AT_bb3_H_3, hhv_main.AT_bb3_J_5, hhv_main.AT_bb3_K_6, hhv_main.AT_bb3_L_7);
      VAL   [hhv_main.AT_bb3_E_0=1, hhv_main.AT_bb3_F_1=0, hhv_main.AT_bb3_G_2=0, hhv_main.AT_bb3_H_3=1, hhv_main.AT_bb3_I_4=1, hhv_main.AT_bb3_J_5=1, hhv_main.AT_bb3_L_7=0]
[L0]  RET   call main.AT_bb3(hbv_main.ATprecall.split_A_17, hbv_main.ATprecall.split_B_18, hbv_main.ATprecall.split_D_10, hbv_main.ATprecall.split_C_19, hbv_main.ATprecall.split_E_9, hbv_main.ATprecall.split_G_8, hbv_main.ATprecall.split_H_6, hbv_main.ATprecall.split_K_4);
      VAL   [hbv_main.ATprecall.split_A_17=1, hbv_main.ATprecall.split_B_18=0, hbv_main.ATprecall.split_C_19=1, hbv_main.ATprecall.split_D_10=0, hbv_main.ATprecall.split_E_9=1, hbv_main.ATprecall.split_G_8=1, hbv_main.ATprecall.split_K_4=0]
[L0]  RET   call main.ATprecall.split();
[L0]  RET   call False();
[L0]        assert false;

  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 8 procedures, 35 locations, 56 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 1.1s, OverallIterations: 2, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.2s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 2 SdHoareTripleChecker+Valid, 0.0s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 1 mSDsluCounter, 107 SdHoareTripleChecker+Invalid, 0.0s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 68 mSDsCounter, 1 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 13 IncrementalHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 1 mSolverCounterUnsat, 39 mSDtfsCounter, 13 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 5 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=35occurred in iteration=0, InterpolantAutomatonStates: 4, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 1 MinimizatonAttempts, 0 StatesRemovedByMinimization, 0 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 0.5s InterpolantComputationTime, 46 NumberOfCodeBlocks, 46 NumberOfCodeBlocksAsserted, 2 NumberOfCheckSat, 18 ConstructedInterpolants, 0 QuantifiedInterpolants, 27 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 1 InterpolantComputations, 1 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:12,555 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Forceful destruction successful, exit code 0
Received shutdown request...
unsat
