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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:45,504 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:45,592 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4f2145e3-0c20-4a3e-ba86-dd9e7d48383d/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:45,596 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:45,597 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:45,631 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:45,631 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:45,631 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:45,632 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:45,632 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:45,632 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:45,633 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:45,633 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:45,633 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:45,634 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:45,634 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:45,634 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:45,634 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:45,635 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:45,635 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:45,635 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:45,635 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:45,635 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:45,635 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:45,635 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:45,636 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:45,636 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:45,967 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:45,977 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:45,980 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:45,983 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:45,984 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:45,985 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4f2145e3-0c20-4a3e-ba86-dd9e7d48383d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-130.smt2
[2025-04-28 21:21:45,988 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:45,992 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:46,235 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4f2145e3-0c20-4a3e-ba86-dd9e7d48383d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-130.smt2
[2025-04-28 21:21:46,240 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:46,243 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:46,245 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:46,245 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:46,246 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:46,249 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,288 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46 Unit
[2025-04-28 21:21:46,290 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:46,291 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:46,292 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:46,292 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:46,309 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,309 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,331 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,331 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,334 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,335 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,337 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,338 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,339 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,349 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:46,350 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:46,350 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:46,350 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:46,354 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (1/1) ...
[2025-04-28 21:21:46,361 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:46,374 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,389 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:46,392 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:46,404 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:46,404 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:46,405 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:46,405 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure END_QUERY given in one single declaration
[2025-04-28 21:21:46,405 INFO  L130     BoogieDeclarations]: Found specification of procedure END_QUERY
[2025-04-28 21:21:46,405 INFO  L138     BoogieDeclarations]: Found implementation of procedure END_QUERY
[2025-04-28 21:21:46,405 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_0 given in one single declaration
[2025-04-28 21:21:46,405 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_0
[2025-04-28 21:21:46,405 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_0
[2025-04-28 21:21:46,405 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:46,405 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:46,405 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:46,405 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:46,406 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:46,406 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:46,470 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:46,472 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:46,680 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:46,680 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:46,697 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:46,698 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:46,698 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:46 BoogieIcfgContainer
[2025-04-28 21:21:46,700 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:46,702 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:46,702 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:46,706 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:46,707 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:46" (1/3) ...
[2025-04-28 21:21:46,708 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@49e4db8e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:46, skipping insertion in model container
[2025-04-28 21:21:46,708 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:46" (2/3) ...
[2025-04-28 21:21:46,709 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@49e4db8e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:46, skipping insertion in model container
[2025-04-28 21:21:46,709 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:46" (3/3) ...
[2025-04-28 21:21:46,713 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:46,730 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:46,732 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 5 procedures, 28 locations, 58 edges, 5 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:46,792 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:46,805 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;@37342842, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:46,806 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:46,811 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 28 states, 9 states have (on average 2.111111111111111) internal successors, (19), 19 states have internal predecessors, (19), 13 states have call successors, (13), 4 states have call predecessors, (13), 4 states have return successors, (13), 5 states have call predecessors, (13), 13 states have call successors, (13)
[2025-04-28 21:21:46,820 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:46,820 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,821 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,821 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,828 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,829 INFO  L85        PathProgramCache]: Analyzing trace with hash 791684326, now seen corresponding path program 1 times
[2025-04-28 21:21:46,838 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,839 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [801381927]
[2025-04-28 21:21:46,839 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,840 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,869 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:46,880 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:46,881 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,881 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,102 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:47,104 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,104 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [801381927]
[2025-04-28 21:21:47,105 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [801381927] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,105 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,111 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:47,113 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [867467283]
[2025-04-28 21:21:47,113 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,121 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:47,124 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,158 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:47,159 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:47,162 INFO  L87              Difference]: Start difference. First operand  has 28 states, 9 states have (on average 2.111111111111111) internal successors, (19), 19 states have internal predecessors, (19), 13 states have call successors, (13), 4 states have call predecessors, (13), 4 states have return successors, (13), 5 states have call predecessors, (13), 13 states have call successors, (13) 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:47,241 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,241 INFO  L93              Difference]: Finished difference Result 30 states and 48 transitions.
[2025-04-28 21:21:47,243 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:47,244 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:47,245 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,251 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:47,251 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:47,253 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:47,257 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 1 mSDsluCounter, 71 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 114 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,257 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 114 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:47,272 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:47,300 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 28.
[2025-04-28 21:21:47,301 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 9 states have (on average 2.0) internal successors, (18), 18 states have internal predecessors, (18), 13 states have call successors, (13), 4 states have call predecessors, (13), 5 states have return successors, (15), 5 states have call predecessors, (15), 13 states have call successors, (15)
[2025-04-28 21:21:47,311 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 46 transitions.
[2025-04-28 21:21:47,312 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 46 transitions. Word has length 12
[2025-04-28 21:21:47,313 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,313 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 46 transitions.
[2025-04-28 21:21:47,316 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:47,316 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 46 transitions.
[2025-04-28 21:21:47,319 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:47,319 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,319 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,320 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:47,320 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,321 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,321 INFO  L85        PathProgramCache]: Analyzing trace with hash 1036935179, now seen corresponding path program 1 times
[2025-04-28 21:21:47,321 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,321 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [613313264]
[2025-04-28 21:21:47,321 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,321 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,326 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:47,329 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:47,329 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,329 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,423 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:47,423 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,424 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [613313264]
[2025-04-28 21:21:47,424 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [613313264] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,424 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,424 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:47,424 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [337279624]
[2025-04-28 21:21:47,424 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,425 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:47,426 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,426 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:47,427 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:47,427 INFO  L87              Difference]: Start difference. First operand 28 states and 46 transitions. 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:47,461 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,461 INFO  L93              Difference]: Finished difference Result 30 states and 47 transitions.
[2025-04-28 21:21:47,462 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:47,462 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:47,462 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,463 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:47,463 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:47,464 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:47,465 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 1 mSDsluCounter, 75 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 119 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,465 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 119 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:47,466 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:47,471 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 28.
[2025-04-28 21:21:47,471 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 9 states have (on average 2.0) internal successors, (18), 18 states have internal predecessors, (18), 13 states have call successors, (13), 4 states have call predecessors, (13), 5 states have return successors, (14), 5 states have call predecessors, (14), 13 states have call successors, (14)
[2025-04-28 21:21:47,472 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 45 transitions.
[2025-04-28 21:21:47,473 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 45 transitions. Word has length 12
[2025-04-28 21:21:47,473 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,473 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 45 transitions.
[2025-04-28 21:21:47,473 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:47,473 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 45 transitions.
[2025-04-28 21:21:47,474 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:47,475 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,475 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,475 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:47,475 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,476 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,476 INFO  L85        PathProgramCache]: Analyzing trace with hash -59671202, now seen corresponding path program 1 times
[2025-04-28 21:21:47,476 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,476 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1961744119]
[2025-04-28 21:21:47,476 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,476 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,482 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:47,561 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:47,562 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,562 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,073 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:48,077 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,078 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1961744119]
[2025-04-28 21:21:48,078 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1961744119] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,078 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,078 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:48,078 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [977162293]
[2025-04-28 21:21:48,078 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,078 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:48,079 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,079 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:48,079 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:48,080 INFO  L87              Difference]: Start difference. First operand 28 states and 45 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:48,336 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,336 INFO  L93              Difference]: Finished difference Result 36 states and 67 transitions.
[2025-04-28 21:21:48,336 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:48,337 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:48,337 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,338 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:48,338 INFO  L226             Difference]: Without dead ends: 36
[2025-04-28 21:21:48,338 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:48,339 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 3 mSDsluCounter, 107 mSDsCounter, 0 mSdLazyCounter, 83 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 142 SdHoareTripleChecker+Invalid, 84 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 83 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,340 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 142 Invalid, 84 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 83 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:48,341 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 36 states.
[2025-04-28 21:21:48,349 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 36 to 32.
[2025-04-28 21:21:48,350 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 11 states have (on average 1.8181818181818181) internal successors, (20), 20 states have internal predecessors, (20), 13 states have call successors, (13), 4 states have call predecessors, (13), 7 states have return successors, (24), 7 states have call predecessors, (24), 13 states have call successors, (24)
[2025-04-28 21:21:48,351 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 57 transitions.
[2025-04-28 21:21:48,351 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 57 transitions. Word has length 16
[2025-04-28 21:21:48,351 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,351 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 57 transitions.
[2025-04-28 21:21:48,351 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:48,352 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 57 transitions.
[2025-04-28 21:21:48,353 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:48,353 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,353 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,353 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:48,354 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,354 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,354 INFO  L85        PathProgramCache]: Analyzing trace with hash 1986552385, now seen corresponding path program 1 times
[2025-04-28 21:21:48,355 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,355 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [985675216]
[2025-04-28 21:21:48,355 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,355 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,360 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:48,366 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:48,366 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,366 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,597 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:48,598 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,598 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [985675216]
[2025-04-28 21:21:48,598 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [985675216] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,598 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,598 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:48,598 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [693898179]
[2025-04-28 21:21:48,598 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,599 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:48,599 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,599 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:48,599 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:48,600 INFO  L87              Difference]: Start difference. First operand 32 states and 57 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:48,795 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,796 INFO  L93              Difference]: Finished difference Result 40 states and 80 transitions.
[2025-04-28 21:21:48,797 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:48,797 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:48,798 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,799 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:21:48,802 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:21:48,802 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:48,803 INFO  L437           NwaCegarLoop]: 37 mSDtfsCounter, 3 mSDsluCounter, 113 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 150 SdHoareTripleChecker+Invalid, 80 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,803 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 150 Invalid, 80 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:48,804 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:21:48,821 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 36.
[2025-04-28 21:21:48,821 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 13 states have (on average 1.6923076923076923) internal successors, (22), 22 states have internal predecessors, (22), 13 states have call successors, (13), 4 states have call predecessors, (13), 9 states have return successors, (35), 9 states have call predecessors, (35), 13 states have call successors, (35)
[2025-04-28 21:21:48,822 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 70 transitions.
[2025-04-28 21:21:48,826 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 70 transitions. Word has length 16
[2025-04-28 21:21:48,826 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,826 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 70 transitions.
[2025-04-28 21:21:48,826 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:48,827 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 70 transitions.
[2025-04-28 21:21:48,828 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:48,828 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,828 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,828 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:48,829 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,829 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,832 INFO  L85        PathProgramCache]: Analyzing trace with hash -488700533, now seen corresponding path program 1 times
[2025-04-28 21:21:48,832 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,832 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1483014907]
[2025-04-28 21:21:48,832 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,833 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,838 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:48,844 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:48,844 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,844 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,043 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:49,043 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,043 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1483014907]
[2025-04-28 21:21:49,043 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1483014907] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,043 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,043 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:49,043 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [310698935]
[2025-04-28 21:21:49,044 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,044 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:49,044 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,045 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:49,045 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:49,045 INFO  L87              Difference]: Start difference. First operand 36 states and 70 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:49,237 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,237 INFO  L93              Difference]: Finished difference Result 40 states and 78 transitions.
[2025-04-28 21:21:49,237 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:49,238 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:49,238 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,239 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:21:49,239 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:21:49,239 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:49,240 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 3 mSDsluCounter, 110 mSDsCounter, 0 mSdLazyCounter, 84 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 146 SdHoareTripleChecker+Invalid, 85 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 84 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,241 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 146 Invalid, 85 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 84 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:49,246 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:21:49,257 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 36.
[2025-04-28 21:21:49,257 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 13 states have (on average 1.6923076923076923) internal successors, (22), 22 states have internal predecessors, (22), 13 states have call successors, (13), 4 states have call predecessors, (13), 9 states have return successors, (33), 9 states have call predecessors, (33), 13 states have call successors, (33)
[2025-04-28 21:21:49,258 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 68 transitions.
[2025-04-28 21:21:49,258 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 68 transitions. Word has length 16
[2025-04-28 21:21:49,258 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,258 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 68 transitions.
[2025-04-28 21:21:49,259 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:49,259 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 68 transitions.
[2025-04-28 21:21:49,260 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:49,260 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,260 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,260 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:49,261 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,261 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,261 INFO  L85        PathProgramCache]: Analyzing trace with hash 315022568, now seen corresponding path program 1 times
[2025-04-28 21:21:49,261 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,261 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1492408968]
[2025-04-28 21:21:49,261 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,262 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,267 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:49,271 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:49,271 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,271 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,561 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:49,561 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,562 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1492408968]
[2025-04-28 21:21:49,562 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1492408968] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,562 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,562 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:49,562 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1124661434]
[2025-04-28 21:21:49,562 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,562 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:49,562 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,563 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:49,563 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:49,563 INFO  L87              Difference]: Start difference. First operand 36 states and 68 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:49,703 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,703 INFO  L93              Difference]: Finished difference Result 36 states and 64 transitions.
[2025-04-28 21:21:49,704 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:49,704 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:49,704 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,705 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:49,705 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:49,706 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=16, Invalid=40, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:49,706 INFO  L437           NwaCegarLoop]: 33 mSDtfsCounter, 1 mSDsluCounter, 99 mSDsCounter, 0 mSdLazyCounter, 68 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 132 SdHoareTripleChecker+Invalid, 76 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 68 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,707 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 132 Invalid, 76 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 68 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:49,707 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:49,712 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 34.
[2025-04-28 21:21:49,712 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 13 states have (on average 1.5384615384615385) internal successors, (20), 20 states have internal predecessors, (20), 11 states have call successors, (11), 4 states have call predecessors, (11), 9 states have return successors, (29), 9 states have call predecessors, (29), 11 states have call successors, (29)
[2025-04-28 21:21:49,713 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 60 transitions.
[2025-04-28 21:21:49,713 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 60 transitions. Word has length 20
[2025-04-28 21:21:49,713 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,713 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 60 transitions.
[2025-04-28 21:21:49,714 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:49,714 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 60 transitions.
[2025-04-28 21:21:49,715 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:49,715 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,715 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,715 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:49,715 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,716 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,716 INFO  L85        PathProgramCache]: Analyzing trace with hash -1610459817, now seen corresponding path program 1 times
[2025-04-28 21:21:49,716 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,716 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [535128721]
[2025-04-28 21:21:49,716 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,716 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,724 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:49,731 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:49,731 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,731 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,797 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:49,797 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,797 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [535128721]
[2025-04-28 21:21:49,797 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [535128721] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,797 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,797 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:49,797 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1172983722]
[2025-04-28 21:21:49,797 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,797 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:49,798 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,798 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:49,798 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:49,798 INFO  L87              Difference]: Start difference. First operand 34 states and 60 transitions. Second operand  has 5 states, 4 states have (on average 2.25) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:49,878 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,878 INFO  L93              Difference]: Finished difference Result 34 states and 58 transitions.
[2025-04-28 21:21:49,879 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:49,879 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 2.25) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 20
[2025-04-28 21:21:49,880 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,881 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:49,881 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:21:49,881 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:49,882 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 0 mSDsluCounter, 64 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 92 SdHoareTripleChecker+Invalid, 46 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,882 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 92 Invalid, 46 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:49,886 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:21:49,894 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 33.
[2025-04-28 21:21:49,894 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 13 states have (on average 1.4615384615384615) internal successors, (19), 19 states have internal predecessors, (19), 10 states have call successors, (10), 4 states have call predecessors, (10), 9 states have return successors, (27), 9 states have call predecessors, (27), 10 states have call successors, (27)
[2025-04-28 21:21:49,895 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 56 transitions.
[2025-04-28 21:21:49,895 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 56 transitions. Word has length 20
[2025-04-28 21:21:49,895 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,895 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 56 transitions.
[2025-04-28 21:21:49,895 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 2.25) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:49,895 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 56 transitions.
[2025-04-28 21:21:49,896 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:49,896 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,898 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,898 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:49,898 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,899 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,899 INFO  L85        PathProgramCache]: Analyzing trace with hash 1254294029, now seen corresponding path program 1 times
[2025-04-28 21:21:49,900 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,900 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1384865574]
[2025-04-28 21:21:49,900 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,900 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,908 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:49,920 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:49,921 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,921 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,246 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:50,246 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,246 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1384865574]
[2025-04-28 21:21:50,246 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1384865574] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,246 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [409968816]
[2025-04-28 21:21:50,246 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,246 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,249 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,251 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:50,256 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,294 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:50,315 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:50,315 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,315 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,322 WARN  L254         TraceCheckSpWp]: Trace formula consists of 92 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,327 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,570 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:50,571 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,468 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:52,468 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [409968816] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,469 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:52,469 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [8, 8] total 15
[2025-04-28 21:21:52,469 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1840203506]
[2025-04-28 21:21:52,469 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,469 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:52,470 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,470 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:52,470 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=168, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:52,471 INFO  L87              Difference]: Start difference. First operand 33 states and 56 transitions. Second operand  has 8 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:52,686 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,686 INFO  L93              Difference]: Finished difference Result 43 states and 87 transitions.
[2025-04-28 21:21:52,687 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:52,687 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:52,687 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,688 INFO  L225             Difference]: With dead ends: 43
[2025-04-28 21:21:52,688 INFO  L226             Difference]: Without dead ends: 43
[2025-04-28 21:21:52,689 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 47 GetRequests, 34 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 12 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=42, Invalid=168, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:52,689 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 3 mSDsluCounter, 104 mSDsCounter, 0 mSdLazyCounter, 124 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 133 SdHoareTripleChecker+Invalid, 126 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 124 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,690 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 133 Invalid, 126 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 124 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:52,690 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 43 states.
[2025-04-28 21:21:52,705 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 43 to 35.
[2025-04-28 21:21:52,706 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 14 states have (on average 1.4285714285714286) internal successors, (20), 20 states have internal predecessors, (20), 10 states have call successors, (10), 4 states have call predecessors, (10), 10 states have return successors, (32), 10 states have call predecessors, (32), 10 states have call successors, (32)
[2025-04-28 21:21:52,707 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 62 transitions.
[2025-04-28 21:21:52,707 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 62 transitions. Word has length 20
[2025-04-28 21:21:52,707 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,707 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 62 transitions.
[2025-04-28 21:21:52,708 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:52,708 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 62 transitions.
[2025-04-28 21:21:52,708 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:52,709 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,709 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,716 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:52,912 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,913 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,913 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,913 INFO  L85        PathProgramCache]: Analyzing trace with hash 1629634234, now seen corresponding path program 1 times
[2025-04-28 21:21:52,913 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,913 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1852239023]
[2025-04-28 21:21:52,913 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,914 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,918 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:52,925 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:52,925 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,925 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,136 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:53,136 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,136 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1852239023]
[2025-04-28 21:21:53,136 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1852239023] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,136 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [344244789]
[2025-04-28 21:21:53,136 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,136 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,142 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,144 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:53,150 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,191 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:53,208 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:53,208 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,208 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,210 INFO  L256         TraceCheckSpWp]: Trace formula consists of 92 conjuncts, 33 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,212 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,343 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:53,345 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,467 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:54,468 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [344244789] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,468 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:54,468 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [8, 8] total 15
[2025-04-28 21:21:54,468 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [731905267]
[2025-04-28 21:21:54,468 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,468 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:54,469 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,469 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:54,469 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=43, Invalid=167, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:54,470 INFO  L87              Difference]: Start difference. First operand 35 states and 62 transitions. Second operand  has 8 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:54,749 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,749 INFO  L93              Difference]: Finished difference Result 43 states and 86 transitions.
[2025-04-28 21:21:54,750 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:54,750 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:54,750 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,752 INFO  L225             Difference]: With dead ends: 43
[2025-04-28 21:21:54,752 INFO  L226             Difference]: Without dead ends: 43
[2025-04-28 21:21:54,752 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 34 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 15 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=57, Invalid=215, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:54,753 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 4 mSDsluCounter, 94 mSDsCounter, 0 mSdLazyCounter, 90 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 125 SdHoareTripleChecker+Invalid, 97 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 90 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,753 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 125 Invalid, 97 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 90 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:54,754 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 43 states.
[2025-04-28 21:21:54,761 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 43 to 35.
[2025-04-28 21:21:54,762 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 14 states have (on average 1.4285714285714286) internal successors, (20), 20 states have internal predecessors, (20), 10 states have call successors, (10), 4 states have call predecessors, (10), 10 states have return successors, (31), 10 states have call predecessors, (31), 10 states have call successors, (31)
[2025-04-28 21:21:54,763 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 61 transitions.
[2025-04-28 21:21:54,763 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 61 transitions. Word has length 20
[2025-04-28 21:21:54,763 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,763 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 61 transitions.
[2025-04-28 21:21:54,763 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:54,764 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 61 transitions.
[2025-04-28 21:21:54,765 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:54,765 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,765 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,770 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:54,968 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,969 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,969 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,969 INFO  L85        PathProgramCache]: Analyzing trace with hash 935806448, now seen corresponding path program 1 times
[2025-04-28 21:21:54,969 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,970 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1126337832]
[2025-04-28 21:21:54,970 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,970 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,974 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:54,980 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:54,980 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,981 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,207 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:55,208 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,208 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1126337832]
[2025-04-28 21:21:55,208 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1126337832] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,208 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1458382231]
[2025-04-28 21:21:55,208 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,208 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,211 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,213 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:55,217 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,259 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:55,273 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:55,273 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,273 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,275 WARN  L254         TraceCheckSpWp]: Trace formula consists of 92 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,276 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,437 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:55,437 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,370 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1458382231] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,370 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:56,370 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8] total 10
[2025-04-28 21:21:56,370 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [331906406]
[2025-04-28 21:21:56,370 INFO  L85    oduleStraightlineAll]: Using 2 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,370 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:56,371 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,371 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:56,371 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:56,372 INFO  L87              Difference]: Start difference. First operand 35 states and 61 transitions. Second operand  has 10 states, 7 states have (on average 1.7142857142857142) internal successors, (12), 9 states have internal predecessors, (12), 4 states have call successors, (5), 1 states have call predecessors, (5), 6 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:56,709 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,709 INFO  L93              Difference]: Finished difference Result 45 states and 92 transitions.
[2025-04-28 21:21:56,710 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:56,710 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 7 states have (on average 1.7142857142857142) internal successors, (12), 9 states have internal predecessors, (12), 4 states have call successors, (5), 1 states have call predecessors, (5), 6 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8) Word has length 20
[2025-04-28 21:21:56,710 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,711 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:21:56,711 INFO  L226             Difference]: Without dead ends: 45
[2025-04-28 21:21:56,711 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 37 GetRequests, 26 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=31, Invalid=125, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:56,712 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 5 mSDsluCounter, 153 mSDsCounter, 0 mSdLazyCounter, 198 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 182 SdHoareTripleChecker+Invalid, 202 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 198 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,712 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 182 Invalid, 202 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 198 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:56,713 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 45 states.
[2025-04-28 21:21:56,720 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 45 to 37.
[2025-04-28 21:21:56,720 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 37 states, 15 states have (on average 1.4) internal successors, (21), 21 states have internal predecessors, (21), 10 states have call successors, (10), 4 states have call predecessors, (10), 11 states have return successors, (36), 11 states have call predecessors, (36), 10 states have call successors, (36)
[2025-04-28 21:21:56,721 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 37 states to 37 states and 67 transitions.
[2025-04-28 21:21:56,721 INFO  L79                 Accepts]: Start accepts. Automaton has 37 states and 67 transitions. Word has length 20
[2025-04-28 21:21:56,721 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,721 INFO  L485      AbstractCegarLoop]: Abstraction has 37 states and 67 transitions.
[2025-04-28 21:21:56,721 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 7 states have (on average 1.7142857142857142) internal successors, (12), 9 states have internal predecessors, (12), 4 states have call successors, (5), 1 states have call predecessors, (5), 6 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:56,721 INFO  L278                IsEmpty]: Start isEmpty. Operand 37 states and 67 transitions.
[2025-04-28 21:21:56,722 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:56,722 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,722 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,729 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:56,923 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,923 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,923 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,924 INFO  L85        PathProgramCache]: Analyzing trace with hash 560466243, now seen corresponding path program 1 times
[2025-04-28 21:21:56,924 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,924 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1073573456]
[2025-04-28 21:21:56,924 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,924 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,928 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:56,933 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:56,933 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,933 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,097 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:57,098 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,098 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1073573456]
[2025-04-28 21:21:57,098 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1073573456] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,098 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1555524630]
[2025-04-28 21:21:57,098 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,098 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,101 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,103 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:57,115 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,160 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:57,175 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:57,175 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,175 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,176 INFO  L256         TraceCheckSpWp]: Trace formula consists of 92 conjuncts, 29 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,178 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,256 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:57,256 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,108 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:58,108 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1555524630] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,109 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:58,109 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [8, 8] total 15
[2025-04-28 21:21:58,109 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1806083875]
[2025-04-28 21:21:58,109 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,109 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:58,109 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,110 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:58,110 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=45, Invalid=165, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:58,110 INFO  L87              Difference]: Start difference. First operand 37 states and 67 transitions. Second operand  has 8 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:58,363 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,364 INFO  L93              Difference]: Finished difference Result 47 states and 99 transitions.
[2025-04-28 21:21:58,364 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:58,364 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:58,365 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,365 INFO  L225             Difference]: With dead ends: 47
[2025-04-28 21:21:58,366 INFO  L226             Difference]: Without dead ends: 47
[2025-04-28 21:21:58,366 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 48 GetRequests, 34 SyntacticMatches, 0 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 13 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=52, Invalid=188, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:58,367 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 3 mSDsluCounter, 105 mSDsCounter, 0 mSdLazyCounter, 159 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 135 SdHoareTripleChecker+Invalid, 161 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 159 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,367 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 135 Invalid, 161 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 159 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:58,367 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 47 states.
[2025-04-28 21:21:58,379 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 47 to 37.
[2025-04-28 21:21:58,379 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 37 states, 15 states have (on average 1.4) internal successors, (21), 21 states have internal predecessors, (21), 10 states have call successors, (10), 4 states have call predecessors, (10), 11 states have return successors, (35), 11 states have call predecessors, (35), 10 states have call successors, (35)
[2025-04-28 21:21:58,380 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 37 states to 37 states and 66 transitions.
[2025-04-28 21:21:58,380 INFO  L79                 Accepts]: Start accepts. Automaton has 37 states and 66 transitions. Word has length 20
[2025-04-28 21:21:58,380 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,380 INFO  L485      AbstractCegarLoop]: Abstraction has 37 states and 66 transitions.
[2025-04-28 21:21:58,380 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:58,380 INFO  L278                IsEmpty]: Start isEmpty. Operand 37 states and 66 transitions.
[2025-04-28 21:21:58,381 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:58,381 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,381 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,386 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:58,585 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-04-28 21:21:58,586 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,586 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,586 INFO  L85        PathProgramCache]: Analyzing trace with hash 1609960909, now seen corresponding path program 1 times
[2025-04-28 21:21:58,586 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,586 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1101498965]
[2025-04-28 21:21:58,586 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,587 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,590 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:58,594 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:58,594 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,594 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,772 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:58,772 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,772 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1101498965]
[2025-04-28 21:21:58,773 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1101498965] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:58,773 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:58,773 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:58,773 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1239447283]
[2025-04-28 21:21:58,773 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,773 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:58,775 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,775 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:58,775 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:58,775 INFO  L87              Difference]: Start difference. First operand 37 states and 66 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:58,977 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,977 INFO  L93              Difference]: Finished difference Result 49 states and 104 transitions.
[2025-04-28 21:21:58,978 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:58,978 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:58,978 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,979 INFO  L225             Difference]: With dead ends: 49
[2025-04-28 21:21:58,979 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:21:58,979 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=53, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:58,980 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 5 mSDsluCounter, 108 mSDsCounter, 0 mSdLazyCounter, 123 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 138 SdHoareTripleChecker+Invalid, 124 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 123 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,981 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 138 Invalid, 124 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 123 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:58,981 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:21:58,993 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 41.
[2025-04-28 21:21:58,993 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 17 states have (on average 1.3529411764705883) internal successors, (23), 23 states have internal predecessors, (23), 10 states have call successors, (10), 4 states have call predecessors, (10), 13 states have return successors, (46), 13 states have call predecessors, (46), 10 states have call successors, (46)
[2025-04-28 21:21:58,994 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 79 transitions.
[2025-04-28 21:21:58,994 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 79 transitions. Word has length 20
[2025-04-28 21:21:58,994 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,994 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 79 transitions.
[2025-04-28 21:21:58,994 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:58,994 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 79 transitions.
[2025-04-28 21:21:58,995 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:58,995 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,995 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,995 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:58,996 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,996 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,996 INFO  L85        PathProgramCache]: Analyzing trace with hash 1234620704, now seen corresponding path program 1 times
[2025-04-28 21:21:58,996 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,996 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [396350429]
[2025-04-28 21:21:58,996 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,996 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,000 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:59,003 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:59,003 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,003 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,181 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:59,181 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,181 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [396350429]
[2025-04-28 21:21:59,181 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [396350429] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,181 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:59,182 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:59,182 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1303148344]
[2025-04-28 21:21:59,182 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,182 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:59,182 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,183 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:59,183 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:59,183 INFO  L87              Difference]: Start difference. First operand 41 states and 79 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:59,389 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,389 INFO  L93              Difference]: Finished difference Result 49 states and 102 transitions.
[2025-04-28 21:21:59,391 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:59,391 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:59,392 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,392 INFO  L225             Difference]: With dead ends: 49
[2025-04-28 21:21:59,393 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:21:59,393 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=53, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:59,393 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 5 mSDsluCounter, 111 mSDsCounter, 0 mSdLazyCounter, 123 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 142 SdHoareTripleChecker+Invalid, 124 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 123 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,394 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 142 Invalid, 124 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 123 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:59,394 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:21:59,403 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 41.
[2025-04-28 21:21:59,404 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 17 states have (on average 1.3529411764705883) internal successors, (23), 23 states have internal predecessors, (23), 10 states have call successors, (10), 4 states have call predecessors, (10), 13 states have return successors, (44), 13 states have call predecessors, (44), 10 states have call successors, (44)
[2025-04-28 21:21:59,405 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 77 transitions.
[2025-04-28 21:21:59,405 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 77 transitions. Word has length 20
[2025-04-28 21:21:59,406 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,406 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 77 transitions.
[2025-04-28 21:21:59,406 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:59,406 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 77 transitions.
[2025-04-28 21:21:59,407 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:59,407 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,407 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,407 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:59,407 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,407 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,408 INFO  L85        PathProgramCache]: Analyzing trace with hash -1947002995, now seen corresponding path program 1 times
[2025-04-28 21:21:59,408 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,408 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [532369041]
[2025-04-28 21:21:59,408 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,408 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,412 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:59,414 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:59,414 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,414 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,484 INFO  L134       CoverageAnalysis]: Checked inductivity of 7 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:59,484 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,484 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [532369041]
[2025-04-28 21:21:59,484 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [532369041] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:59,485 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1172476936]
[2025-04-28 21:21:59,485 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,485 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,487 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:59,489 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:59,493 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:59,545 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:59,565 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:59,565 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,565 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,566 INFO  L256         TraceCheckSpWp]: Trace formula consists of 119 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:59,568 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:59,624 INFO  L134       CoverageAnalysis]: Checked inductivity of 7 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:59,625 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:59,625 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1172476936] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,625 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:59,625 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [7] total 8
[2025-04-28 21:21:59,625 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [403647231]
[2025-04-28 21:21:59,625 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,625 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:59,627 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,627 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:59,627 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:59,628 INFO  L87              Difference]: Start difference. First operand 41 states and 77 transitions. Second operand  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:59,731 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,731 INFO  L93              Difference]: Finished difference Result 49 states and 94 transitions.
[2025-04-28 21:21:59,732 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:59,732 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6) Word has length 24
[2025-04-28 21:21:59,732 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,733 INFO  L225             Difference]: With dead ends: 49
[2025-04-28 21:21:59,733 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:21:59,734 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 26 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=19, Invalid=53, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:59,734 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 3 mSDsluCounter, 112 mSDsCounter, 0 mSdLazyCounter, 72 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 146 SdHoareTripleChecker+Invalid, 76 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 72 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,734 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 146 Invalid, 76 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 72 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:59,735 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:21:59,741 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 47.
[2025-04-28 21:21:59,741 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 47 states, 20 states have (on average 1.3) internal successors, (26), 26 states have internal predecessors, (26), 10 states have call successors, (10), 4 states have call predecessors, (10), 16 states have return successors, (56), 16 states have call predecessors, (56), 10 states have call successors, (56)
[2025-04-28 21:21:59,742 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 47 states to 47 states and 92 transitions.
[2025-04-28 21:21:59,742 INFO  L79                 Accepts]: Start accepts. Automaton has 47 states and 92 transitions. Word has length 24
[2025-04-28 21:21:59,742 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,742 INFO  L485      AbstractCegarLoop]: Abstraction has 47 states and 92 transitions.
[2025-04-28 21:21:59,742 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:59,742 INFO  L278                IsEmpty]: Start isEmpty. Operand 47 states and 92 transitions.
[2025-04-28 21:21:59,743 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:59,743 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,744 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,750 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:59,944 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,944 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,945 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,945 INFO  L85        PathProgramCache]: Analyzing trace with hash 1705464719, now seen corresponding path program 1 times
[2025-04-28 21:21:59,945 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,945 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2128997879]
[2025-04-28 21:21:59,945 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,945 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,949 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:59,954 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:59,954 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,954 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,245 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:00,245 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,245 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2128997879]
[2025-04-28 21:22:00,245 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2128997879] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,245 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [48346739]
[2025-04-28 21:22:00,245 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,246 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,248 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,250 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:22:00,253 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,304 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:00,322 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:00,322 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,322 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,324 INFO  L256         TraceCheckSpWp]: Trace formula consists of 120 conjuncts, 48 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,325 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,469 INFO  L325             Elim1Store]: treesize reduction 7, result has 12.5 percent of original size
[2025-04-28 21:22:00,470 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 25 treesize of output 15
[2025-04-28 21:22:00,473 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:00,474 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:00,474 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [48346739] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:00,474 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:00,474 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [10] total 12
[2025-04-28 21:22:00,474 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1457246243]
[2025-04-28 21:22:00,474 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,475 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:00,475 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,475 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:00,475 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=22, Invalid=110, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:22:00,475 INFO  L87              Difference]: Start difference. First operand 47 states and 92 transitions. Second operand  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:00,645 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,645 INFO  L93              Difference]: Finished difference Result 53 states and 115 transitions.
[2025-04-28 21:22:00,646 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:00,646 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:22:00,646 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,647 INFO  L225             Difference]: With dead ends: 53
[2025-04-28 21:22:00,647 INFO  L226             Difference]: Without dead ends: 53
[2025-04-28 21:22:00,647 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 34 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=27, Invalid=129, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:22:00,648 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 3 mSDsluCounter, 72 mSDsCounter, 0 mSdLazyCounter, 108 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 100 SdHoareTripleChecker+Invalid, 108 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 108 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,648 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 100 Invalid, 108 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 108 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:00,649 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 53 states.
[2025-04-28 21:22:00,655 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 53 to 45.
[2025-04-28 21:22:00,655 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 45 states, 19 states have (on average 1.3157894736842106) internal successors, (25), 25 states have internal predecessors, (25), 10 states have call successors, (10), 4 states have call predecessors, (10), 15 states have return successors, (51), 15 states have call predecessors, (51), 10 states have call successors, (51)
[2025-04-28 21:22:00,656 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 45 states to 45 states and 86 transitions.
[2025-04-28 21:22:00,656 INFO  L79                 Accepts]: Start accepts. Automaton has 45 states and 86 transitions. Word has length 24
[2025-04-28 21:22:00,656 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,656 INFO  L485      AbstractCegarLoop]: Abstraction has 45 states and 86 transitions.
[2025-04-28 21:22:00,656 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:00,656 INFO  L278                IsEmpty]: Start isEmpty. Operand 45 states and 86 transitions.
[2025-04-28 21:22:00,657 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:22:00,657 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,657 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,665 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:22:00,857 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-04-28 21:22:00,858 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,858 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,858 INFO  L85        PathProgramCache]: Analyzing trace with hash 581577394, now seen corresponding path program 1 times
[2025-04-28 21:22:00,858 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,858 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [42197945]
[2025-04-28 21:22:00,858 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,858 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,862 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:00,863 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:00,863 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,863 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,902 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:00,902 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,902 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [42197945]
[2025-04-28 21:22:00,902 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [42197945] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:00,902 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:00,902 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:00,902 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [75272765]
[2025-04-28 21:22:00,902 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,902 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:00,902 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,903 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:00,903 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:00,903 INFO  L87              Difference]: Start difference. First operand 45 states and 86 transitions. Second operand  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:01,028 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,028 INFO  L93              Difference]: Finished difference Result 73 states and 162 transitions.
[2025-04-28 21:22:01,029 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:01,029 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:22:01,030 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,031 INFO  L225             Difference]: With dead ends: 73
[2025-04-28 21:22:01,031 INFO  L226             Difference]: Without dead ends: 73
[2025-04-28 21:22:01,031 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:01,031 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 5 mSDsluCounter, 40 mSDsCounter, 0 mSdLazyCounter, 72 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 76 SdHoareTripleChecker+Invalid, 75 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 72 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,032 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 76 Invalid, 75 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 72 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:01,032 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 73 states.
[2025-04-28 21:22:01,046 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 73 to 65.
[2025-04-28 21:22:01,047 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 65 states, 28 states have (on average 1.3214285714285714) internal successors, (37), 36 states have internal predecessors, (37), 13 states have call successors, (13), 5 states have call predecessors, (13), 23 states have return successors, (91), 23 states have call predecessors, (91), 13 states have call successors, (91)
[2025-04-28 21:22:01,051 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 65 states to 65 states and 141 transitions.
[2025-04-28 21:22:01,051 INFO  L79                 Accepts]: Start accepts. Automaton has 65 states and 141 transitions. Word has length 24
[2025-04-28 21:22:01,051 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,051 INFO  L485      AbstractCegarLoop]: Abstraction has 65 states and 141 transitions.
[2025-04-28 21:22:01,051 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:01,052 INFO  L278                IsEmpty]: Start isEmpty. Operand 65 states and 141 transitions.
[2025-04-28 21:22:01,053 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:22:01,053 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,053 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,053 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:22:01,053 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,053 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,054 INFO  L85        PathProgramCache]: Analyzing trace with hash -1305888078, now seen corresponding path program 1 times
[2025-04-28 21:22:01,054 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,054 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1932820855]
[2025-04-28 21:22:01,054 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,054 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,069 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:01,074 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:01,074 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,074 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,290 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:01,290 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,290 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1932820855]
[2025-04-28 21:22:01,290 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1932820855] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:01,290 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [754869674]
[2025-04-28 21:22:01,290 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,290 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,293 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:01,295 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:22:01,298 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:01,345 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:01,361 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:01,361 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,362 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,363 INFO  L256         TraceCheckSpWp]: Trace formula consists of 120 conjuncts, 59 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:01,365 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:01,536 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:01,536 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:02,806 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [754869674] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,806 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:22:02,806 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 10] total 12
[2025-04-28 21:22:02,807 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1749365880]
[2025-04-28 21:22:02,808 INFO  L85    oduleStraightlineAll]: Using 2 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:02,808 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:22:02,808 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:02,809 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:22:02,809 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=130, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:22:02,809 INFO  L87              Difference]: Start difference. First operand 65 states and 141 transitions. Second operand  has 12 states, 8 states have (on average 1.75) internal successors, (14), 11 states have internal predecessors, (14), 5 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:22:03,736 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,736 INFO  L93              Difference]: Finished difference Result 89 states and 186 transitions.
[2025-04-28 21:22:03,736 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:03,737 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 8 states have (on average 1.75) internal successors, (14), 11 states have internal predecessors, (14), 5 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10) Word has length 24
[2025-04-28 21:22:03,737 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,738 INFO  L225             Difference]: With dead ends: 89
[2025-04-28 21:22:03,738 INFO  L226             Difference]: Without dead ends: 89
[2025-04-28 21:22:03,738 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 46 GetRequests, 29 SyntacticMatches, 1 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 16 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=54, Invalid=252, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:22:03,739 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 7 mSDsluCounter, 165 mSDsCounter, 0 mSdLazyCounter, 268 mSolverCounterSat, 12 mSolverCounterUnsat, 6 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 196 SdHoareTripleChecker+Invalid, 286 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 268 IncrementalHoareTripleChecker+Invalid, 6 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,739 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 196 Invalid, 286 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 268 Invalid, 6 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:03,740 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 89 states.
[2025-04-28 21:22:03,751 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 89 to 71.
[2025-04-28 21:22:03,751 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 71 states, 31 states have (on average 1.2903225806451613) internal successors, (40), 39 states have internal predecessors, (40), 13 states have call successors, (13), 5 states have call predecessors, (13), 26 states have return successors, (98), 26 states have call predecessors, (98), 13 states have call successors, (98)
[2025-04-28 21:22:03,752 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 71 states to 71 states and 151 transitions.
[2025-04-28 21:22:03,753 INFO  L79                 Accepts]: Start accepts. Automaton has 71 states and 151 transitions. Word has length 24
[2025-04-28 21:22:03,753 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,753 INFO  L485      AbstractCegarLoop]: Abstraction has 71 states and 151 transitions.
[2025-04-28 21:22:03,753 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 8 states have (on average 1.75) internal successors, (14), 11 states have internal predecessors, (14), 5 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:22:03,753 INFO  L278                IsEmpty]: Start isEmpty. Operand 71 states and 151 transitions.
[2025-04-28 21:22:03,755 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:22:03,755 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,755 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,761 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:22:03,958 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable17
[2025-04-28 21:22:03,959 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,959 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,959 INFO  L85        PathProgramCache]: Analyzing trace with hash -590935675, now seen corresponding path program 1 times
[2025-04-28 21:22:03,959 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,959 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1827573824]
[2025-04-28 21:22:03,959 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:03,959 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,963 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:03,966 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:03,966 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,966 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,160 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:04,160 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,161 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1827573824]
[2025-04-28 21:22:04,161 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1827573824] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:04,161 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1429127157]
[2025-04-28 21:22:04,161 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:04,161 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,164 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:04,166 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:22:04,169 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:22:04,223 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:04,245 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:04,245 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,246 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,248 INFO  L256         TraceCheckSpWp]: Trace formula consists of 120 conjuncts, 39 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:04,249 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:04,372 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:04,373 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:05,703 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1429127157] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:05,703 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:22:05,703 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 10] total 12
[2025-04-28 21:22:05,703 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1395508643]
[2025-04-28 21:22:05,703 INFO  L85    oduleStraightlineAll]: Using 2 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,703 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:22:05,704 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,704 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:22:05,704 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=51, Invalid=221, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:22:05,705 INFO  L87              Difference]: Start difference. First operand 71 states and 151 transitions. Second operand  has 12 states, 8 states have (on average 1.75) internal successors, (14), 11 states have internal predecessors, (14), 5 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:22:06,108 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,108 INFO  L93              Difference]: Finished difference Result 97 states and 206 transitions.
[2025-04-28 21:22:06,108 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:06,108 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 8 states have (on average 1.75) internal successors, (14), 11 states have internal predecessors, (14), 5 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10) Word has length 24
[2025-04-28 21:22:06,109 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,110 INFO  L225             Difference]: With dead ends: 97
[2025-04-28 21:22:06,110 INFO  L226             Difference]: Without dead ends: 97
[2025-04-28 21:22:06,110 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 55 GetRequests, 35 SyntacticMatches, 0 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 35 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=92, Invalid=370, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:06,111 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 7 mSDsluCounter, 159 mSDsCounter, 0 mSdLazyCounter, 301 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 189 SdHoareTripleChecker+Invalid, 314 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 301 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,111 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 189 Invalid, 314 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 301 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:06,111 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 97 states.
[2025-04-28 21:22:06,122 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 97 to 79.
[2025-04-28 21:22:06,123 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 35 states have (on average 1.2571428571428571) internal successors, (44), 43 states have internal predecessors, (44), 13 states have call successors, (13), 5 states have call predecessors, (13), 30 states have return successors, (109), 30 states have call predecessors, (109), 13 states have call successors, (109)
[2025-04-28 21:22:06,124 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 166 transitions.
[2025-04-28 21:22:06,124 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 166 transitions. Word has length 24
[2025-04-28 21:22:06,124 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,124 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 166 transitions.
[2025-04-28 21:22:06,124 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 8 states have (on average 1.75) internal successors, (14), 11 states have internal predecessors, (14), 5 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:22:06,124 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 166 transitions.
[2025-04-28 21:22:06,125 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:22:06,126 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,126 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:06,131 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:06,329 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,330 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,330 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,330 INFO  L85        PathProgramCache]: Analyzing trace with hash -810999684, now seen corresponding path program 1 times
[2025-04-28 21:22:06,330 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,330 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1088872679]
[2025-04-28 21:22:06,330 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,330 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,334 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:06,340 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:06,342 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,342 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,539 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:06,539 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,540 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1088872679]
[2025-04-28 21:22:06,540 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1088872679] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:06,540 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1553744703]
[2025-04-28 21:22:06,540 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,540 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,543 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:06,545 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:22:06,548 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:06,609 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:06,626 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:06,626 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,626 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,627 INFO  L256         TraceCheckSpWp]: Trace formula consists of 120 conjuncts, 41 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:06,629 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:06,746 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:06,746 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:07,936 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:07,937 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1553744703] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:07,937 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:07,937 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 10, 10] total 17
[2025-04-28 21:22:07,937 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1754652883]
[2025-04-28 21:22:07,937 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,938 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:22:07,938 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,938 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:22:07,938 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=47, Invalid=225, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:22:07,939 INFO  L87              Difference]: Start difference. First operand 79 states and 166 transitions. Second operand  has 17 states, 9 states have (on average 2.111111111111111) internal successors, (19), 16 states have internal predecessors, (19), 9 states have call successors, (10), 1 states have call predecessors, (10), 8 states have return successors, (14), 7 states have call predecessors, (14), 9 states have call successors, (14)
[2025-04-28 21:22:08,691 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:08,691 INFO  L93              Difference]: Finished difference Result 137 states and 309 transitions.
[2025-04-28 21:22:08,692 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:22:08,692 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 9 states have (on average 2.111111111111111) internal successors, (19), 16 states have internal predecessors, (19), 9 states have call successors, (10), 1 states have call predecessors, (10), 8 states have return successors, (14), 7 states have call predecessors, (14), 9 states have call successors, (14) Word has length 24
[2025-04-28 21:22:08,692 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,694 INFO  L225             Difference]: With dead ends: 137
[2025-04-28 21:22:08,694 INFO  L226             Difference]: Without dead ends: 137
[2025-04-28 21:22:08,695 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 42 SyntacticMatches, 0 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 67 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=110, Invalid=540, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:22:08,695 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 12 mSDsluCounter, 227 mSDsCounter, 0 mSdLazyCounter, 495 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 261 SdHoareTripleChecker+Invalid, 511 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 495 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,696 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 261 Invalid, 511 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 495 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:22:08,696 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 137 states.
[2025-04-28 21:22:08,721 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 137 to 83.
[2025-04-28 21:22:08,721 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 83 states, 37 states have (on average 1.2432432432432432) internal successors, (46), 45 states have internal predecessors, (46), 13 states have call successors, (13), 5 states have call predecessors, (13), 32 states have return successors, (122), 32 states have call predecessors, (122), 13 states have call successors, (122)
[2025-04-28 21:22:08,722 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 83 states to 83 states and 181 transitions.
[2025-04-28 21:22:08,723 INFO  L79                 Accepts]: Start accepts. Automaton has 83 states and 181 transitions. Word has length 24
[2025-04-28 21:22:08,723 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,723 INFO  L485      AbstractCegarLoop]: Abstraction has 83 states and 181 transitions.
[2025-04-28 21:22:08,723 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 9 states have (on average 2.111111111111111) internal successors, (19), 16 states have internal predecessors, (19), 9 states have call successors, (10), 1 states have call predecessors, (10), 8 states have return successors, (14), 7 states have call predecessors, (14), 9 states have call successors, (14)
[2025-04-28 21:22:08,723 INFO  L278                IsEmpty]: Start isEmpty. Operand 83 states and 181 transitions.
[2025-04-28 21:22:08,725 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:22:08,725 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,725 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:08,731 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:22:08,930 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19,10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:08,930 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:08,931 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:08,932 INFO  L85        PathProgramCache]: Analyzing trace with hash -96047281, now seen corresponding path program 2 times
[2025-04-28 21:22:08,932 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:08,932 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [365973606]
[2025-04-28 21:22:08,932 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:08,932 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:08,938 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:22:08,945 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:08,948 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:08,948 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,204 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:09,204 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:09,204 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [365973606]
[2025-04-28 21:22:09,204 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [365973606] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:09,204 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [90796036]
[2025-04-28 21:22:09,204 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:09,204 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,207 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:09,209 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:09,212 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:09,277 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:22:09,295 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:09,295 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:09,295 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,297 INFO  L256         TraceCheckSpWp]: Trace formula consists of 120 conjuncts, 59 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:09,298 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:09,459 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:09,459 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:11,292 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:11,292 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [90796036] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:11,293 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:11,293 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 18
[2025-04-28 21:22:11,293 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1956926739]
[2025-04-28 21:22:11,293 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:11,293 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:22:11,294 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:11,294 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:22:11,294 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=51, Invalid=255, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:22:11,294 INFO  L87              Difference]: Start difference. First operand 83 states and 181 transitions. Second operand  has 18 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 17 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (13), 7 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:22:12,075 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,075 INFO  L93              Difference]: Finished difference Result 123 states and 267 transitions.
[2025-04-28 21:22:12,075 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:22:12,075 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 17 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (13), 7 states have call predecessors, (13), 10 states have call successors, (13) Word has length 24
[2025-04-28 21:22:12,076 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,077 INFO  L225             Difference]: With dead ends: 123
[2025-04-28 21:22:12,077 INFO  L226             Difference]: Without dead ends: 123
[2025-04-28 21:22:12,078 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 67 GetRequests, 40 SyntacticMatches, 1 SemanticMatches, 26 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 95 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=130, Invalid=626, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:22:12,078 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 16 mSDsluCounter, 194 mSDsCounter, 0 mSdLazyCounter, 398 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 229 SdHoareTripleChecker+Invalid, 424 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 398 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,078 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 229 Invalid, 424 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 398 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:22:12,079 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 123 states.
[2025-04-28 21:22:12,094 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 123 to 83.
[2025-04-28 21:22:12,094 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 83 states, 37 states have (on average 1.2432432432432432) internal successors, (46), 45 states have internal predecessors, (46), 13 states have call successors, (13), 5 states have call predecessors, (13), 32 states have return successors, (121), 32 states have call predecessors, (121), 13 states have call successors, (121)
[2025-04-28 21:22:12,095 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 83 states to 83 states and 180 transitions.
[2025-04-28 21:22:12,095 INFO  L79                 Accepts]: Start accepts. Automaton has 83 states and 180 transitions. Word has length 24
[2025-04-28 21:22:12,095 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:12,096 INFO  L485      AbstractCegarLoop]: Abstraction has 83 states and 180 transitions.
[2025-04-28 21:22:12,096 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 17 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (13), 7 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:22:12,096 INFO  L278                IsEmpty]: Start isEmpty. Operand 83 states and 180 transitions.
[2025-04-28 21:22:12,097 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:22:12,097 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:12,097 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:12,103 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:12,301 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:12,302 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:12,302 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:12,302 INFO  L85        PathProgramCache]: Analyzing trace with hash 656893253, now seen corresponding path program 2 times
[2025-04-28 21:22:12,302 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:12,302 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [658437716]
[2025-04-28 21:22:12,302 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:12,303 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:12,309 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:22:12,312 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:12,313 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:12,313 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:12,407 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:12,407 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:12,407 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [658437716]
[2025-04-28 21:22:12,407 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [658437716] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:12,408 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:12,408 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:12,408 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [96475185]
[2025-04-28 21:22:12,408 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,408 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:12,408 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,408 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:12,408 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:12,409 INFO  L87              Difference]: Start difference. First operand 83 states and 180 transitions. Second operand  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:12,527 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,527 INFO  L93              Difference]: Finished difference Result 91 states and 185 transitions.
[2025-04-28 21:22:12,527 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:12,527 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:22:12,528 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,529 INFO  L225             Difference]: With dead ends: 91
[2025-04-28 21:22:12,529 INFO  L226             Difference]: Without dead ends: 91
[2025-04-28 21:22:12,529 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:12,530 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 4 mSDsluCounter, 43 mSDsCounter, 0 mSdLazyCounter, 67 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 83 SdHoareTripleChecker+Invalid, 69 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 67 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,530 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 83 Invalid, 69 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 67 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:12,530 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-04-28 21:22:12,539 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 79.
[2025-04-28 21:22:12,540 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 35 states have (on average 1.2571428571428571) internal successors, (44), 43 states have internal predecessors, (44), 13 states have call successors, (13), 5 states have call predecessors, (13), 30 states have return successors, (102), 30 states have call predecessors, (102), 13 states have call successors, (102)
[2025-04-28 21:22:12,541 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 159 transitions.
[2025-04-28 21:22:12,541 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 159 transitions. Word has length 24
[2025-04-28 21:22:12,541 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:12,541 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 159 transitions.
[2025-04-28 21:22:12,541 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:12,542 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 159 transitions.
[2025-04-28 21:22:12,543 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:12,543 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:12,543 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:12,543 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-04-28 21:22:12,543 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:12,543 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:12,544 INFO  L85        PathProgramCache]: Analyzing trace with hash 51172001, now seen corresponding path program 1 times
[2025-04-28 21:22:12,544 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:12,544 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [369212796]
[2025-04-28 21:22:12,544 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:12,544 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:12,548 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:12,552 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:12,555 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:12,555 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:12,624 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:12,624 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:12,624 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [369212796]
[2025-04-28 21:22:12,624 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [369212796] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:12,624 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:12,624 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:12,625 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [914902161]
[2025-04-28 21:22:12,625 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,625 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:12,625 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,626 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:12,626 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:12,626 INFO  L87              Difference]: Start difference. First operand 79 states and 159 transitions. Second operand  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:22:12,744 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,744 INFO  L93              Difference]: Finished difference Result 109 states and 192 transitions.
[2025-04-28 21:22:12,744 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:12,745 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 3 states have call successors, (7) Word has length 28
[2025-04-28 21:22:12,745 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,746 INFO  L225             Difference]: With dead ends: 109
[2025-04-28 21:22:12,746 INFO  L226             Difference]: Without dead ends: 89
[2025-04-28 21:22:12,746 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:12,748 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 4 mSDsluCounter, 38 mSDsCounter, 0 mSdLazyCounter, 63 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 76 SdHoareTripleChecker+Invalid, 70 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 63 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,748 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 76 Invalid, 70 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 63 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:12,749 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 89 states.
[2025-04-28 21:22:12,756 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 89 to 83.
[2025-04-28 21:22:12,757 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 83 states, 37 states have (on average 1.2702702702702702) internal successors, (47), 45 states have internal predecessors, (47), 14 states have call successors, (14), 6 states have call predecessors, (14), 31 states have return successors, (90), 31 states have call predecessors, (90), 14 states have call successors, (90)
[2025-04-28 21:22:12,758 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 83 states to 83 states and 151 transitions.
[2025-04-28 21:22:12,758 INFO  L79                 Accepts]: Start accepts. Automaton has 83 states and 151 transitions. Word has length 28
[2025-04-28 21:22:12,758 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:12,758 INFO  L485      AbstractCegarLoop]: Abstraction has 83 states and 151 transitions.
[2025-04-28 21:22:12,758 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:22:12,758 INFO  L278                IsEmpty]: Start isEmpty. Operand 83 states and 151 transitions.
[2025-04-28 21:22:12,759 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:12,760 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:12,760 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:12,760 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-04-28 21:22:12,760 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:12,760 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:12,760 INFO  L85        PathProgramCache]: Analyzing trace with hash -815265447, now seen corresponding path program 1 times
[2025-04-28 21:22:12,760 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:12,761 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1060397189]
[2025-04-28 21:22:12,761 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:12,761 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:12,764 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:12,766 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:12,767 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:12,767 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:12,828 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:12,828 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:12,829 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1060397189]
[2025-04-28 21:22:12,829 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1060397189] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:12,829 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1141000490]
[2025-04-28 21:22:12,829 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:12,829 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:12,831 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:12,833 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:12,838 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:22:12,907 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:12,925 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:12,925 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:12,925 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:12,926 INFO  L256         TraceCheckSpWp]: Trace formula consists of 142 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:12,927 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:12,948 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:12,948 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:13,312 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 5 treesize of output 3
[2025-04-28 21:22:13,320 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 7 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:22:13,321 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1141000490] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:13,321 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:13,321 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 9
[2025-04-28 21:22:13,321 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [210649011]
[2025-04-28 21:22:13,321 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:13,321 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:22:13,321 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:13,321 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:22:13,322 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=53, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:22:13,322 INFO  L87              Difference]: Start difference. First operand 83 states and 151 transitions. Second operand  has 9 states, 5 states have (on average 3.0) internal successors, (15), 9 states have internal predecessors, (15), 6 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (9), 4 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:22:13,564 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:13,564 INFO  L93              Difference]: Finished difference Result 141 states and 256 transitions.
[2025-04-28 21:22:13,565 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:13,565 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 3.0) internal successors, (15), 9 states have internal predecessors, (15), 6 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (9), 4 states have call predecessors, (9), 6 states have call successors, (9) Word has length 28
[2025-04-28 21:22:13,565 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:13,567 INFO  L225             Difference]: With dead ends: 141
[2025-04-28 21:22:13,567 INFO  L226             Difference]: Without dead ends: 129
[2025-04-28 21:22:13,567 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 70 GetRequests, 56 SyntacticMatches, 1 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 16 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=55, Invalid=155, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:22:13,567 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 15 mSDsluCounter, 132 mSDsCounter, 0 mSdLazyCounter, 164 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 170 SdHoareTripleChecker+Invalid, 186 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 164 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:13,568 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 170 Invalid, 186 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 164 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:13,568 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 129 states.
[2025-04-28 21:22:13,584 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 129 to 93.
[2025-04-28 21:22:13,585 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 93 states, 40 states have (on average 1.4) internal successors, (56), 53 states have internal predecessors, (56), 21 states have call successors, (21), 9 states have call predecessors, (21), 31 states have return successors, (95), 30 states have call predecessors, (95), 21 states have call successors, (95)
[2025-04-28 21:22:13,586 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 93 states to 93 states and 172 transitions.
[2025-04-28 21:22:13,586 INFO  L79                 Accepts]: Start accepts. Automaton has 93 states and 172 transitions. Word has length 28
[2025-04-28 21:22:13,587 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,587 INFO  L485      AbstractCegarLoop]: Abstraction has 93 states and 172 transitions.
[2025-04-28 21:22:13,587 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 3.0) internal successors, (15), 9 states have internal predecessors, (15), 6 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (9), 4 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:22:13,587 INFO  L278                IsEmpty]: Start isEmpty. Operand 93 states and 172 transitions.
[2025-04-28 21:22:13,588 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:13,589 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,589 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:13,595 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:13,793 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable23
[2025-04-28 21:22:13,794 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,794 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,794 INFO  L85        PathProgramCache]: Analyzing trace with hash 1695447065, now seen corresponding path program 1 times
[2025-04-28 21:22:13,794 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,794 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [834012259]
[2025-04-28 21:22:13,795 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,795 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,800 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:13,808 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:13,808 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,808 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,927 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 6 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:13,927 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,927 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [834012259]
[2025-04-28 21:22:13,928 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [834012259] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:13,928 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [505927710]
[2025-04-28 21:22:13,928 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,928 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,930 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:13,932 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:13,936 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-04-28 21:22:14,011 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:14,033 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:14,033 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:14,033 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:14,035 INFO  L256         TraceCheckSpWp]: Trace formula consists of 145 conjuncts, 50 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:14,038 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:14,225 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 4 proven. 1 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:14,225 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:14,925 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [505927710] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:14,925 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:22:14,925 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 7] total 13
[2025-04-28 21:22:14,925 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1604590516]
[2025-04-28 21:22:14,925 INFO  L85    oduleStraightlineAll]: Using 2 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:14,925 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:22:14,925 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:14,925 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:22:14,926 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=31, Invalid=151, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:22:14,926 INFO  L87              Difference]: Start difference. First operand 93 states and 172 transitions. Second operand  has 13 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 13 states have internal predecessors, (21), 6 states have call successors, (10), 1 states have call predecessors, (10), 9 states have return successors, (12), 8 states have call predecessors, (12), 6 states have call successors, (12)
[2025-04-28 21:22:15,717 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:15,717 INFO  L93              Difference]: Finished difference Result 183 states and 426 transitions.
[2025-04-28 21:22:15,718 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 22 states. 
[2025-04-28 21:22:15,718 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 13 states have internal predecessors, (21), 6 states have call successors, (10), 1 states have call predecessors, (10), 9 states have return successors, (12), 8 states have call predecessors, (12), 6 states have call successors, (12) Word has length 28
[2025-04-28 21:22:15,718 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:15,720 INFO  L225             Difference]: With dead ends: 183
[2025-04-28 21:22:15,720 INFO  L226             Difference]: Without dead ends: 148
[2025-04-28 21:22:15,721 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 61 GetRequests, 37 SyntacticMatches, 0 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 94 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=115, Invalid=535, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:22:15,721 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 12 mSDsluCounter, 249 mSDsCounter, 0 mSdLazyCounter, 588 mSolverCounterSat, 45 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 292 SdHoareTripleChecker+Invalid, 633 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 45 IncrementalHoareTripleChecker+Valid, 588 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:15,724 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 292 Invalid, 633 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [45 Valid, 588 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:15,724 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 148 states.
[2025-04-28 21:22:15,739 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 148 to 116.
[2025-04-28 21:22:15,740 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 116 states, 47 states have (on average 1.553191489361702) internal successors, (73), 69 states have internal predecessors, (73), 37 states have call successors, (37), 16 states have call predecessors, (37), 31 states have return successors, (153), 30 states have call predecessors, (153), 37 states have call successors, (153)
[2025-04-28 21:22:15,741 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 116 states to 116 states and 263 transitions.
[2025-04-28 21:22:15,742 INFO  L79                 Accepts]: Start accepts. Automaton has 116 states and 263 transitions. Word has length 28
[2025-04-28 21:22:15,742 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:15,742 INFO  L485      AbstractCegarLoop]: Abstraction has 116 states and 263 transitions.
[2025-04-28 21:22:15,742 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 13 states have internal predecessors, (21), 6 states have call successors, (10), 1 states have call predecessors, (10), 9 states have return successors, (12), 8 states have call predecessors, (12), 6 states have call successors, (12)
[2025-04-28 21:22:15,742 INFO  L278                IsEmpty]: Start isEmpty. Operand 116 states and 263 transitions.
[2025-04-28 21:22:15,744 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:15,745 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:15,745 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:15,752 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Ended with exit code 0
[2025-04-28 21:22:15,948 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable24,13 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:15,949 INFO  L403      AbstractCegarLoop]: === Iteration 25 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:15,949 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:15,949 INFO  L85        PathProgramCache]: Analyzing trace with hash -1602842004, now seen corresponding path program 1 times
[2025-04-28 21:22:15,949 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:15,949 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1517538808]
[2025-04-28 21:22:15,950 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:15,950 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:15,953 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:15,956 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:15,956 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:15,956 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:16,032 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 6 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:16,032 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:16,032 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1517538808]
[2025-04-28 21:22:16,032 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1517538808] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:16,032 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [972007536]
[2025-04-28 21:22:16,032 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:16,033 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:16,035 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:16,037 INFO  L229       MonitoredProcess]: Starting monitored process 14 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:16,039 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Waiting until timeout for monitored process
[2025-04-28 21:22:16,121 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:16,140 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:16,140 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:16,140 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:16,143 INFO  L256         TraceCheckSpWp]: Trace formula consists of 145 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:16,144 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:16,169 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 6 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:16,169 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
