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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:35,620 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:35,713 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_aad7073e-1b95-4856-a4b9-b1859847efbf/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:35,722 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:35,722 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:35,758 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:35,758 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:35,758 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:35,759 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:35,759 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:35,761 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:35,761 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:35,761 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:35,761 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:35,761 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:35,761 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:35,761 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:35,761 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:35,762 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:35,762 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:35,762 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:35,762 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:35,762 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:35,762 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:35,762 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:35,763 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:35,763 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:36,130 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:36,143 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:36,145 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:36,148 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:36,149 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:36,150 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_aad7073e-1b95-4856-a4b9-b1859847efbf/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-286.smt2
[2025-04-28 21:21:36,154 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:36,157 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:36,344 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_aad7073e-1b95-4856-a4b9-b1859847efbf/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-286.smt2
[2025-04-28 21:21:36,348 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:36,349 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:36,351 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:36,351 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:36,351 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:36,354 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,374 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36 Unit
[2025-04-28 21:21:36,374 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:36,375 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:36,375 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:36,375 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:36,392 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,392 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,413 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,413 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,415 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,415 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,417 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,418 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,418 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,429 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:36,430 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:36,430 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:36,430 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:36,431 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,434 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:36,446 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,462 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:36,466 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:36,478 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:36,478 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:36,478 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:36,478 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fail given in one single declaration
[2025-04-28 21:21:36,478 INFO  L130     BoogieDeclarations]: Found specification of procedure fail
[2025-04-28 21:21:36,479 INFO  L138     BoogieDeclarations]: Found implementation of procedure fail
[2025-04-28 21:21:36,479 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:36,479 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:36,479 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:36,479 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:36,479 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:36,479 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:36,512 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:36,514 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:36,600 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:36,600 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:36,612 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:36,613 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:36,613 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:36 BoogieIcfgContainer
[2025-04-28 21:21:36,614 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:36,616 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:36,616 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:36,620 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:36,621 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:36" (1/3) ...
[2025-04-28 21:21:36,622 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1161b96e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:36, skipping insertion in model container
[2025-04-28 21:21:36,622 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (2/3) ...
[2025-04-28 21:21:36,622 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1161b96e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:36, skipping insertion in model container
[2025-04-28 21:21:36,622 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:36" (3/3) ...
[2025-04-28 21:21:36,624 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:36,640 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:36,643 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 16 locations, 21 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:36,687 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:36,706 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;@233d1861, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:36,707 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:36,712 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:36,719 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:36,719 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,720 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,720 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,726 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,726 INFO  L85        PathProgramCache]: Analyzing trace with hash 812378868, now seen corresponding path program 1 times
[2025-04-28 21:21:36,734 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,735 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [309844943]
[2025-04-28 21:21:36,735 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,736 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,763 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:36,781 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:36,781 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,781 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,897 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:36,898 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,898 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [309844943]
[2025-04-28 21:21:36,899 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [309844943] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,899 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,902 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:36,903 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1135211110]
[2025-04-28 21:21:36,904 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,908 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:36,908 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,934 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:36,934 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:36,936 INFO  L87              Difference]: Start difference. First operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:36,971 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,971 INFO  L93              Difference]: Finished difference Result 16 states and 17 transitions.
[2025-04-28 21:21:36,973 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:36,974 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:36,974 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,980 INFO  L225             Difference]: With dead ends: 16
[2025-04-28 21:21:36,980 INFO  L226             Difference]: Without dead ends: 16
[2025-04-28 21:21:36,982 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:36,985 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 1 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 35 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,985 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 35 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:36,998 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 16 states.
[2025-04-28 21:21:37,014 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 16 to 16.
[2025-04-28 21:21:37,015 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 16 states, 7 states have (on average 1.1428571428571428) internal successors, (8), 8 states have internal predecessors, (8), 4 states have call successors, (4), 3 states have call predecessors, (4), 4 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:37,022 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 16 states to 16 states and 17 transitions.
[2025-04-28 21:21:37,024 INFO  L79                 Accepts]: Start accepts. Automaton has 16 states and 17 transitions. Word has length 12
[2025-04-28 21:21:37,024 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,024 INFO  L485      AbstractCegarLoop]: Abstraction has 16 states and 17 transitions.
[2025-04-28 21:21:37,024 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:37,024 INFO  L278                IsEmpty]: Start isEmpty. Operand 16 states and 17 transitions.
[2025-04-28 21:21:37,026 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:37,026 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,026 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,026 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:37,026 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,027 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,027 INFO  L85        PathProgramCache]: Analyzing trace with hash 1337627512, now seen corresponding path program 1 times
[2025-04-28 21:21:37,027 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,027 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [249866793]
[2025-04-28 21:21:37,027 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,027 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,033 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:37,053 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:37,054 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,054 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,175 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:37,175 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,175 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [249866793]
[2025-04-28 21:21:37,176 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [249866793] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,176 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2130130909]
[2025-04-28 21:21:37,176 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,176 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,179 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,181 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:37,185 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,221 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:37,246 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:37,246 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,246 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,250 INFO  L256         TraceCheckSpWp]: Trace formula consists of 47 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,256 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,391 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:37,391 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:37,744 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:37,744 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2130130909] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:37,744 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:37,744 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:37,746 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1583325372]
[2025-04-28 21:21:37,746 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,746 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:37,747 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,747 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:37,747 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=38, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:37,748 INFO  L87              Difference]: Start difference. First operand 16 states and 17 transitions. Second operand  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:37,841 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,842 INFO  L93              Difference]: Finished difference Result 18 states and 19 transitions.
[2025-04-28 21:21:37,843 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:37,844 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6) Word has length 16
[2025-04-28 21:21:37,845 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,845 INFO  L225             Difference]: With dead ends: 18
[2025-04-28 21:21:37,845 INFO  L226             Difference]: Without dead ends: 18
[2025-04-28 21:21:37,846 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 29 SyntacticMatches, 2 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=49, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:37,849 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 4 mSDsluCounter, 41 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 55 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,849 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 55 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:37,850 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 18 states.
[2025-04-28 21:21:37,852 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 18 to 18.
[2025-04-28 21:21:37,852 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 18 states, 8 states have (on average 1.125) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 5 states have return successors, (6), 5 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:37,853 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 18 states to 18 states and 19 transitions.
[2025-04-28 21:21:37,855 INFO  L79                 Accepts]: Start accepts. Automaton has 18 states and 19 transitions. Word has length 16
[2025-04-28 21:21:37,856 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,856 INFO  L485      AbstractCegarLoop]: Abstraction has 18 states and 19 transitions.
[2025-04-28 21:21:37,856 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:37,857 INFO  L278                IsEmpty]: Start isEmpty. Operand 18 states and 19 transitions.
[2025-04-28 21:21:37,859 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:37,859 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,859 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,871 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:38,059 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,060 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,061 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,061 INFO  L85        PathProgramCache]: Analyzing trace with hash 1410960252, now seen corresponding path program 2 times
[2025-04-28 21:21:38,061 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,061 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1373486842]
[2025-04-28 21:21:38,061 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:38,061 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,072 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:38,090 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:38,093 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:38,093 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,281 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:38,281 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,281 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1373486842]
[2025-04-28 21:21:38,281 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1373486842] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:38,281 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1088772201]
[2025-04-28 21:21:38,282 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:38,282 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,285 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:38,287 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:38,289 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:38,326 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:38,341 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:38,341 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:38,341 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,342 INFO  L256         TraceCheckSpWp]: Trace formula consists of 63 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:38,344 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:38,387 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:38,387 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,989 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:38,991 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1088772201] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,991 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,991 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 10
[2025-04-28 21:21:38,991 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [537258997]
[2025-04-28 21:21:38,992 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,992 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:38,993 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,994 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:38,994 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:38,994 INFO  L87              Difference]: Start difference. First operand 18 states and 19 transitions. Second operand  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:39,058 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,058 INFO  L93              Difference]: Finished difference Result 20 states and 21 transitions.
[2025-04-28 21:21:39,059 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:39,059 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8) Word has length 20
[2025-04-28 21:21:39,059 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,060 INFO  L225             Difference]: With dead ends: 20
[2025-04-28 21:21:39,060 INFO  L226             Difference]: Without dead ends: 20
[2025-04-28 21:21:39,060 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 36 SyntacticMatches, 3 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=42, Invalid=90, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:39,061 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 8 mSDsluCounter, 39 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 53 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,062 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 53 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:39,062 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 20 states.
[2025-04-28 21:21:39,067 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 20 to 20.
[2025-04-28 21:21:39,068 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 20 states, 9 states have (on average 1.1111111111111112) internal successors, (10), 10 states have internal predecessors, (10), 4 states have call successors, (4), 3 states have call predecessors, (4), 6 states have return successors, (7), 6 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:39,068 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 21 transitions.
[2025-04-28 21:21:39,068 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 21 transitions. Word has length 20
[2025-04-28 21:21:39,069 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,069 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 21 transitions.
[2025-04-28 21:21:39,069 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:39,069 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 21 transitions.
[2025-04-28 21:21:39,070 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:39,070 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,070 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,076 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:39,275 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,276 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,276 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,276 INFO  L85        PathProgramCache]: Analyzing trace with hash -1097944320, now seen corresponding path program 3 times
[2025-04-28 21:21:39,276 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,277 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [416117655]
[2025-04-28 21:21:39,277 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:39,277 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,283 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:39,299 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:39,300 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:39,300 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,436 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 12 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:39,436 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,436 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [416117655]
[2025-04-28 21:21:39,436 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [416117655] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,437 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1581650631]
[2025-04-28 21:21:39,437 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:39,437 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,439 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,441 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:39,445 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,482 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:39,501 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:39,502 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:39,502 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,502 INFO  L256         TraceCheckSpWp]: Trace formula consists of 79 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,504 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,555 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 12 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:39,555 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,519 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 15 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:40,520 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1581650631] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,520 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,521 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 10] total 12
[2025-04-28 21:21:40,521 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2126061888]
[2025-04-28 21:21:40,521 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,521 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:40,521 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,523 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:40,523 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=92, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:40,524 INFO  L87              Difference]: Start difference. First operand 20 states and 21 transitions. Second operand  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:40,614 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,615 INFO  L93              Difference]: Finished difference Result 22 states and 23 transitions.
[2025-04-28 21:21:40,617 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:40,617 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10) Word has length 24
[2025-04-28 21:21:40,617 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,618 INFO  L225             Difference]: With dead ends: 22
[2025-04-28 21:21:40,619 INFO  L226             Difference]: Without dead ends: 22
[2025-04-28 21:21:40,619 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 60 GetRequests, 43 SyntacticMatches, 4 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 35 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=67, Invalid=143, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:40,620 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 6 mSDsluCounter, 64 mSDsCounter, 0 mSdLazyCounter, 33 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 78 SdHoareTripleChecker+Invalid, 34 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 33 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,622 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 78 Invalid, 34 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 33 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:40,623 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 22 states.
[2025-04-28 21:21:40,629 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 22 to 22.
[2025-04-28 21:21:40,629 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 10 states have (on average 1.1) internal successors, (11), 11 states have internal predecessors, (11), 4 states have call successors, (4), 3 states have call predecessors, (4), 7 states have return successors, (8), 7 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:40,630 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 23 transitions.
[2025-04-28 21:21:40,632 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 23 transitions. Word has length 24
[2025-04-28 21:21:40,632 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,632 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 23 transitions.
[2025-04-28 21:21:40,632 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:40,633 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 23 transitions.
[2025-04-28 21:21:40,633 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:40,633 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,633 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,639 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:40,834 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,834 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,835 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,835 INFO  L85        PathProgramCache]: Analyzing trace with hash 306702852, now seen corresponding path program 4 times
[2025-04-28 21:21:40,835 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,835 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [724747280]
[2025-04-28 21:21:40,835 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:40,835 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,841 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:40,854 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:40,855 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:40,855 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,095 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 23 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:41,095 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,095 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [724747280]
[2025-04-28 21:21:41,095 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [724747280] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,095 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1477305319]
[2025-04-28 21:21:41,096 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:41,096 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,099 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,102 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:41,105 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,152 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:41,175 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:41,175 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:41,175 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,176 INFO  L256         TraceCheckSpWp]: Trace formula consists of 95 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,178 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,221 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:41,221 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:42,652 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 26 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:42,653 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1477305319] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:42,653 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:42,653 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 12] total 15
[2025-04-28 21:21:42,653 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [728399369]
[2025-04-28 21:21:42,653 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,654 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:42,654 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,655 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:42,655 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=61, Invalid=149, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:42,656 INFO  L87              Difference]: Start difference. First operand 22 states and 23 transitions. Second operand  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (13), 5 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:42,766 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,766 INFO  L93              Difference]: Finished difference Result 24 states and 25 transitions.
[2025-04-28 21:21:42,767 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:42,767 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (13), 5 states have call predecessors, (13), 9 states have call successors, (13) Word has length 28
[2025-04-28 21:21:42,768 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,768 INFO  L225             Difference]: With dead ends: 24
[2025-04-28 21:21:42,768 INFO  L226             Difference]: Without dead ends: 24
[2025-04-28 21:21:42,769 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 71 GetRequests, 49 SyntacticMatches, 5 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 69 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=109, Invalid=233, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:42,769 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 15 mSDsluCounter, 76 mSDsCounter, 0 mSdLazyCounter, 36 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 90 SdHoareTripleChecker+Invalid, 47 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 36 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,770 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 90 Invalid, 47 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 36 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:42,771 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 24 states.
[2025-04-28 21:21:42,773 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 24 to 24.
[2025-04-28 21:21:42,774 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 4 states have call successors, (4), 3 states have call predecessors, (4), 8 states have return successors, (9), 8 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:42,774 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 25 transitions.
[2025-04-28 21:21:42,775 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 25 transitions. Word has length 28
[2025-04-28 21:21:42,775 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,775 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 25 transitions.
[2025-04-28 21:21:42,775 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (13), 5 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:42,775 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 25 transitions.
[2025-04-28 21:21:42,776 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:42,776 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,776 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,782 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:42,977 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:21:42,977 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,977 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,978 INFO  L85        PathProgramCache]: Analyzing trace with hash -627371896, now seen corresponding path program 5 times
[2025-04-28 21:21:42,978 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,978 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [494498348]
[2025-04-28 21:21:42,978 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:42,978 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,984 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 32 statements into 6 equivalence classes.
[2025-04-28 21:21:43,014 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:43,014 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:43,015 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,219 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 30 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:43,219 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,219 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [494498348]
[2025-04-28 21:21:43,219 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [494498348] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,220 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [314788189]
[2025-04-28 21:21:43,220 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:43,220 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,222 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,224 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,228 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,280 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 32 statements into 6 equivalence classes.
[2025-04-28 21:21:43,301 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:43,301 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:43,301 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,303 INFO  L256         TraceCheckSpWp]: Trace formula consists of 111 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,304 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,365 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 30 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:43,366 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,301 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 40 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:45,301 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [314788189] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,302 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,302 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 14] total 16
[2025-04-28 21:21:45,302 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [339946257]
[2025-04-28 21:21:45,302 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,302 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:45,303 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,303 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:45,303 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=70, Invalid=170, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:45,304 INFO  L87              Difference]: Start difference. First operand 24 states and 25 transitions. Second operand  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (14), 6 states have call predecessors, (14), 9 states have call successors, (14)
[2025-04-28 21:21:45,417 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,417 INFO  L93              Difference]: Finished difference Result 26 states and 27 transitions.
[2025-04-28 21:21:45,418 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:45,418 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (14), 6 states have call predecessors, (14), 9 states have call successors, (14) Word has length 32
[2025-04-28 21:21:45,418 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,420 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:45,420 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:45,420 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 82 GetRequests, 57 SyntacticMatches, 6 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 87 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=135, Invalid=285, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:45,421 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 15 mSDsluCounter, 66 mSDsCounter, 0 mSdLazyCounter, 36 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 80 SdHoareTripleChecker+Invalid, 47 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 36 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,421 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 80 Invalid, 47 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 36 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,422 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:45,427 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:45,429 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.0833333333333333) internal successors, (13), 13 states have internal predecessors, (13), 4 states have call successors, (4), 3 states have call predecessors, (4), 9 states have return successors, (10), 9 states have call predecessors, (10), 4 states have call successors, (10)
[2025-04-28 21:21:45,430 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 27 transitions.
[2025-04-28 21:21:45,430 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 27 transitions. Word has length 32
[2025-04-28 21:21:45,430 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,430 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 27 transitions.
[2025-04-28 21:21:45,431 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (14), 6 states have call predecessors, (14), 9 states have call successors, (14)
[2025-04-28 21:21:45,431 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 27 transitions.
[2025-04-28 21:21:45,432 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:45,433 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,433 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,439 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:45,634 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,634 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,634 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,634 INFO  L85        PathProgramCache]: Analyzing trace with hash 822478476, now seen corresponding path program 6 times
[2025-04-28 21:21:45,635 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,635 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [743664747]
[2025-04-28 21:21:45,635 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:45,635 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,640 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:45,658 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:45,658 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:45,658 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,856 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 3 proven. 44 refuted. 0 times theorem prover too weak. 31 trivial. 0 not checked.
[2025-04-28 21:21:45,856 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,856 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [743664747]
[2025-04-28 21:21:45,856 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [743664747] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,856 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [399132792]
[2025-04-28 21:21:45,856 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:45,856 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,859 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,861 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:45,864 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,938 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:45,958 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:45,958 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:45,958 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,959 INFO  L256         TraceCheckSpWp]: Trace formula consists of 127 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,961 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,024 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 42 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:46,024 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,738 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 57 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:21:48,739 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [399132792] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,739 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,739 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 16] total 19
[2025-04-28 21:21:48,739 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [490708895]
[2025-04-28 21:21:48,739 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,740 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:48,740 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,741 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:48,741 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=97, Invalid=245, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:48,741 INFO  L87              Difference]: Start difference. First operand 26 states and 27 transitions. Second operand  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (17), 7 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:48,880 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,880 INFO  L93              Difference]: Finished difference Result 28 states and 29 transitions.
[2025-04-28 21:21:48,881 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:48,882 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (17), 7 states have call predecessors, (17), 11 states have call successors, (17) Word has length 36
[2025-04-28 21:21:48,882 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,883 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:48,883 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:48,883 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 93 GetRequests, 63 SyntacticMatches, 7 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 149 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=193, Invalid=407, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:48,884 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 26 mSDsluCounter, 76 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 35 SdHoareTripleChecker+Valid, 90 SdHoareTripleChecker+Invalid, 63 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,884 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [35 Valid, 90 Invalid, 63 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:48,885 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:48,889 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 28.
[2025-04-28 21:21:48,889 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 4 states have call successors, (4), 3 states have call predecessors, (4), 10 states have return successors, (11), 10 states have call predecessors, (11), 4 states have call successors, (11)
[2025-04-28 21:21:48,890 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 29 transitions.
[2025-04-28 21:21:48,890 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 29 transitions. Word has length 36
[2025-04-28 21:21:48,891 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,891 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 29 transitions.
[2025-04-28 21:21:48,891 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (17), 7 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:48,891 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 29 transitions.
[2025-04-28 21:21:48,892 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:48,892 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,892 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,897 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:49,093 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,093 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,093 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,094 INFO  L85        PathProgramCache]: Analyzing trace with hash -1020351472, now seen corresponding path program 7 times
[2025-04-28 21:21:49,094 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,094 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1470288667]
[2025-04-28 21:21:49,094 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:49,094 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,100 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:49,109 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:49,110 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,110 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,367 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 56 refuted. 0 times theorem prover too weak. 49 trivial. 0 not checked.
[2025-04-28 21:21:49,368 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,368 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1470288667]
[2025-04-28 21:21:49,368 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1470288667] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:49,368 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [949191359]
[2025-04-28 21:21:49,368 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:49,368 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,371 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,373 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:49,377 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,473 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:49,497 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:49,498 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,498 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,499 INFO  L256         TraceCheckSpWp]: Trace formula consists of 143 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:49,501 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:49,559 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 56 refuted. 0 times theorem prover too weak. 49 trivial. 0 not checked.
[2025-04-28 21:21:49,559 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,025 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 77 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:21:53,026 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [949191359] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,026 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,026 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 18] total 20
[2025-04-28 21:21:53,026 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1597601653]
[2025-04-28 21:21:53,026 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,027 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:53,027 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,028 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:53,028 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=108, Invalid=272, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:53,028 INFO  L87              Difference]: Start difference. First operand 28 states and 29 transitions. Second operand  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (18), 8 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:21:53,158 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,158 INFO  L93              Difference]: Finished difference Result 30 states and 31 transitions.
[2025-04-28 21:21:53,159 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:53,159 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (18), 8 states have call predecessors, (18), 11 states have call successors, (18) Word has length 40
[2025-04-28 21:21:53,160 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,160 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:53,160 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:53,161 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 104 GetRequests, 71 SyntacticMatches, 8 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 163 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=227, Invalid=475, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:53,161 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 16 mSDsluCounter, 95 mSDsCounter, 0 mSdLazyCounter, 48 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 109 SdHoareTripleChecker+Invalid, 58 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 48 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,162 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 109 Invalid, 58 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 48 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:53,162 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:53,165 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 30.
[2025-04-28 21:21:53,165 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 30 states, 14 states have (on average 1.0714285714285714) internal successors, (15), 15 states have internal predecessors, (15), 4 states have call successors, (4), 3 states have call predecessors, (4), 11 states have return successors, (12), 11 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:53,166 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 31 transitions.
[2025-04-28 21:21:53,166 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 31 transitions. Word has length 40
[2025-04-28 21:21:53,166 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,166 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 31 transitions.
[2025-04-28 21:21:53,166 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (18), 8 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:21:53,166 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 31 transitions.
[2025-04-28 21:21:53,167 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:53,167 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,167 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,172 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:53,370 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable8
[2025-04-28 21:21:53,370 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,371 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,371 INFO  L85        PathProgramCache]: Analyzing trace with hash 1491263764, now seen corresponding path program 8 times
[2025-04-28 21:21:53,371 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,371 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [734061441]
[2025-04-28 21:21:53,371 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:53,371 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,377 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 44 statements into 2 equivalence classes.
[2025-04-28 21:21:53,390 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:53,391 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:53,391 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,686 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 64 trivial. 0 not checked.
[2025-04-28 21:21:53,686 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,686 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [734061441]
[2025-04-28 21:21:53,686 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [734061441] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,686 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1246816066]
[2025-04-28 21:21:53,686 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:53,686 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,689 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,691 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:53,696 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,832 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 44 statements into 2 equivalence classes.
[2025-04-28 21:21:53,855 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:53,856 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:53,856 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,857 INFO  L256         TraceCheckSpWp]: Trace formula consists of 159 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,859 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,922 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 64 trivial. 0 not checked.
[2025-04-28 21:21:53,922 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,679 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 100 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:58,679 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1246816066] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:58,679 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:58,679 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 20] total 22
[2025-04-28 21:21:58,679 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1623547818]
[2025-04-28 21:21:58,679 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,680 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:58,680 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,680 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:58,681 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=130, Invalid=332, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:58,681 INFO  L87              Difference]: Start difference. First operand 30 states and 31 transitions. Second operand  has 22 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 21 states have internal predecessors, (24), 12 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 12 states have call successors, (20)
[2025-04-28 21:21:58,842 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,843 INFO  L93              Difference]: Finished difference Result 32 states and 33 transitions.
[2025-04-28 21:21:58,845 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:58,846 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 21 states have internal predecessors, (24), 12 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 12 states have call successors, (20) Word has length 44
[2025-04-28 21:21:58,846 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,847 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:58,847 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:58,847 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 115 GetRequests, 78 SyntacticMatches, 9 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 210 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=282, Invalid=588, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:58,848 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 38 mSDsluCounter, 96 mSDsCounter, 0 mSdLazyCounter, 46 mSolverCounterSat, 35 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 49 SdHoareTripleChecker+Valid, 110 SdHoareTripleChecker+Invalid, 81 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 35 IncrementalHoareTripleChecker+Valid, 46 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,848 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [49 Valid, 110 Invalid, 81 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [35 Valid, 46 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:58,852 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:58,856 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:21:58,856 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 15 states have (on average 1.0666666666666667) internal successors, (16), 16 states have internal predecessors, (16), 4 states have call successors, (4), 3 states have call predecessors, (4), 12 states have return successors, (13), 12 states have call predecessors, (13), 4 states have call successors, (13)
[2025-04-28 21:21:58,857 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 33 transitions.
[2025-04-28 21:21:58,857 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 33 transitions. Word has length 44
[2025-04-28 21:21:58,857 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,858 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 33 transitions.
[2025-04-28 21:21:58,858 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 21 states have internal predecessors, (24), 12 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 12 states have call successors, (20)
[2025-04-28 21:21:58,858 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 33 transitions.
[2025-04-28 21:21:58,859 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:21:58,859 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,859 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,868 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:59,065 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:21:59,066 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,066 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,066 INFO  L85        PathProgramCache]: Analyzing trace with hash -635927144, now seen corresponding path program 9 times
[2025-04-28 21:21:59,066 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,066 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1292256474]
[2025-04-28 21:21:59,066 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:59,066 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,073 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 10 equivalence classes.
[2025-04-28 21:21:59,095 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:59,095 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:59,095 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,340 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:21:59,341 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,341 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1292256474]
[2025-04-28 21:21:59,341 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1292256474] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:59,341 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [369714972]
[2025-04-28 21:21:59,341 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:59,341 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,344 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:59,346 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:59,350 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:59,546 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 10 equivalence classes.
[2025-04-28 21:21:59,580 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:59,580 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:59,581 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,582 INFO  L256         TraceCheckSpWp]: Trace formula consists of 175 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:59,584 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:59,645 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:21:59,645 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:06,126 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 126 refuted. 0 times theorem prover too weak. 45 trivial. 0 not checked.
[2025-04-28 21:22:06,126 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [369714972] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:06,126 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:06,126 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 22] total 24
[2025-04-28 21:22:06,126 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1303139600]
[2025-04-28 21:22:06,127 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:06,127 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:22:06,127 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:06,128 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:22:06,128 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=154, Invalid=398, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:22:06,129 INFO  L87              Difference]: Start difference. First operand 32 states and 33 transitions. Second operand  has 24 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 23 states have internal predecessors, (26), 13 states have call successors, (14), 1 states have call predecessors, (14), 11 states have return successors, (22), 10 states have call predecessors, (22), 13 states have call successors, (22)
[2025-04-28 21:22:06,310 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,310 INFO  L93              Difference]: Finished difference Result 34 states and 35 transitions.
[2025-04-28 21:22:06,312 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:22:06,313 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 23 states have internal predecessors, (26), 13 states have call successors, (14), 1 states have call predecessors, (14), 11 states have return successors, (22), 10 states have call predecessors, (22), 13 states have call successors, (22) Word has length 48
[2025-04-28 21:22:06,313 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,314 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:22:06,314 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:22:06,315 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 126 GetRequests, 85 SyntacticMatches, 10 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 263 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=343, Invalid=713, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:06,316 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 41 mSDsluCounter, 118 mSDsCounter, 0 mSdLazyCounter, 58 mSolverCounterSat, 35 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 53 SdHoareTripleChecker+Valid, 132 SdHoareTripleChecker+Invalid, 93 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 35 IncrementalHoareTripleChecker+Valid, 58 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,317 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [53 Valid, 132 Invalid, 93 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [35 Valid, 58 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:06,318 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:22:06,321 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 34.
[2025-04-28 21:22:06,324 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 16 states have (on average 1.0625) internal successors, (17), 17 states have internal predecessors, (17), 4 states have call successors, (4), 3 states have call predecessors, (4), 13 states have return successors, (14), 13 states have call predecessors, (14), 4 states have call successors, (14)
[2025-04-28 21:22:06,325 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 35 transitions.
[2025-04-28 21:22:06,326 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 35 transitions. Word has length 48
[2025-04-28 21:22:06,326 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,326 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 35 transitions.
[2025-04-28 21:22:06,326 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 23 states have internal predecessors, (26), 13 states have call successors, (14), 1 states have call predecessors, (14), 11 states have return successors, (22), 10 states have call predecessors, (22), 13 states have call successors, (22)
[2025-04-28 21:22:06,327 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 35 transitions.
[2025-04-28 21:22:06,327 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:22:06,331 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,331 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:06,337 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:06,531 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable10
[2025-04-28 21:22:06,532 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,532 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,533 INFO  L85        PathProgramCache]: Analyzing trace with hash -722634340, now seen corresponding path program 10 times
[2025-04-28 21:22:06,533 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,533 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [293450658]
[2025-04-28 21:22:06,533 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:06,533 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,545 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 52 statements into 2 equivalence classes.
[2025-04-28 21:22:06,566 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:22:06,566 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:06,567 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,869 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 119 refuted. 0 times theorem prover too weak. 91 trivial. 0 not checked.
[2025-04-28 21:22:06,869 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,869 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [293450658]
[2025-04-28 21:22:06,870 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [293450658] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:06,870 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1218260058]
[2025-04-28 21:22:06,870 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:06,870 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,872 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:06,874 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:06,879 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,181 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 52 statements into 2 equivalence classes.
[2025-04-28 21:22:07,217 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:22:07,217 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:07,217 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,220 INFO  L256         TraceCheckSpWp]: Trace formula consists of 191 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,222 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:07,295 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:22:07,296 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
