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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:42,682 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:42,784 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_59b804f0-0aac-4d79-bf08-e04c2309f89d/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:42,792 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:42,793 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:42,828 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:42,829 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:42,829 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:42,829 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:42,829 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:42,830 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:42,830 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:42,830 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:42,830 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:42,830 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:42,830 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:42,830 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:42,830 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:42,831 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:42,831 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:42,831 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:42,831 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:42,831 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:42,831 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:42,833 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:42,834 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:42,834 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:43,166 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:43,176 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:43,179 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:43,181 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:43,182 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:43,184 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_59b804f0-0aac-4d79-bf08-e04c2309f89d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-058.smt2
[2025-04-28 21:21:43,186 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:43,189 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:43,545 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_59b804f0-0aac-4d79-bf08-e04c2309f89d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-058.smt2
[2025-04-28 21:21:43,549 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:43,550 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:43,551 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:43,551 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:43,551 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:43,557 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,609 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43 Unit
[2025-04-28 21:21:43,611 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:43,613 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:43,613 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:43,613 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:43,631 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,631 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,677 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,678 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,686 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,691 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,693 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,695 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,700 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,729 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:43,730 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:43,731 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:43,733 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:43,734 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,737 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:43,755 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,770 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,774 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,789 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:43,789 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:43,789 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:43,789 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:43,790 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:43,790 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:43,790 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb77.i given in one single declaration
[2025-04-28 21:21:43,790 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb77.i
[2025-04-28 21:21:43,790 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb77.i
[2025-04-28 21:21:43,790 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb51.i given in one single declaration
[2025-04-28 21:21:43,790 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb51.i
[2025-04-28 21:21:43,790 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb51.i
[2025-04-28 21:21:43,790 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb28.i given in one single declaration
[2025-04-28 21:21:43,791 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb28.i
[2025-04-28 21:21:43,791 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb28.i
[2025-04-28 21:21:43,791 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb14.i given in one single declaration
[2025-04-28 21:21:43,791 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb14.i
[2025-04-28 21:21:43,791 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb14.i
[2025-04-28 21:21:43,791 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:43,791 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:43,791 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:43,792 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:43,792 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:43,792 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:43,867 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:43,870 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:44,148 INFO  L?                        ?]: Removed 86 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:44,148 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:44,169 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:44,169 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:44,170 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:44 BoogieIcfgContainer
[2025-04-28 21:21:44,170 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:44,175 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:44,176 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:44,181 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:44,182 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:43" (1/3) ...
[2025-04-28 21:21:44,182 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@45a8da30 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:44, skipping insertion in model container
[2025-04-28 21:21:44,183 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (2/3) ...
[2025-04-28 21:21:44,183 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@45a8da30 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:44, skipping insertion in model container
[2025-04-28 21:21:44,184 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:44" (3/3) ...
[2025-04-28 21:21:44,186 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:44,202 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:44,205 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 8 procedures, 34 locations, 52 edges, 8 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:44,275 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:44,291 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;@449a9acd, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:44,292 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:44,297 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 34 states, 14 states have (on average 1.3571428571428572) internal successors, (19), 19 states have internal predecessors, (19), 11 states have call successors, (11), 7 states have call predecessors, (11), 7 states have return successors, (11), 7 states have call predecessors, (11), 11 states have call successors, (11)
[2025-04-28 21:21:44,309 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 28
[2025-04-28 21:21:44,310 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,311 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,311 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,319 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,319 INFO  L85        PathProgramCache]: Analyzing trace with hash -199631287, now seen corresponding path program 1 times
[2025-04-28 21:21:44,330 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,330 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1345348660]
[2025-04-28 21:21:44,331 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,331 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,389 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 27 statements into 1 equivalence classes.
[2025-04-28 21:21:44,461 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:44,466 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,466 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,955 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:44,958 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,958 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1345348660]
[2025-04-28 21:21:44,960 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1345348660] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,960 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,964 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:44,965 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1391341495]
[2025-04-28 21:21:44,968 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,972 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:44,974 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,003 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:45,005 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:45,037 INFO  L87              Difference]: Start difference. First operand  has 34 states, 14 states have (on average 1.3571428571428572) internal successors, (19), 19 states have internal predecessors, (19), 11 states have call successors, (11), 7 states have call predecessors, (11), 7 states have return successors, (11), 7 states have call predecessors, (11), 11 states have call successors, (11) Second operand  has 6 states, 4 states have (on average 3.25) internal successors, (13), 6 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:45,218 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,219 INFO  L93              Difference]: Finished difference Result 38 states and 47 transitions.
[2025-04-28 21:21:45,221 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:45,222 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.25) internal successors, (13), 6 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 27
[2025-04-28 21:21:45,223 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,236 INFO  L225             Difference]: With dead ends: 38
[2025-04-28 21:21:45,239 INFO  L226             Difference]: Without dead ends: 38
[2025-04-28 21:21:45,241 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:45,245 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 3 mSDsluCounter, 129 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 165 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:45,247 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 165 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:45,267 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 38 states.
[2025-04-28 21:21:45,314 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 38 to 36.
[2025-04-28 21:21:45,321 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 15 states have (on average 1.2666666666666666) internal successors, (19), 19 states have internal predecessors, (19), 11 states have call successors, (11), 7 states have call predecessors, (11), 9 states have return successors, (14), 9 states have call predecessors, (14), 11 states have call successors, (14)
[2025-04-28 21:21:45,338 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 44 transitions.
[2025-04-28 21:21:45,342 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 44 transitions. Word has length 27
[2025-04-28 21:21:45,343 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,343 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 44 transitions.
[2025-04-28 21:21:45,343 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.25) internal successors, (13), 6 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:45,343 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 44 transitions.
[2025-04-28 21:21:45,345 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 32
[2025-04-28 21:21:45,346 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,347 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,347 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:45,347 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,348 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,349 INFO  L85        PathProgramCache]: Analyzing trace with hash -1819134533, now seen corresponding path program 1 times
[2025-04-28 21:21:45,349 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,349 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2058342456]
[2025-04-28 21:21:45,349 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,349 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,375 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 31 statements into 1 equivalence classes.
[2025-04-28 21:21:45,414 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 31 of 31 statements.
[2025-04-28 21:21:45,415 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,415 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,828 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:45,829 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,829 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2058342456]
[2025-04-28 21:21:45,829 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2058342456] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,829 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,830 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:45,830 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1186675896]
[2025-04-28 21:21:45,830 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,831 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:45,831 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,832 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:45,833 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:45,833 INFO  L87              Difference]: Start difference. First operand 36 states and 44 transitions. Second operand  has 8 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:46,001 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,001 INFO  L93              Difference]: Finished difference Result 48 states and 60 transitions.
[2025-04-28 21:21:46,003 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:46,003 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8) Word has length 31
[2025-04-28 21:21:46,004 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,005 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:46,006 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:46,006 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:46,007 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 5 mSDsluCounter, 181 mSDsCounter, 0 mSdLazyCounter, 56 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 215 SdHoareTripleChecker+Invalid, 56 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 56 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,010 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 215 Invalid, 56 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 56 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:46,011 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:46,022 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 40.
[2025-04-28 21:21:46,022 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 17 states have (on average 1.2352941176470589) internal successors, (21), 21 states have internal predecessors, (21), 11 states have call successors, (11), 7 states have call predecessors, (11), 11 states have return successors, (18), 11 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:21:46,023 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 50 transitions.
[2025-04-28 21:21:46,025 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 50 transitions. Word has length 31
[2025-04-28 21:21:46,025 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,026 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 50 transitions.
[2025-04-28 21:21:46,026 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:46,026 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 50 transitions.
[2025-04-28 21:21:46,028 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 32
[2025-04-28 21:21:46,029 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,029 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,029 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:46,029 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,030 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,030 INFO  L85        PathProgramCache]: Analyzing trace with hash 1638041815, now seen corresponding path program 1 times
[2025-04-28 21:21:46,031 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,031 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1359717813]
[2025-04-28 21:21:46,031 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,032 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,047 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 31 statements into 1 equivalence classes.
[2025-04-28 21:21:46,066 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 31 of 31 statements.
[2025-04-28 21:21:46,067 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,068 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,305 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:46,305 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,305 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1359717813]
[2025-04-28 21:21:46,305 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1359717813] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,305 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,306 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:46,306 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [86803823]
[2025-04-28 21:21:46,306 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,307 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:46,307 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,308 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:46,308 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:46,309 INFO  L87              Difference]: Start difference. First operand 40 states and 50 transitions. Second operand  has 7 states, 5 states have (on average 2.8) internal successors, (14), 7 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:46,445 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,445 INFO  L93              Difference]: Finished difference Result 44 states and 54 transitions.
[2025-04-28 21:21:46,446 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:46,446 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.8) internal successors, (14), 7 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8) Word has length 31
[2025-04-28 21:21:46,446 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,447 INFO  L225             Difference]: With dead ends: 44
[2025-04-28 21:21:46,447 INFO  L226             Difference]: Without dead ends: 44
[2025-04-28 21:21:46,447 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:46,448 INFO  L437           NwaCegarLoop]: 33 mSDtfsCounter, 2 mSDsluCounter, 141 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 174 SdHoareTripleChecker+Invalid, 56 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,449 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 174 Invalid, 56 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:46,450 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 44 states.
[2025-04-28 21:21:46,455 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 44 to 42.
[2025-04-28 21:21:46,455 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 18 states have (on average 1.2222222222222223) internal successors, (22), 22 states have internal predecessors, (22), 11 states have call successors, (11), 7 states have call predecessors, (11), 12 states have return successors, (18), 12 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:21:46,456 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 51 transitions.
[2025-04-28 21:21:46,457 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 51 transitions. Word has length 31
[2025-04-28 21:21:46,457 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,457 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 51 transitions.
[2025-04-28 21:21:46,457 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.8) internal successors, (14), 7 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:46,457 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 51 transitions.
[2025-04-28 21:21:46,458 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 36
[2025-04-28 21:21:46,458 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,459 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, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,459 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:46,459 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,459 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,460 INFO  L85        PathProgramCache]: Analyzing trace with hash 509456585, now seen corresponding path program 1 times
[2025-04-28 21:21:46,460 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,460 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [891874742]
[2025-04-28 21:21:46,460 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,460 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,473 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 35 statements into 1 equivalence classes.
[2025-04-28 21:21:46,491 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 35 of 35 statements.
[2025-04-28 21:21:46,491 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,491 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,838 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:46,838 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,838 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [891874742]
[2025-04-28 21:21:46,838 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [891874742] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,839 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,839 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:46,839 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1475914498]
[2025-04-28 21:21:46,839 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,839 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:46,839 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,840 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:46,840 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:46,840 INFO  L87              Difference]: Start difference. First operand 42 states and 51 transitions. Second operand  has 8 states, 5 states have (on average 3.2) internal successors, (16), 8 states have internal predecessors, (16), 5 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:46,974 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,974 INFO  L93              Difference]: Finished difference Result 44 states and 53 transitions.
[2025-04-28 21:21:46,977 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:46,977 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 3.2) internal successors, (16), 8 states have internal predecessors, (16), 5 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 5 states have call successors, (9) Word has length 35
[2025-04-28 21:21:46,978 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,978 INFO  L225             Difference]: With dead ends: 44
[2025-04-28 21:21:46,979 INFO  L226             Difference]: Without dead ends: 38
[2025-04-28 21:21:46,979 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=18, Invalid=54, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:46,980 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 4 mSDsluCounter, 145 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 179 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,980 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 179 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:46,982 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 38 states.
[2025-04-28 21:21:46,990 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 38 to 36.
[2025-04-28 21:21:46,990 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 15 states have (on average 1.2666666666666666) internal successors, (19), 19 states have internal predecessors, (19), 11 states have call successors, (11), 7 states have call predecessors, (11), 9 states have return successors, (13), 9 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:21:46,991 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 43 transitions.
[2025-04-28 21:21:46,991 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 43 transitions. Word has length 35
[2025-04-28 21:21:46,991 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,991 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 43 transitions.
[2025-04-28 21:21:46,991 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 3.2) internal successors, (16), 8 states have internal predecessors, (16), 5 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:46,992 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 43 transitions.
[2025-04-28 21:21:46,996 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 36
[2025-04-28 21:21:46,996 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,996 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, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,996 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:46,996 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,997 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,997 INFO  L85        PathProgramCache]: Analyzing trace with hash 1125997917, now seen corresponding path program 1 times
[2025-04-28 21:21:46,997 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,997 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [170083853]
[2025-04-28 21:21:46,997 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,997 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,012 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 35 statements into 1 equivalence classes.
[2025-04-28 21:21:47,033 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 35 of 35 statements.
[2025-04-28 21:21:47,036 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,037 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,376 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:47,376 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,376 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [170083853]
[2025-04-28 21:21:47,377 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [170083853] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,377 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,377 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:47,378 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1665744221]
[2025-04-28 21:21:47,378 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,378 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:47,378 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,379 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:47,379 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:47,379 INFO  L87              Difference]: Start difference. First operand 36 states and 43 transitions. Second operand  has 9 states, 6 states have (on average 2.5) internal successors, (15), 9 states have internal predecessors, (15), 5 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 5 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:47,561 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,561 INFO  L93              Difference]: Finished difference Result 50 states and 61 transitions.
[2025-04-28 21:21:47,562 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:47,563 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.5) internal successors, (15), 9 states have internal predecessors, (15), 5 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 5 states have call predecessors, (9), 5 states have call successors, (9) Word has length 35
[2025-04-28 21:21:47,563 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,564 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:21:47,566 INFO  L226             Difference]: Without dead ends: 50
[2025-04-28 21:21:47,566 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=87, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:47,567 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 5 mSDsluCounter, 199 mSDsCounter, 0 mSdLazyCounter, 80 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 231 SdHoareTripleChecker+Invalid, 80 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 80 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,567 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 231 Invalid, 80 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 80 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:47,568 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-04-28 21:21:47,579 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 48.
[2025-04-28 21:21:47,580 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 21 states have (on average 1.1904761904761905) internal successors, (25), 25 states have internal predecessors, (25), 11 states have call successors, (11), 7 states have call predecessors, (11), 15 states have return successors, (22), 15 states have call predecessors, (22), 11 states have call successors, (22)
[2025-04-28 21:21:47,581 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 58 transitions.
[2025-04-28 21:21:47,584 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 58 transitions. Word has length 35
[2025-04-28 21:21:47,585 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,585 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 58 transitions.
[2025-04-28 21:21:47,585 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.5) internal successors, (15), 9 states have internal predecessors, (15), 5 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 5 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:47,585 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 58 transitions.
[2025-04-28 21:21:47,586 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 40
[2025-04-28 21:21:47,586 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,586 INFO  L218           NwaCegarLoop]: trace histogram [2, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,586 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:47,586 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,587 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,587 INFO  L85        PathProgramCache]: Analyzing trace with hash 1069407467, now seen corresponding path program 1 times
[2025-04-28 21:21:47,587 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,587 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [215600758]
[2025-04-28 21:21:47,587 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,590 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,610 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 39 statements into 1 equivalence classes.
[2025-04-28 21:21:47,637 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:47,638 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,638 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,061 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:48,062 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,062 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [215600758]
[2025-04-28 21:21:48,062 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [215600758] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,062 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,062 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:48,063 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [326646041]
[2025-04-28 21:21:48,063 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,064 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:48,064 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,064 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:48,066 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:48,066 INFO  L87              Difference]: Start difference. First operand 48 states and 58 transitions. Second operand  has 9 states, 6 states have (on average 2.8333333333333335) internal successors, (17), 9 states have internal predecessors, (17), 5 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (10), 5 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:21:48,253 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,253 INFO  L93              Difference]: Finished difference Result 50 states and 60 transitions.
[2025-04-28 21:21:48,253 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:48,254 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.8333333333333335) internal successors, (17), 9 states have internal predecessors, (17), 5 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (10), 5 states have call predecessors, (10), 5 states have call successors, (10) Word has length 39
[2025-04-28 21:21:48,254 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,255 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:21:48,255 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:21:48,255 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=87, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:48,256 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 5 mSDsluCounter, 191 mSDsCounter, 0 mSdLazyCounter, 102 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 223 SdHoareTripleChecker+Invalid, 102 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 102 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,258 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 223 Invalid, 102 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 102 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:48,259 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:21:48,266 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 38.
[2025-04-28 21:21:48,266 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 38 states, 16 states have (on average 1.25) internal successors, (20), 20 states have internal predecessors, (20), 11 states have call successors, (11), 7 states have call predecessors, (11), 10 states have return successors, (14), 10 states have call predecessors, (14), 11 states have call successors, (14)
[2025-04-28 21:21:48,267 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 38 states to 38 states and 45 transitions.
[2025-04-28 21:21:48,267 INFO  L79                 Accepts]: Start accepts. Automaton has 38 states and 45 transitions. Word has length 39
[2025-04-28 21:21:48,270 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,270 INFO  L485      AbstractCegarLoop]: Abstraction has 38 states and 45 transitions.
[2025-04-28 21:21:48,270 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.8333333333333335) internal successors, (17), 9 states have internal predecessors, (17), 5 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (10), 5 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:21:48,271 INFO  L278                IsEmpty]: Start isEmpty. Operand 38 states and 45 transitions.
[2025-04-28 21:21:48,271 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 40
[2025-04-28 21:21:48,271 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,272 INFO  L218           NwaCegarLoop]: trace histogram [2, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,272 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:48,272 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,272 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,272 INFO  L85        PathProgramCache]: Analyzing trace with hash 829643062, now seen corresponding path program 1 times
[2025-04-28 21:21:48,273 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,273 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1550588838]
[2025-04-28 21:21:48,273 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,276 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,301 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 39 statements into 1 equivalence classes.
[2025-04-28 21:21:48,387 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:48,387 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,387 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,292 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:50,294 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,294 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1550588838]
[2025-04-28 21:21:50,294 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1550588838] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,294 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1397353445]
[2025-04-28 21:21:50,294 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,295 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,300 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,305 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:50,308 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,406 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 39 statements into 1 equivalence classes.
[2025-04-28 21:21:50,476 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:50,476 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,476 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,481 INFO  L256         TraceCheckSpWp]: Trace formula consists of 241 conjuncts, 97 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,493 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,735 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 14 treesize of output 13
[2025-04-28 21:21:50,825 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 8 treesize of output 7
[2025-04-28 21:21:51,169 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 12 treesize of output 9
[2025-04-28 21:21:51,274 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:51,274 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,962 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:56,963 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 7 treesize of output 6
[2025-04-28 21:21:58,460 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:58,461 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 7 treesize of output 6
[2025-04-28 21:21:59,362 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:59,363 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 7 treesize of output 6
[2025-04-28 21:21:59,371 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:59,371 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 7 treesize of output 6
[2025-04-28 21:21:59,425 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 5 treesize of output 3
[2025-04-28 21:21:59,990 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:59,990 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 7 treesize of output 6
[2025-04-28 21:21:59,999 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:59,999 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 7 treesize of output 6
[2025-04-28 21:22:00,051 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 37 treesize of output 33
[2025-04-28 21:22:00,325 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:00,325 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 7 treesize of output 6
[2025-04-28 21:22:00,369 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 27 treesize of output 23
[2025-04-28 21:22:00,536 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:00,537 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 7 treesize of output 6
[2025-04-28 21:22:00,673 INFO  L172   IndexEqualityManager]: detected equality via solver
[2025-04-28 21:22:00,674 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 7 treesize of output 1
[2025-04-28 21:22:00,694 INFO  L172   IndexEqualityManager]: detected equality via solver
[2025-04-28 21:22:00,694 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 7 treesize of output 1
[2025-04-28 21:22:00,723 INFO  L172   IndexEqualityManager]: detected equality via solver
[2025-04-28 21:22:00,723 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 0 case distinctions, treesize of input 14 treesize of output 1
[2025-04-28 21:22:00,748 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:00,749 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1397353445] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:00,749 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:00,749 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 16, 16] total 31
[2025-04-28 21:22:00,750 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2023909444]
[2025-04-28 21:22:00,750 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,750 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 31 states
[2025-04-28 21:22:00,751 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,752 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 31 interpolants.
[2025-04-28 21:22:00,753 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=82, Invalid=848, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:22:00,753 INFO  L87              Difference]: Start difference. First operand 38 states and 45 transitions. Second operand  has 31 states, 13 states have (on average 3.076923076923077) internal successors, (40), 31 states have internal predecessors, (40), 21 states have call successors, (25), 1 states have call predecessors, (25), 13 states have return successors, (25), 13 states have call predecessors, (25), 21 states have call successors, (25)
[2025-04-28 21:22:01,505 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,505 INFO  L93              Difference]: Finished difference Result 56 states and 68 transitions.
[2025-04-28 21:22:01,506 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 19 states. 
[2025-04-28 21:22:01,506 INFO  L79                 Accepts]: Start accepts. Automaton has  has 31 states, 13 states have (on average 3.076923076923077) internal successors, (40), 31 states have internal predecessors, (40), 21 states have call successors, (25), 1 states have call predecessors, (25), 13 states have return successors, (25), 13 states have call predecessors, (25), 21 states have call successors, (25) Word has length 39
[2025-04-28 21:22:01,506 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,507 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:22:01,507 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:22:01,508 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 100 GetRequests, 60 SyntacticMatches, 0 SemanticMatches, 40 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 208 ImplicationChecksByTransitivity, 1.3s TimeCoverageRelationStatistics Valid=155, Invalid=1567, Unknown=0, NotChecked=0, Total=1722
[2025-04-28 21:22:01,509 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 25 mSDsluCounter, 443 mSDsCounter, 0 mSdLazyCounter, 263 mSolverCounterSat, 31 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 477 SdHoareTripleChecker+Invalid, 294 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 31 IncrementalHoareTripleChecker+Valid, 263 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,509 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 477 Invalid, 294 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [31 Valid, 263 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:01,510 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:22:01,515 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 42.
[2025-04-28 21:22:01,515 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 18 states have (on average 1.2222222222222223) internal successors, (22), 22 states have internal predecessors, (22), 11 states have call successors, (11), 7 states have call predecessors, (11), 12 states have return successors, (17), 12 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:22:01,516 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 50 transitions.
[2025-04-28 21:22:01,516 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 50 transitions. Word has length 39
[2025-04-28 21:22:01,516 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,516 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 50 transitions.
[2025-04-28 21:22:01,517 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 31 states, 13 states have (on average 3.076923076923077) internal successors, (40), 31 states have internal predecessors, (40), 21 states have call successors, (25), 1 states have call predecessors, (25), 13 states have return successors, (25), 13 states have call predecessors, (25), 21 states have call successors, (25)
[2025-04-28 21:22:01,517 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 50 transitions.
[2025-04-28 21:22:01,518 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 44
[2025-04-28 21:22:01,518 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,518 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,528 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:22:01,722 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable7
[2025-04-28 21:22:01,723 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,723 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,723 INFO  L85        PathProgramCache]: Analyzing trace with hash -1672221336, now seen corresponding path program 2 times
[2025-04-28 21:22:01,723 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,724 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1465519302]
[2025-04-28 21:22:01,724 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:01,724 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,740 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 43 statements into 2 equivalence classes.
[2025-04-28 21:22:01,754 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 43 of 43 statements.
[2025-04-28 21:22:01,754 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:01,754 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,145 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 4 proven. 5 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:02,145 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,145 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1465519302]
[2025-04-28 21:22:02,145 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1465519302] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,145 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1158584003]
[2025-04-28 21:22:02,145 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:02,145 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,148 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:02,150 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:22:02,153 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,282 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 43 statements into 2 equivalence classes.
[2025-04-28 21:22:02,330 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 43 of 43 statements.
[2025-04-28 21:22:02,331 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:02,331 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,333 INFO  L256         TraceCheckSpWp]: Trace formula consists of 283 conjuncts, 31 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,335 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,443 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 4 proven. 5 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:02,444 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:05,637 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:05,637 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1158584003] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:05,637 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:05,637 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 19
[2025-04-28 21:22:05,637 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1268058788]
[2025-04-28 21:22:05,637 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,638 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:22:05,638 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,638 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:22:05,639 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=59, Invalid=283, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:22:05,639 INFO  L87              Difference]: Start difference. First operand 42 states and 50 transitions. Second operand  has 19 states, 9 states have (on average 3.3333333333333335) internal successors, (30), 19 states have internal predecessors, (30), 13 states have call successors, (18), 1 states have call predecessors, (18), 9 states have return successors, (19), 9 states have call predecessors, (19), 13 states have call successors, (19)
[2025-04-28 21:22:05,782 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:05,782 INFO  L93              Difference]: Finished difference Result 48 states and 57 transitions.
[2025-04-28 21:22:05,784 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:22:05,784 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 3.3333333333333335) internal successors, (30), 19 states have internal predecessors, (30), 13 states have call successors, (18), 1 states have call predecessors, (18), 9 states have return successors, (19), 9 states have call predecessors, (19), 13 states have call successors, (19) Word has length 43
[2025-04-28 21:22:05,784 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:05,785 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:22:05,785 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:22:05,785 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 99 GetRequests, 77 SyntacticMatches, 1 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 87 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=90, Invalid=416, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:22:05,786 INFO  L437           NwaCegarLoop]: 37 mSDtfsCounter, 15 mSDsluCounter, 284 mSDsCounter, 0 mSdLazyCounter, 99 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 321 SdHoareTripleChecker+Invalid, 117 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 99 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:05,786 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 321 Invalid, 117 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 99 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:05,787 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:22:05,794 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 48.
[2025-04-28 21:22:05,794 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 21 states have (on average 1.1904761904761905) internal successors, (25), 25 states have internal predecessors, (25), 11 states have call successors, (11), 7 states have call predecessors, (11), 15 states have return successors, (21), 15 states have call predecessors, (21), 11 states have call successors, (21)
[2025-04-28 21:22:05,795 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 57 transitions.
[2025-04-28 21:22:05,796 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 57 transitions. Word has length 43
[2025-04-28 21:22:05,796 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:05,796 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 57 transitions.
[2025-04-28 21:22:05,797 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 3.3333333333333335) internal successors, (30), 19 states have internal predecessors, (30), 13 states have call successors, (18), 1 states have call predecessors, (18), 9 states have return successors, (19), 9 states have call predecessors, (19), 13 states have call successors, (19)
[2025-04-28 21:22:05,797 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 57 transitions.
[2025-04-28 21:22:05,798 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 44
[2025-04-28 21:22:05,798 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:05,798 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:05,803 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:22:05,998 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:05,999 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:05,999 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:05,999 INFO  L85        PathProgramCache]: Analyzing trace with hash -1479922812, now seen corresponding path program 1 times
[2025-04-28 21:22:05,999 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:05,999 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1670019894]
[2025-04-28 21:22:05,999 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:05,999 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,009 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 43 statements into 1 equivalence classes.
[2025-04-28 21:22:06,023 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 43 of 43 statements.
[2025-04-28 21:22:06,023 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,023 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,310 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:06,310 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,310 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1670019894]
[2025-04-28 21:22:06,311 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1670019894] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:06,311 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [759535623]
[2025-04-28 21:22:06,311 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,311 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,313 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:06,316 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:22:06,319 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:22:06,469 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 43 statements into 1 equivalence classes.
[2025-04-28 21:22:06,513 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 43 of 43 statements.
[2025-04-28 21:22:06,513 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,513 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,515 INFO  L256         TraceCheckSpWp]: Trace formula consists of 269 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:06,517 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:06,637 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:06,638 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:08,886 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:08,886 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [759535623] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,886 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,886 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 19
[2025-04-28 21:22:08,886 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [572358706]
[2025-04-28 21:22:08,886 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,887 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:22:08,887 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,888 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:22:08,888 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=56, Invalid=286, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:22:08,888 INFO  L87              Difference]: Start difference. First operand 48 states and 57 transitions. Second operand  has 19 states, 9 states have (on average 3.2222222222222223) internal successors, (29), 19 states have internal predecessors, (29), 13 states have call successors, (18), 1 states have call predecessors, (18), 9 states have return successors, (19), 9 states have call predecessors, (19), 13 states have call successors, (19)
[2025-04-28 21:22:09,068 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:09,068 INFO  L93              Difference]: Finished difference Result 52 states and 62 transitions.
[2025-04-28 21:22:09,068 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:09,068 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 3.2222222222222223) internal successors, (29), 19 states have internal predecessors, (29), 13 states have call successors, (18), 1 states have call predecessors, (18), 9 states have return successors, (19), 9 states have call predecessors, (19), 13 states have call successors, (19) Word has length 43
[2025-04-28 21:22:09,069 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:09,069 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:22:09,069 INFO  L226             Difference]: Without dead ends: 44
[2025-04-28 21:22:09,070 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 98 GetRequests, 76 SyntacticMatches, 2 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 75 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=77, Invalid=385, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:09,070 INFO  L437           NwaCegarLoop]: 37 mSDtfsCounter, 9 mSDsluCounter, 373 mSDsCounter, 0 mSdLazyCounter, 129 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 410 SdHoareTripleChecker+Invalid, 132 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 129 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:09,070 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 410 Invalid, 132 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 129 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:09,071 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 44 states.
[2025-04-28 21:22:09,075 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 44 to 42.
[2025-04-28 21:22:09,075 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 18 states have (on average 1.2222222222222223) internal successors, (22), 22 states have internal predecessors, (22), 11 states have call successors, (11), 7 states have call predecessors, (11), 12 states have return successors, (16), 12 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:22:09,075 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 49 transitions.
[2025-04-28 21:22:09,076 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 49 transitions. Word has length 43
[2025-04-28 21:22:09,076 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:09,076 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 49 transitions.
[2025-04-28 21:22:09,076 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 3.2222222222222223) internal successors, (29), 19 states have internal predecessors, (29), 13 states have call successors, (18), 1 states have call predecessors, (18), 9 states have return successors, (19), 9 states have call predecessors, (19), 13 states have call successors, (19)
[2025-04-28 21:22:09,076 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 49 transitions.
[2025-04-28 21:22:09,077 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 48
[2025-04-28 21:22:09,077 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:09,077 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1]
[2025-04-28 21:22:09,083 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:22:09,281 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,281 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,281 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,281 INFO  L85        PathProgramCache]: Analyzing trace with hash 1371471306, now seen corresponding path program 3 times
[2025-04-28 21:22:09,281 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,281 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [435116456]
[2025-04-28 21:22:09,281 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:09,281 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,310 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 47 statements into 3 equivalence classes.
[2025-04-28 21:22:09,336 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 47 of 47 statements.
[2025-04-28 21:22:09,336 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:22:09,336 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,868 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 4 proven. 5 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:09,868 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:09,869 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [435116456]
[2025-04-28 21:22:09,869 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [435116456] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:09,869 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1159468853]
[2025-04-28 21:22:09,869 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:09,869 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,872 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:09,874 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:22:09,876 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:10,056 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 47 statements into 3 equivalence classes.
[2025-04-28 21:22:10,113 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 47 of 47 statements.
[2025-04-28 21:22:10,113 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:22:10,114 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,116 INFO  L256         TraceCheckSpWp]: Trace formula consists of 321 conjuncts, 36 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:10,118 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:10,224 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 4 proven. 5 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:10,224 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
