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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:33,008 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:33,129 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b90d8bca-212f-4fff-a728-bbcdfaa02e1e/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:33,138 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:33,139 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:33,178 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:33,178 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:33,178 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:33,179 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:33,180 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:33,181 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:33,181 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:33,181 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:33,181 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:33,181 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:33,182 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:33,182 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:33,182 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:33,182 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:33,182 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:33,182 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:33,182 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:33,182 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:33,183 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:33,183 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:33,185 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:33,186 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:33,570 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:33,585 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:33,588 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:33,591 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:33,592 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:33,594 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b90d8bca-212f-4fff-a728-bbcdfaa02e1e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-048.smt2
[2025-04-28 21:21:33,599 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:33,607 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:33,982 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b90d8bca-212f-4fff-a728-bbcdfaa02e1e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-048.smt2
[2025-04-28 21:21:33,986 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:33,992 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:33,994 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:33,994 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:33,994 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:34,000 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:34,056 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34 Unit
[2025-04-28 21:21:34,060 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:34,062 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:34,062 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:34,062 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:34,083 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,084 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,118 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,119 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,130 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,131 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,136 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,137 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,142 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,164 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:34,168 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:34,168 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:34,168 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:34,169 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,171 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:34,185 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,198 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:34,201 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:34,213 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:34,213 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:34,213 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:34,213 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:34,213 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:34,214 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:34,214 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb45.i given in one single declaration
[2025-04-28 21:21:34,214 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb45.i
[2025-04-28 21:21:34,214 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb45.i
[2025-04-28 21:21:34,214 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb18.i given in one single declaration
[2025-04-28 21:21:34,214 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb18.i
[2025-04-28 21:21:34,214 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb18.i
[2025-04-28 21:21:34,214 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:34,214 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:34,214 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:34,214 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:34,215 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:34,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:34,298 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:34,300 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:34,551 INFO  L?                        ?]: Removed 85 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:34,551 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:34,575 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:34,575 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:34,576 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:34 BoogieIcfgContainer
[2025-04-28 21:21:34,576 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:34,579 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:34,581 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:34,585 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:34,587 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:33" (1/3) ...
[2025-04-28 21:21:34,588 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@469ee4d3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:34, skipping insertion in model container
[2025-04-28 21:21:34,588 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (2/3) ...
[2025-04-28 21:21:34,588 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@469ee4d3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:34, skipping insertion in model container
[2025-04-28 21:21:34,590 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:34" (3/3) ...
[2025-04-28 21:21:34,592 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:34,608 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:34,611 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 6 procedures, 24 locations, 34 edges, 6 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:34,661 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:34,676 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;@75898805, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:34,676 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:34,683 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 24 states, 10 states have (on average 1.3) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 5 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:34,695 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:34,695 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,696 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:34,697 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,703 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,705 INFO  L85        PathProgramCache]: Analyzing trace with hash -1702169744, now seen corresponding path program 1 times
[2025-04-28 21:21:34,714 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,714 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1774353521]
[2025-04-28 21:21:34,715 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,715 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,776 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:34,846 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:34,846 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,846 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,391 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:35,391 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,392 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1774353521]
[2025-04-28 21:21:35,393 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1774353521] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,393 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:35,396 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:35,398 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [931410521]
[2025-04-28 21:21:35,399 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,403 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:35,403 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,438 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:35,440 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:35,442 INFO  L87              Difference]: Start difference. First operand  has 24 states, 10 states have (on average 1.3) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 5 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 7 states have call successors, (7) Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:35,564 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,565 INFO  L93              Difference]: Finished difference Result 28 states and 33 transitions.
[2025-04-28 21:21:35,566 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:35,568 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 19
[2025-04-28 21:21:35,568 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,604 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:35,605 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:35,606 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:35,610 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 3 mSDsluCounter, 73 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 95 SdHoareTripleChecker+Invalid, 28 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,610 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 95 Invalid, 28 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:35,655 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:35,672 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 26.
[2025-04-28 21:21:35,673 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 5 states have call predecessors, (7), 7 states have return successors, (10), 7 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:35,686 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 30 transitions.
[2025-04-28 21:21:35,688 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 30 transitions. Word has length 19
[2025-04-28 21:21:35,688 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,689 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 30 transitions.
[2025-04-28 21:21:35,689 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:35,692 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 30 transitions.
[2025-04-28 21:21:35,694 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-04-28 21:21:35,694 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,694 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]
[2025-04-28 21:21:35,695 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:35,695 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,700 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,700 INFO  L85        PathProgramCache]: Analyzing trace with hash 1852032173, now seen corresponding path program 1 times
[2025-04-28 21:21:35,700 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,700 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1382307078]
[2025-04-28 21:21:35,700 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,700 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,732 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:35,870 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:35,870 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,870 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,539 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:37,539 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,540 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1382307078]
[2025-04-28 21:21:37,541 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1382307078] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,541 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [872142660]
[2025-04-28 21:21:37,541 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,542 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,545 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,550 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:37,552 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,645 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:37,707 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:37,708 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,708 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,712 INFO  L256         TraceCheckSpWp]: Trace formula consists of 185 conjuncts, 67 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,723 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,902 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 12 treesize of output 1
[2025-04-28 21:21:37,907 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 12 treesize of output 1
[2025-04-28 21:21:37,912 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 18 treesize of output 17
[2025-04-28 21:21:38,050 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:38,052 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:41,096 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:41,100 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:41,110 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:41,111 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 1 case distinctions, treesize of input 13 treesize of output 12
[2025-04-28 21:21:41,653 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:41,664 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:41,665 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 1 case distinctions, treesize of input 13 treesize of output 12
[2025-04-28 21:21:41,675 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:41,862 INFO  L172   IndexEqualityManager]: detected equality via solver
[2025-04-28 21:21:41,862 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 13 treesize of output 1
[2025-04-28 21:21:41,913 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:41,913 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [872142660] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:41,914 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:41,914 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:41,915 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1585555807]
[2025-04-28 21:21:41,915 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,916 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:41,916 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,916 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:41,917 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:41,917 INFO  L87              Difference]: Start difference. First operand 26 states and 30 transitions. Second operand  has 12 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:42,136 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,136 INFO  L93              Difference]: Finished difference Result 32 states and 38 transitions.
[2025-04-28 21:21:42,137 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:42,137 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11) Word has length 23
[2025-04-28 21:21:42,137 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,139 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:42,139 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:42,140 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 43 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:42,140 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 6 mSDsluCounter, 132 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 156 SdHoareTripleChecker+Invalid, 78 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,141 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 156 Invalid, 78 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:42,144 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:42,153 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 28.
[2025-04-28 21:21:42,153 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 5 states have call predecessors, (7), 8 states have return successors, (12), 8 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:42,156 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 33 transitions.
[2025-04-28 21:21:42,156 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 33 transitions. Word has length 23
[2025-04-28 21:21:42,157 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,157 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 33 transitions.
[2025-04-28 21:21:42,157 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:42,157 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 33 transitions.
[2025-04-28 21:21:42,158 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-04-28 21:21:42,158 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,158 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]
[2025-04-28 21:21:42,165 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:42,359 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,359 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,359 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,360 INFO  L85        PathProgramCache]: Analyzing trace with hash -864348446, now seen corresponding path program 1 times
[2025-04-28 21:21:42,360 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,360 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1051879019]
[2025-04-28 21:21:42,360 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,360 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,377 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:42,396 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:42,396 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,396 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,691 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:42,691 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,691 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1051879019]
[2025-04-28 21:21:42,691 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1051879019] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,691 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,691 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:42,692 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [145395463]
[2025-04-28 21:21:42,692 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,692 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:42,692 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,693 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:42,694 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:42,694 INFO  L87              Difference]: Start difference. First operand 28 states and 33 transitions. Second operand  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 5 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:42,817 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,817 INFO  L93              Difference]: Finished difference Result 34 states and 40 transitions.
[2025-04-28 21:21:42,818 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:42,818 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 5 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 5 states have call successors, (6) Word has length 23
[2025-04-28 21:21:42,818 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,819 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:42,819 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:42,819 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:42,820 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 5 mSDsluCounter, 88 mSDsCounter, 0 mSdLazyCounter, 47 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 110 SdHoareTripleChecker+Invalid, 47 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 47 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,820 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 110 Invalid, 47 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 47 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:42,821 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:42,825 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 28.
[2025-04-28 21:21:42,825 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 5 states have call predecessors, (7), 8 states have return successors, (11), 8 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:42,826 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 32 transitions.
[2025-04-28 21:21:42,826 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 32 transitions. Word has length 23
[2025-04-28 21:21:42,826 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,826 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 32 transitions.
[2025-04-28 21:21:42,827 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 5 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:42,827 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 32 transitions.
[2025-04-28 21:21:42,827 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 28
[2025-04-28 21:21:42,827 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,828 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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:42,828 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:42,828 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,828 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,829 INFO  L85        PathProgramCache]: Analyzing trace with hash -2119075617, now seen corresponding path program 1 times
[2025-04-28 21:21:42,829 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,829 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [861245567]
[2025-04-28 21:21:42,829 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,829 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,839 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 27 statements into 1 equivalence classes.
[2025-04-28 21:21:42,851 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:42,851 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,851 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,313 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:43,313 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,313 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [861245567]
[2025-04-28 21:21:43,314 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [861245567] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,314 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1034369558]
[2025-04-28 21:21:43,314 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,314 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,317 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,320 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:43,325 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,415 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 27 statements into 1 equivalence classes.
[2025-04-28 21:21:43,467 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:43,468 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,468 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,475 INFO  L256         TraceCheckSpWp]: Trace formula consists of 234 conjuncts, 32 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,479 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,678 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:43,678 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,893 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:46,893 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1034369558] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,893 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,893 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 20
[2025-04-28 21:21:46,893 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1115457262]
[2025-04-28 21:21:46,893 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,894 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:46,894 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,895 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:46,896 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=61, Invalid=319, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:46,896 INFO  L87              Difference]: Start difference. First operand 28 states and 32 transitions. Second operand  has 20 states, 10 states have (on average 2.4) internal successors, (24), 20 states have internal predecessors, (24), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (16), 9 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:47,123 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,123 INFO  L93              Difference]: Finished difference Result 32 states and 37 transitions.
[2025-04-28 21:21:47,126 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:47,127 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.4) internal successors, (24), 20 states have internal predecessors, (24), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (16), 9 states have call predecessors, (16), 13 states have call successors, (16) Word has length 27
[2025-04-28 21:21:47,127 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,128 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:47,128 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:47,128 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 43 SyntacticMatches, 2 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 94 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=84, Invalid=422, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:47,129 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 11 mSDsluCounter, 188 mSDsCounter, 0 mSdLazyCounter, 119 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 211 SdHoareTripleChecker+Invalid, 124 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 119 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,130 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 211 Invalid, 124 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 119 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:47,133 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:47,139 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 26.
[2025-04-28 21:21:47,140 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 5 states have call predecessors, (7), 7 states have return successors, (9), 7 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:47,141 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 29 transitions.
[2025-04-28 21:21:47,141 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 29 transitions. Word has length 27
[2025-04-28 21:21:47,141 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,141 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 29 transitions.
[2025-04-28 21:21:47,141 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.4) internal successors, (24), 20 states have internal predecessors, (24), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (16), 9 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:47,142 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 29 transitions.
[2025-04-28 21:21:47,144 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 28
[2025-04-28 21:21:47,145 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,145 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,152 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:47,349 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,350 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,350 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,350 INFO  L85        PathProgramCache]: Analyzing trace with hash -574323542, now seen corresponding path program 2 times
[2025-04-28 21:21:47,350 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,351 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [493141579]
[2025-04-28 21:21:47,351 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,351 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,371 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 27 statements into 2 equivalence classes.
[2025-04-28 21:21:47,472 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:47,472 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,472 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,868 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:48,868 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,868 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [493141579]
[2025-04-28 21:21:48,869 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [493141579] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:48,869 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1892308874]
[2025-04-28 21:21:48,869 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:48,869 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,871 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,873 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:48,876 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,974 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 27 statements into 2 equivalence classes.
[2025-04-28 21:21:49,017 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:49,017 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:49,018 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,022 INFO  L256         TraceCheckSpWp]: Trace formula consists of 244 conjuncts, 95 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:49,026 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:49,128 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 20 treesize of output 17
[2025-04-28 21:21:49,138 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 12 treesize of output 1
[2025-04-28 21:21:49,147 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 12 treesize of output 1
[2025-04-28 21:21:49,211 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 24 treesize of output 15
[2025-04-28 21:21:49,222 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 24 treesize of output 15
[2025-04-28 21:21:49,225 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 24 treesize of output 15
[2025-04-28 21:21:49,289 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:49,290 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,171 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 18 treesize of output 1
[2025-04-28 21:21:54,175 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 18 treesize of output 1
[2025-04-28 21:21:54,182 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:54,182 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 1 case distinctions, treesize of input 24 treesize of output 12
[2025-04-28 21:21:55,366 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 18 treesize of output 1
[2025-04-28 21:21:55,382 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:55,382 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 1 case distinctions, treesize of input 24 treesize of output 12
[2025-04-28 21:21:55,399 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 18 treesize of output 1
[2025-04-28 21:21:55,913 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:55,922 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:55,922 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 1 case distinctions, treesize of input 15 treesize of output 12
[2025-04-28 21:21:55,934 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:55,981 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 11 treesize of output 9
[2025-04-28 21:21:56,096 INFO  L172   IndexEqualityManager]: detected equality via solver
[2025-04-28 21:21:56,097 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 13 treesize of output 1
[2025-04-28 21:21:56,134 INFO  L325             Elim1Store]: treesize reduction 5, result has 16.7 percent of original size
[2025-04-28 21:21:56,135 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 1 select indices, 1 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 1 case distinctions, treesize of input 26 treesize of output 1
[2025-04-28 21:21:56,157 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:56,157 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1892308874] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,157 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,157 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 17
[2025-04-28 21:21:56,157 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [778706310]
[2025-04-28 21:21:56,158 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,158 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:56,158 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,159 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:56,159 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=47, Invalid=225, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:56,159 INFO  L87              Difference]: Start difference. First operand 26 states and 29 transitions. Second operand  has 17 states, 8 states have (on average 2.5) internal successors, (20), 17 states have internal predecessors, (20), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (15), 7 states have call predecessors, (15), 11 states have call successors, (15)
[2025-04-28 21:21:56,404 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,405 INFO  L93              Difference]: Finished difference Result 28 states and 31 transitions.
[2025-04-28 21:21:56,406 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:56,406 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 17 states have internal predecessors, (20), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (15), 7 states have call predecessors, (15), 11 states have call successors, (15) Word has length 27
[2025-04-28 21:21:56,407 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,407 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:56,407 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:56,408 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 37 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=76, Invalid=304, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:56,409 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 7 mSDsluCounter, 198 mSDsCounter, 0 mSdLazyCounter, 73 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 221 SdHoareTripleChecker+Invalid, 84 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 73 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,409 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 221 Invalid, 84 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 73 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,410 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:56,413 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 28.
[2025-04-28 21:21:56,413 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 5 states have call predecessors, (7), 8 states have return successors, (10), 8 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:56,414 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 31 transitions.
[2025-04-28 21:21:56,414 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 31 transitions. Word has length 27
[2025-04-28 21:21:56,415 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,415 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 31 transitions.
[2025-04-28 21:21:56,415 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 17 states have internal predecessors, (20), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (15), 7 states have call predecessors, (15), 11 states have call successors, (15)
[2025-04-28 21:21:56,415 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 31 transitions.
[2025-04-28 21:21:56,416 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 32
[2025-04-28 21:21:56,416 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,416 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 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:56,421 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:56,616 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,617 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,617 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,617 INFO  L85        PathProgramCache]: Analyzing trace with hash 131668380, now seen corresponding path program 2 times
[2025-04-28 21:21:56,617 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,617 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1405087457]
[2025-04-28 21:21:56,617 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:56,618 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,629 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 31 statements into 2 equivalence classes.
[2025-04-28 21:21:56,712 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 31 of 31 statements.
[2025-04-28 21:21:56,713 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:56,713 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,932 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:57,932 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,933 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1405087457]
[2025-04-28 21:21:57,933 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1405087457] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,933 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1041159675]
[2025-04-28 21:21:57,933 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:57,933 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,937 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,939 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:57,944 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,088 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 31 statements into 2 equivalence classes.
[2025-04-28 21:21:58,141 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 31 of 31 statements.
[2025-04-28 21:21:58,141 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:58,141 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,147 INFO  L256         TraceCheckSpWp]: Trace formula consists of 293 conjuncts, 100 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,150 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,259 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 20 treesize of output 17
[2025-04-28 21:21:58,267 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 12 treesize of output 1
[2025-04-28 21:21:58,272 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 12 treesize of output 1
[2025-04-28 21:21:58,666 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:58,666 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
