./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-012.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:14,971 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:15,035 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6ea44b24-2bb8-44da-b7be-9577fafd2bfb/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:15,040 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:15,040 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:15,073 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:15,075 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:15,076 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:15,077 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:15,077 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:15,077 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:15,078 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:15,078 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:15,078 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:15,078 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:15,078 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:15,078 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:15,078 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:15,079 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:15,079 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:15,079 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:15,079 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:15,079 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:15,079 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:15,079 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:15,080 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:15,080 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:15,421 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:15,431 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:15,434 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:15,435 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:15,436 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:15,437 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6ea44b24-2bb8-44da-b7be-9577fafd2bfb/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-012.smt2
[2025-04-28 21:21:15,438 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:15,442 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:15,648 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6ea44b24-2bb8-44da-b7be-9577fafd2bfb/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-012.smt2
[2025-04-28 21:21:15,651 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:15,653 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:15,653 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:15,653 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:15,654 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:15,656 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,685 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15 Unit
[2025-04-28 21:21:15,686 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:15,688 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,688 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:15,688 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:15,704 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,705 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,731 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,732 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,735 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,736 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,738 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,738 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,743 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,763 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,766 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:15,766 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:15,766 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:15,767 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,770 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:15,789 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:15,808 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:15,814 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:15,830 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:15,831 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:15,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:15,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry.split given in one single declaration
[2025-04-28 21:21:15,831 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry.split
[2025-04-28 21:21:15,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry.split
[2025-04-28 21:21:15,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure id given in one single declaration
[2025-04-28 21:21:15,831 INFO  L130     BoogieDeclarations]: Found specification of procedure id
[2025-04-28 21:21:15,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure id
[2025-04-28 21:21:15,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure id.ATUnifiedReturnBlock1.split given in one single declaration
[2025-04-28 21:21:15,832 INFO  L130     BoogieDeclarations]: Found specification of procedure id.ATUnifiedReturnBlock1.split
[2025-04-28 21:21:15,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure id.ATUnifiedReturnBlock1.split
[2025-04-28 21:21:15,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure id.AT_tail given in one single declaration
[2025-04-28 21:21:15,832 INFO  L130     BoogieDeclarations]: Found specification of procedure id.AT_tail
[2025-04-28 21:21:15,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure id.AT_tail
[2025-04-28 21:21:15,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:15,832 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:15,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:15,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:15,832 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:15,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:15,885 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:15,888 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:16,005 INFO  L?                        ?]: Removed 16 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:16,005 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:16,023 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:16,024 INFO  L312             CfgBuilder]: Removed 3 assume(true) statements.
[2025-04-28 21:21:16,024 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:16 BoogieIcfgContainer
[2025-04-28 21:21:16,026 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:16,032 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:16,032 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:16,038 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:16,038 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/3) ...
[2025-04-28 21:21:16,039 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5fc71597 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:16, skipping insertion in model container
[2025-04-28 21:21:16,039 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (2/3) ...
[2025-04-28 21:21:16,039 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5fc71597 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:16, skipping insertion in model container
[2025-04-28 21:21:16,039 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:16" (3/3) ...
[2025-04-28 21:21:16,041 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:16,056 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:16,059 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 26 locations, 36 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:16,102 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:16,118 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;@2518fd15, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:16,118 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:16,122 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 26 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 7 states have call successors, (7), 6 states have call predecessors, (7), 6 states have return successors, (7), 7 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:16,130 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:16,130 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,131 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:16,131 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,139 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,140 INFO  L85        PathProgramCache]: Analyzing trace with hash -1251070431, now seen corresponding path program 1 times
[2025-04-28 21:21:16,151 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,151 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1592547463]
[2025-04-28 21:21:16,151 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,152 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,178 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:16,191 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:16,192 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,192 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,280 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:16,280 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,280 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1592547463]
[2025-04-28 21:21:16,281 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1592547463] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,281 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,284 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:16,286 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [817399758]
[2025-04-28 21:21:16,286 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,290 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:16,291 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,321 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:16,322 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:16,324 INFO  L87              Difference]: Start difference. First operand  has 26 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 7 states have call successors, (7), 6 states have call predecessors, (7), 6 states have return successors, (7), 7 states have call predecessors, (7), 7 states have call successors, (7) Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:16,377 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,378 INFO  L93              Difference]: Finished difference Result 26 states and 29 transitions.
[2025-04-28 21:21:16,379 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:16,380 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 15
[2025-04-28 21:21:16,381 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,388 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:16,388 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:16,390 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 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:16,393 INFO  L437           NwaCegarLoop]: 26 mSDtfsCounter, 1 mSDsluCounter, 42 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 68 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,394 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 68 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:16,408 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:16,451 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:16,452 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 13 states have internal predecessors, (14), 7 states have call successors, (7), 6 states have call predecessors, (7), 7 states have return successors, (8), 7 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:16,461 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 29 transitions.
[2025-04-28 21:21:16,466 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 29 transitions. Word has length 15
[2025-04-28 21:21:16,467 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,467 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 29 transitions.
[2025-04-28 21:21:16,467 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:16,471 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 29 transitions.
[2025-04-28 21:21:16,472 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:16,472 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,473 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:16,473 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:16,473 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,474 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,474 INFO  L85        PathProgramCache]: Analyzing trace with hash 1052852364, now seen corresponding path program 1 times
[2025-04-28 21:21:16,476 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,476 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [169623320]
[2025-04-28 21:21:16,476 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,477 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,486 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:16,501 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:16,501 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,501 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,586 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:16,588 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,588 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [169623320]
[2025-04-28 21:21:16,588 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [169623320] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,588 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,589 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:16,589 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [722312774]
[2025-04-28 21:21:16,589 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,590 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:16,590 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,591 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:16,592 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:16,593 INFO  L87              Difference]: Start difference. First operand 26 states and 29 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:16,634 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,634 INFO  L93              Difference]: Finished difference Result 30 states and 33 transitions.
[2025-04-28 21:21:16,638 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:16,639 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 15
[2025-04-28 21:21:16,639 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,639 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:16,639 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:16,640 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 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:16,641 INFO  L437           NwaCegarLoop]: 26 mSDtfsCounter, 1 mSDsluCounter, 42 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 68 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,641 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 68 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:16,644 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:16,647 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 26.
[2025-04-28 21:21:16,648 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 12 states have internal predecessors, (14), 7 states have call successors, (7), 6 states have call predecessors, (7), 7 states have return successors, (8), 7 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:16,649 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 29 transitions.
[2025-04-28 21:21:16,649 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 29 transitions. Word has length 15
[2025-04-28 21:21:16,650 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,650 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 29 transitions.
[2025-04-28 21:21:16,650 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:16,650 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 29 transitions.
[2025-04-28 21:21:16,651 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 27
[2025-04-28 21:21:16,651 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,651 INFO  L218           NwaCegarLoop]: trace histogram [2, 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:16,651 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:16,651 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,653 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,653 INFO  L85        PathProgramCache]: Analyzing trace with hash -1524042294, now seen corresponding path program 1 times
[2025-04-28 21:21:16,653 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,654 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1180979769]
[2025-04-28 21:21:16,654 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,654 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,721 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:21:16,741 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:21:16,741 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,741 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,845 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:16,845 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,846 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1180979769]
[2025-04-28 21:21:16,846 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1180979769] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,846 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,846 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:16,846 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [242273791]
[2025-04-28 21:21:16,846 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,847 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:16,847 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,847 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:16,847 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:16,849 INFO  L87              Difference]: Start difference. First operand 26 states and 29 transitions. Second operand  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:16,871 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,872 INFO  L93              Difference]: Finished difference Result 28 states and 30 transitions.
[2025-04-28 21:21:16,873 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:16,873 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7) Word has length 26
[2025-04-28 21:21:16,873 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,874 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:16,874 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:16,874 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 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:16,875 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 1 mSDsluCounter, 44 mSDsCounter, 0 mSdLazyCounter, 4 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 71 SdHoareTripleChecker+Invalid, 5 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 4 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,876 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 71 Invalid, 5 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 4 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:16,877 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:16,880 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:16,880 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 7 states have call successors, (7), 6 states have call predecessors, (7), 7 states have return successors, (8), 7 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:16,881 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 27 transitions.
[2025-04-28 21:21:16,881 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 27 transitions. Word has length 26
[2025-04-28 21:21:16,881 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,881 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 27 transitions.
[2025-04-28 21:21:16,882 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:16,882 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 27 transitions.
[2025-04-28 21:21:16,882 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 27
[2025-04-28 21:21:16,883 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,883 INFO  L218           NwaCegarLoop]: trace histogram [2, 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:16,883 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:16,883 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,884 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,884 INFO  L85        PathProgramCache]: Analyzing trace with hash -927243009, now seen corresponding path program 1 times
[2025-04-28 21:21:16,884 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,884 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [556924291]
[2025-04-28 21:21:16,884 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,885 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,903 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:21:16,932 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:21:16,932 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,933 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,261 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:17,261 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,261 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [556924291]
[2025-04-28 21:21:17,261 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [556924291] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:17,261 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [955312782]
[2025-04-28 21:21:17,261 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,262 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:17,265 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:17,267 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:17,272 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:17,324 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:21:17,353 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:21:17,354 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,354 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,356 INFO  L256         TraceCheckSpWp]: Trace formula consists of 88 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:17,364 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:17,596 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:17,600 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:18,409 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:18,409 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [955312782] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:18,409 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:18,409 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 12
[2025-04-28 21:21:18,409 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [409990129]
[2025-04-28 21:21:18,409 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,411 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:18,411 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,412 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:18,413 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=102, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:18,413 INFO  L87              Difference]: Start difference. First operand 26 states and 27 transitions. Second operand  has 12 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 12 states have internal predecessors, (17), 8 states have call successors, (13), 1 states have call predecessors, (13), 7 states have return successors, (14), 8 states have call predecessors, (14), 8 states have call successors, (14)
[2025-04-28 21:21:18,488 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,488 INFO  L93              Difference]: Finished difference Result 31 states and 33 transitions.
[2025-04-28 21:21:18,490 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:18,491 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 12 states have internal predecessors, (17), 8 states have call successors, (13), 1 states have call predecessors, (13), 7 states have return successors, (14), 8 states have call predecessors, (14), 8 states have call successors, (14) Word has length 26
[2025-04-28 21:21:18,491 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,492 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:18,492 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:18,492 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 14 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=30, Invalid=102, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:18,493 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 3 mSDsluCounter, 141 mSDsCounter, 0 mSdLazyCounter, 29 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 165 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 29 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,493 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 165 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 29 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:18,496 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:18,501 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 31.
[2025-04-28 21:21:18,502 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 8 states have call successors, (8), 6 states have call predecessors, (8), 9 states have return successors, (11), 10 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:18,503 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 33 transitions.
[2025-04-28 21:21:18,503 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 33 transitions. Word has length 26
[2025-04-28 21:21:18,503 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,503 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 33 transitions.
[2025-04-28 21:21:18,503 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 12 states have internal predecessors, (17), 8 states have call successors, (13), 1 states have call predecessors, (13), 7 states have return successors, (14), 8 states have call predecessors, (14), 8 states have call successors, (14)
[2025-04-28 21:21:18,504 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 33 transitions.
[2025-04-28 21:21:18,504 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:18,505 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,505 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,511 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:18,709 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:18,709 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,710 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,710 INFO  L85        PathProgramCache]: Analyzing trace with hash -1803250, now seen corresponding path program 2 times
[2025-04-28 21:21:18,710 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,710 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1626740773]
[2025-04-28 21:21:18,710 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:18,710 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,722 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 37 statements into 2 equivalence classes.
[2025-04-28 21:21:18,741 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:18,741 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:18,742 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,024 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 8 proven. 3 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:19,024 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,025 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1626740773]
[2025-04-28 21:21:19,025 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1626740773] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:19,025 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [647861137]
[2025-04-28 21:21:19,025 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:19,025 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:19,028 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:19,030 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:19,034 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:19,098 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 37 statements into 2 equivalence classes.
[2025-04-28 21:21:19,127 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:19,128 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:19,128 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,129 INFO  L256         TraceCheckSpWp]: Trace formula consists of 134 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:19,132 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:19,448 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 1 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:19,448 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:21,759 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 1 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:21,759 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [647861137] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:21,759 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:21,759 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 11, 11] total 18
[2025-04-28 21:21:21,759 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1842491046]
[2025-04-28 21:21:21,759 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,760 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:21,760 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,761 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:21,761 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=50, Invalid=256, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:21,761 INFO  L87              Difference]: Start difference. First operand 31 states and 33 transitions. Second operand  has 18 states, 10 states have (on average 2.8) internal successors, (28), 18 states have internal predecessors, (28), 13 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (22), 12 states have call predecessors, (22), 13 states have call successors, (22)
[2025-04-28 21:21:21,949 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,949 INFO  L93              Difference]: Finished difference Result 28 states and 30 transitions.
[2025-04-28 21:21:21,949 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:21,950 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 10 states have (on average 2.8) internal successors, (28), 18 states have internal predecessors, (28), 13 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (22), 12 states have call predecessors, (22), 13 states have call successors, (22) Word has length 37
[2025-04-28 21:21:21,950 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,950 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:21,950 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:21,951 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 86 GetRequests, 65 SyntacticMatches, 0 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 70 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=85, Invalid=421, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:21,952 INFO  L437           NwaCegarLoop]: 20 mSDtfsCounter, 5 mSDsluCounter, 143 mSDsCounter, 0 mSdLazyCounter, 69 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 163 SdHoareTripleChecker+Invalid, 80 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 69 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,954 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 163 Invalid, 80 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 69 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:21,955 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:21,955 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:21,955 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:21:21,955 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:21,955 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 37
[2025-04-28 21:21:21,955 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,956 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:21,958 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 10 states have (on average 2.8) internal successors, (28), 18 states have internal predecessors, (28), 13 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (22), 12 states have call predecessors, (22), 13 states have call successors, (22)
[2025-04-28 21:21:21,958 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:21,959 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:21,961 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:21,967 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:22,166 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,169 INFO  L422         BasicCegarLoop]: Path program histogram: [2, 1, 1, 1]
[2025-04-28 21:21:22,172 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:22,175 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:22 BoogieIcfgContainer
[2025-04-28 21:21:22,175 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:22,176 INFO  L158              Benchmark]: Toolchain (without parser) took 6523.69ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 161.7MB in the beginning and 89.7MB in the end (delta: 71.9MB). Peak memory consumption was 9.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:22,177 INFO  L158              Benchmark]: SmtParser took 0.31ms. Allocated memory is still 234.9MB. Free memory was 169.6MB in the beginning and 168.9MB in the end (delta: 783.0kB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:22,177 INFO  L158              Benchmark]: ChcToBoogie took 33.17ms. Allocated memory is still 234.9MB. Free memory was 161.7MB in the beginning and 160.1MB in the end (delta: 1.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:22,177 INFO  L158              Benchmark]: Boogie Preprocessor took 76.79ms. Allocated memory is still 234.9MB. Free memory was 160.1MB in the beginning and 158.5MB in the end (delta: 1.6MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:22,178 INFO  L158              Benchmark]: RCFGBuilder took 260.60ms. Allocated memory is still 234.9MB. Free memory was 158.5MB in the beginning and 148.9MB in the end (delta: 9.5MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:22,178 INFO  L158              Benchmark]: TraceAbstraction took 6143.68ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 148.1MB in the beginning and 89.7MB in the end (delta: 58.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:22,180 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.31ms. Allocated memory is still 234.9MB. Free memory was 169.6MB in the beginning and 168.9MB in the end (delta: 783.0kB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * ChcToBoogie took 33.17ms. Allocated memory is still 234.9MB. Free memory was 161.7MB in the beginning and 160.1MB in the end (delta: 1.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 76.79ms. Allocated memory is still 234.9MB. Free memory was 160.1MB in the beginning and 158.5MB in the end (delta: 1.6MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 260.60ms. Allocated memory is still 234.9MB. Free memory was 158.5MB in the beginning and 148.9MB in the end (delta: 9.5MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 6143.68ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 148.1MB in the beginning and 89.7MB in the end (delta: 58.4MB). 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
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 7 procedures, 26 locations, 36 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 6.1s, OverallIterations: 5, TraceHistogramMax: 3, PathProgramHistogramMax: 2, EmptinessCheckTime: 0.0s, AutomataDifference: 0.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 19 SdHoareTripleChecker+Valid, 0.2s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 11 mSDsluCounter, 535 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 412 mSDsCounter, 15 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 116 IncrementalHoareTripleChecker+Invalid, 131 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 15 mSolverCounterUnsat, 123 mSDtfsCounter, 116 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 156 GetRequests, 119 SyntacticMatches, 0 SemanticMatches, 37 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 84 ImplicationChecksByTransitivity, 0.5s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=31occurred in iteration=4, InterpolantAutomatonStates: 31, 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, 5 MinimizatonAttempts, 4 StatesRemovedByMinimization, 1 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 4.6s InterpolantComputationTime, 182 NumberOfCodeBlocks, 182 NumberOfCodeBlocksAsserted, 9 NumberOfCheckSat, 236 ConstructedInterpolants, 0 QuantifiedInterpolants, 469 SizeOfPredicates, 12 NumberOfNonLiveVariables, 222 ConjunctsInSsa, 38 ConjunctsInUnsatCore, 9 InterpolantComputations, 3 PerfectInterpolantSequences, 34/63 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
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:21:22,195 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...
sat
