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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:43,992 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:44,089 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_48febbc1-f8bd-4827-90cb-95427cffecaf/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:44,094 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:44,096 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:44,129 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:44,131 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:44,131 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:44,132 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:44,133 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:44,133 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:44,133 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:44,134 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:44,134 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:44,135 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:44,135 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:44,135 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:44,135 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:44,135 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:44,135 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:44,136 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:44,136 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:44,136 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:44,136 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:44,136 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:44,137 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:44,137 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:44,501 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:44,516 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:44,519 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:44,521 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:44,522 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:44,523 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_48febbc1-f8bd-4827-90cb-95427cffecaf/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-164.smt2
[2025-04-28 21:21:44,526 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:44,533 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:44,769 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_48febbc1-f8bd-4827-90cb-95427cffecaf/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-164.smt2
[2025-04-28 21:21:44,772 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:44,775 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:44,775 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:44,776 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:44,776 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:44,778 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,804 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44 Unit
[2025-04-28 21:21:44,804 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:44,805 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:44,805 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:44,805 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:44,822 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,822 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,849 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,849 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,853 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,853 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,855 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,857 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,858 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,879 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:44,880 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:44,883 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:44,883 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:44,884 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,887 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:44,906 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,919 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:44,923 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:44,941 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:44,942 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:44,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:44,942 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure END_QUERY given in one single declaration
[2025-04-28 21:21:44,942 INFO  L130     BoogieDeclarations]: Found specification of procedure END_QUERY
[2025-04-28 21:21:44,942 INFO  L138     BoogieDeclarations]: Found implementation of procedure END_QUERY
[2025-04-28 21:21:44,943 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_2 given in one single declaration
[2025-04-28 21:21:44,943 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_2
[2025-04-28 21:21:44,943 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_2
[2025-04-28 21:21:44,944 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:44,944 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:44,945 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:44,945 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:44,945 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:44,945 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:44,992 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:44,994 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:45,169 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:45,170 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:45,187 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:45,188 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:45,188 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:45 BoogieIcfgContainer
[2025-04-28 21:21:45,188 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:45,194 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:45,194 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:45,198 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:45,198 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:44" (1/3) ...
[2025-04-28 21:21:45,199 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@c0289d7 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:45, skipping insertion in model container
[2025-04-28 21:21:45,199 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (2/3) ...
[2025-04-28 21:21:45,200 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@c0289d7 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:45, skipping insertion in model container
[2025-04-28 21:21:45,200 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:45" (3/3) ...
[2025-04-28 21:21:45,201 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:45,220 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:45,222 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 5 procedures, 25 locations, 46 edges, 5 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:45,268 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:45,284 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;@3dc7cb92, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:45,284 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:45,288 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 25 states, 9 states have (on average 1.7777777777777777) internal successors, (16), 16 states have internal predecessors, (16), 10 states have call successors, (10), 4 states have call predecessors, (10), 4 states have return successors, (10), 5 states have call predecessors, (10), 10 states have call successors, (10)
[2025-04-28 21:21:45,298 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:45,299 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,299 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:45,300 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,305 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,305 INFO  L85        PathProgramCache]: Analyzing trace with hash -2057131199, now seen corresponding path program 1 times
[2025-04-28 21:21:45,313 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,313 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1411120953]
[2025-04-28 21:21:45,314 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,314 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,345 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:45,363 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:45,363 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,363 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,540 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:45,541 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,541 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1411120953]
[2025-04-28 21:21:45,542 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1411120953] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,542 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,545 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:45,546 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [89895551]
[2025-04-28 21:21:45,547 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,551 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:45,551 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,579 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:45,579 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:45,581 INFO  L87              Difference]: Start difference. First operand  has 25 states, 9 states have (on average 1.7777777777777777) internal successors, (16), 16 states have internal predecessors, (16), 10 states have call successors, (10), 4 states have call predecessors, (10), 4 states have return successors, (10), 5 states have call predecessors, (10), 10 states have call successors, (10) Second operand  has 5 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:45,701 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,702 INFO  L93              Difference]: Finished difference Result 27 states and 43 transitions.
[2025-04-28 21:21:45,705 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:45,706 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:21:45,707 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,714 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:45,715 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:45,717 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 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:45,721 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 1 mSDsluCounter, 64 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 91 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,722 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 91 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,741 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:45,768 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:45,796 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 10 states have (on average 1.6) internal successors, (16), 16 states have internal predecessors, (16), 10 states have call successors, (10), 4 states have call predecessors, (10), 6 states have return successors, (17), 6 states have call predecessors, (17), 10 states have call successors, (17)
[2025-04-28 21:21:45,802 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 43 transitions.
[2025-04-28 21:21:45,803 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 43 transitions. Word has length 16
[2025-04-28 21:21:45,804 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,805 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 43 transitions.
[2025-04-28 21:21:45,805 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:45,806 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 43 transitions.
[2025-04-28 21:21:45,807 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:45,808 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,808 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:45,809 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:45,809 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,810 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,812 INFO  L85        PathProgramCache]: Analyzing trace with hash 938204016, now seen corresponding path program 1 times
[2025-04-28 21:21:45,812 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,812 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1533244743]
[2025-04-28 21:21:45,813 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,813 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,823 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:45,855 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:45,855 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,855 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,107 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:46,107 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,107 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1533244743]
[2025-04-28 21:21:46,107 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1533244743] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,107 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,107 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:46,107 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [454384355]
[2025-04-28 21:21:46,108 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,109 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:46,109 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,109 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:46,109 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:46,112 INFO  L87              Difference]: Start difference. First operand 27 states and 43 transitions. Second operand  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:46,442 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,442 INFO  L93              Difference]: Finished difference Result 43 states and 83 transitions.
[2025-04-28 21:21:46,443 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:46,443 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:46,444 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,445 INFO  L225             Difference]: With dead ends: 43
[2025-04-28 21:21:46,445 INFO  L226             Difference]: Without dead ends: 43
[2025-04-28 21:21:46,446 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:46,447 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 7 mSDsluCounter, 76 mSDsCounter, 0 mSdLazyCounter, 131 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 106 SdHoareTripleChecker+Invalid, 141 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 131 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,447 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 106 Invalid, 141 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 131 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:46,448 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 43 states.
[2025-04-28 21:21:46,459 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 43 to 37.
[2025-04-28 21:21:46,460 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 37 states, 14 states have (on average 1.6428571428571428) internal successors, (23), 22 states have internal predecessors, (23), 13 states have call successors, (13), 5 states have call predecessors, (13), 9 states have return successors, (30), 9 states have call predecessors, (30), 13 states have call successors, (30)
[2025-04-28 21:21:46,461 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 37 states to 37 states and 66 transitions.
[2025-04-28 21:21:46,462 INFO  L79                 Accepts]: Start accepts. Automaton has 37 states and 66 transitions. Word has length 20
[2025-04-28 21:21:46,462 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,462 INFO  L485      AbstractCegarLoop]: Abstraction has 37 states and 66 transitions.
[2025-04-28 21:21:46,462 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:46,462 INFO  L278                IsEmpty]: Start isEmpty. Operand 37 states and 66 transitions.
[2025-04-28 21:21:46,464 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:46,464 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,464 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:46,464 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:46,464 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,465 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,465 INFO  L85        PathProgramCache]: Analyzing trace with hash 918530691, now seen corresponding path program 1 times
[2025-04-28 21:21:46,465 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,465 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1791754941]
[2025-04-28 21:21:46,466 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,466 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,472 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:46,480 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:46,481 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,481 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,666 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:46,667 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,667 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1791754941]
[2025-04-28 21:21:46,667 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1791754941] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,667 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,667 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:46,667 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [336311466]
[2025-04-28 21:21:46,667 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,668 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:46,668 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,668 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:46,668 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:46,668 INFO  L87              Difference]: Start difference. First operand 37 states and 66 transitions. Second operand  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:46,927 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,927 INFO  L93              Difference]: Finished difference Result 45 states and 79 transitions.
[2025-04-28 21:21:46,930 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:46,930 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:46,931 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,932 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:21:46,932 INFO  L226             Difference]: Without dead ends: 45
[2025-04-28 21:21:46,932 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:46,933 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 6 mSDsluCounter, 79 mSDsCounter, 0 mSdLazyCounter, 120 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 110 SdHoareTripleChecker+Invalid, 127 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 120 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,936 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 110 Invalid, 127 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 120 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:46,937 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 45 states.
[2025-04-28 21:21:46,952 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 45 to 35.
[2025-04-28 21:21:46,956 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 13 states have (on average 1.6923076923076923) internal successors, (22), 21 states have internal predecessors, (22), 13 states have call successors, (13), 5 states have call predecessors, (13), 8 states have return successors, (24), 8 states have call predecessors, (24), 13 states have call successors, (24)
[2025-04-28 21:21:46,957 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 59 transitions.
[2025-04-28 21:21:46,957 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 59 transitions. Word has length 20
[2025-04-28 21:21:46,957 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,958 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 59 transitions.
[2025-04-28 21:21:46,958 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:46,958 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 59 transitions.
[2025-04-28 21:21:46,959 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:46,959 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,959 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:46,959 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:46,961 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,962 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,962 INFO  L85        PathProgramCache]: Analyzing trace with hash 591290123, now seen corresponding path program 1 times
[2025-04-28 21:21:46,962 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,962 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1192853946]
[2025-04-28 21:21:46,962 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,962 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,974 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:46,988 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:46,988 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,989 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,239 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:47,239 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,239 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1192853946]
[2025-04-28 21:21:47,239 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1192853946] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,239 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [462952124]
[2025-04-28 21:21:47,239 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,239 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,242 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,244 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:47,251 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,283 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:47,300 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:47,300 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,300 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,303 INFO  L256         TraceCheckSpWp]: Trace formula consists of 86 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,309 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,490 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:47,493 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,286 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:48,288 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [462952124] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,288 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,288 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 14
[2025-04-28 21:21:48,289 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [308950532]
[2025-04-28 21:21:48,289 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,289 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:48,289 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,290 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:48,292 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=140, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:48,292 INFO  L87              Difference]: Start difference. First operand 35 states and 59 transitions. Second operand  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:48,597 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,597 INFO  L93              Difference]: Finished difference Result 61 states and 106 transitions.
[2025-04-28 21:21:48,598 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:48,598 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11) Word has length 20
[2025-04-28 21:21:48,598 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,600 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:48,600 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:48,600 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 50 GetRequests, 35 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 23 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=68, Invalid=204, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:48,601 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 14 mSDsluCounter, 109 mSDsCounter, 0 mSdLazyCounter, 147 mSolverCounterSat, 37 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 28 SdHoareTripleChecker+Valid, 132 SdHoareTripleChecker+Invalid, 184 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 37 IncrementalHoareTripleChecker+Valid, 147 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,601 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [28 Valid, 132 Invalid, 184 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [37 Valid, 147 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:48,602 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:48,618 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 45.
[2025-04-28 21:21:48,622 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 45 states, 17 states have (on average 1.7058823529411764) internal successors, (29), 27 states have internal predecessors, (29), 16 states have call successors, (16), 6 states have call predecessors, (16), 11 states have return successors, (36), 11 states have call predecessors, (36), 16 states have call successors, (36)
[2025-04-28 21:21:48,624 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 45 states to 45 states and 81 transitions.
[2025-04-28 21:21:48,624 INFO  L79                 Accepts]: Start accepts. Automaton has 45 states and 81 transitions. Word has length 20
[2025-04-28 21:21:48,624 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,624 INFO  L485      AbstractCegarLoop]: Abstraction has 45 states and 81 transitions.
[2025-04-28 21:21:48,624 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:48,624 INFO  L278                IsEmpty]: Start isEmpty. Operand 45 states and 81 transitions.
[2025-04-28 21:21:48,626 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:48,629 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,629 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:48,635 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:48,830 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,830 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,831 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,831 INFO  L85        PathProgramCache]: Analyzing trace with hash -144792113, now seen corresponding path program 1 times
[2025-04-28 21:21:48,831 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,831 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [348696319]
[2025-04-28 21:21:48,831 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,831 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,836 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:48,842 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:48,845 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,845 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,967 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:48,967 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,967 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [348696319]
[2025-04-28 21:21:48,967 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [348696319] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:48,967 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1044474721]
[2025-04-28 21:21:48,967 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,968 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,970 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,972 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:48,975 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,010 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:49,023 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,024 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,024 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,025 INFO  L256         TraceCheckSpWp]: Trace formula consists of 86 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:49,026 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:49,082 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:49,082 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:49,635 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:49,636 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1044474721] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:49,636 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:49,636 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:49,636 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [591230702]
[2025-04-28 21:21:49,637 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,637 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:49,637 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,638 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:49,638 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:49,639 INFO  L87              Difference]: Start difference. First operand 45 states and 81 transitions. Second operand  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:49,847 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,847 INFO  L93              Difference]: Finished difference Result 65 states and 126 transitions.
[2025-04-28 21:21:49,851 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:49,851 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10) Word has length 20
[2025-04-28 21:21:49,851 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,852 INFO  L225             Difference]: With dead ends: 65
[2025-04-28 21:21:49,853 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:49,853 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 48 GetRequests, 34 SyntacticMatches, 3 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 15 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:49,854 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 6 mSDsluCounter, 128 mSDsCounter, 0 mSdLazyCounter, 123 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 156 SdHoareTripleChecker+Invalid, 141 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 123 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,854 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 156 Invalid, 141 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 123 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:49,858 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:49,872 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 49.
[2025-04-28 21:21:49,873 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 49 states, 19 states have (on average 1.631578947368421) internal successors, (31), 29 states have internal predecessors, (31), 16 states have call successors, (16), 6 states have call predecessors, (16), 13 states have return successors, (46), 13 states have call predecessors, (46), 16 states have call successors, (46)
[2025-04-28 21:21:49,875 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 49 states to 49 states and 93 transitions.
[2025-04-28 21:21:49,875 INFO  L79                 Accepts]: Start accepts. Automaton has 49 states and 93 transitions. Word has length 20
[2025-04-28 21:21:49,876 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,876 INFO  L485      AbstractCegarLoop]: Abstraction has 49 states and 93 transitions.
[2025-04-28 21:21:49,876 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:49,876 INFO  L278                IsEmpty]: Start isEmpty. Operand 49 states and 93 transitions.
[2025-04-28 21:21:49,883 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:49,883 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,883 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,888 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:50,083 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,083 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,084 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,084 INFO  L85        PathProgramCache]: Analyzing trace with hash 642549034, now seen corresponding path program 1 times
[2025-04-28 21:21:50,084 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,084 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [935989504]
[2025-04-28 21:21:50,084 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,084 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,089 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:50,094 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,099 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,099 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,214 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,214 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,214 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [935989504]
[2025-04-28 21:21:50,215 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [935989504] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,215 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [207267972]
[2025-04-28 21:21:50,215 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,215 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,217 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,220 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:50,223 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,261 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:50,275 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,275 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,275 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,276 INFO  L256         TraceCheckSpWp]: Trace formula consists of 90 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,278 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,396 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,396 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,901 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,902 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [207267972] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,902 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,902 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 17
[2025-04-28 21:21:50,902 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1302052462]
[2025-04-28 21:21:50,902 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,902 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:50,903 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,903 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:50,903 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=235, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:50,904 INFO  L87              Difference]: Start difference. First operand 49 states and 93 transitions. Second operand  has 17 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 5 states have call predecessors, (11), 10 states have call successors, (11)
[2025-04-28 21:21:51,447 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,448 INFO  L93              Difference]: Finished difference Result 87 states and 180 transitions.
[2025-04-28 21:21:51,448 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-04-28 21:21:51,448 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 5 states have call predecessors, (11), 10 states have call successors, (11) Word has length 20
[2025-04-28 21:21:51,448 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,450 INFO  L225             Difference]: With dead ends: 87
[2025-04-28 21:21:51,450 INFO  L226             Difference]: Without dead ends: 79
[2025-04-28 21:21:51,451 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 59 GetRequests, 30 SyntacticMatches, 2 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 81 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=116, Invalid=696, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:21:51,451 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 15 mSDsluCounter, 270 mSDsCounter, 0 mSdLazyCounter, 256 mSolverCounterSat, 73 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 298 SdHoareTripleChecker+Invalid, 329 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 73 IncrementalHoareTripleChecker+Valid, 256 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,452 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 298 Invalid, 329 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [73 Valid, 256 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:51,452 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 79 states.
[2025-04-28 21:21:51,489 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 79 to 53.
[2025-04-28 21:21:51,490 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 53 states, 21 states have (on average 1.5714285714285714) internal successors, (33), 31 states have internal predecessors, (33), 16 states have call successors, (16), 6 states have call predecessors, (16), 15 states have return successors, (54), 15 states have call predecessors, (54), 16 states have call successors, (54)
[2025-04-28 21:21:51,491 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 53 states to 53 states and 103 transitions.
[2025-04-28 21:21:51,491 INFO  L79                 Accepts]: Start accepts. Automaton has 53 states and 103 transitions. Word has length 20
[2025-04-28 21:21:51,491 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,491 INFO  L485      AbstractCegarLoop]: Abstraction has 53 states and 103 transitions.
[2025-04-28 21:21:51,491 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 5 states have call predecessors, (11), 10 states have call successors, (11)
[2025-04-28 21:21:51,491 INFO  L278                IsEmpty]: Start isEmpty. Operand 53 states and 103 transitions.
[2025-04-28 21:21:51,492 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:51,497 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,497 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:51,503 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:51,697 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,697 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,698 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,698 INFO  L85        PathProgramCache]: Analyzing trace with hash 1429890181, now seen corresponding path program 1 times
[2025-04-28 21:21:51,698 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,698 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [533055316]
[2025-04-28 21:21:51,699 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,699 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,702 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:51,706 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:51,706 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,706 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,791 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:51,791 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,792 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [533055316]
[2025-04-28 21:21:51,792 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [533055316] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:51,792 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1782731051]
[2025-04-28 21:21:51,792 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,792 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,795 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:51,797 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:51,800 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:51,839 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:51,852 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:51,852 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,852 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,853 INFO  L256         TraceCheckSpWp]: Trace formula consists of 86 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:51,855 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:51,913 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:51,913 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,415 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:52,415 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1782731051] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,415 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,415 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:52,415 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1884838475]
[2025-04-28 21:21:52,415 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,416 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:52,416 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,416 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:52,417 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:52,417 INFO  L87              Difference]: Start difference. First operand 53 states and 103 transitions. Second operand  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:52,626 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,629 INFO  L93              Difference]: Finished difference Result 65 states and 132 transitions.
[2025-04-28 21:21:52,630 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:52,630 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10) Word has length 20
[2025-04-28 21:21:52,631 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,632 INFO  L225             Difference]: With dead ends: 65
[2025-04-28 21:21:52,632 INFO  L226             Difference]: Without dead ends: 65
[2025-04-28 21:21:52,632 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 48 GetRequests, 34 SyntacticMatches, 3 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 15 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:52,633 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 6 mSDsluCounter, 145 mSDsCounter, 0 mSdLazyCounter, 156 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 173 SdHoareTripleChecker+Invalid, 174 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 156 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,633 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 173 Invalid, 174 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 156 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:52,638 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 65 states.
[2025-04-28 21:21:52,655 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 65 to 49.
[2025-04-28 21:21:52,656 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 49 states, 19 states have (on average 1.631578947368421) internal successors, (31), 29 states have internal predecessors, (31), 16 states have call successors, (16), 6 states have call predecessors, (16), 13 states have return successors, (46), 13 states have call predecessors, (46), 16 states have call successors, (46)
[2025-04-28 21:21:52,657 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 49 states to 49 states and 93 transitions.
[2025-04-28 21:21:52,657 INFO  L79                 Accepts]: Start accepts. Automaton has 49 states and 93 transitions. Word has length 20
[2025-04-28 21:21:52,658 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,658 INFO  L485      AbstractCegarLoop]: Abstraction has 49 states and 93 transitions.
[2025-04-28 21:21:52,658 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:52,658 INFO  L278                IsEmpty]: Start isEmpty. Operand 49 states and 93 transitions.
[2025-04-28 21:21:52,659 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:52,659 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,659 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,665 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:52,860 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,860 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,861 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,861 INFO  L85        PathProgramCache]: Analyzing trace with hash -1058423851, now seen corresponding path program 2 times
[2025-04-28 21:21:52,861 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,861 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2014946656]
[2025-04-28 21:21:52,861 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:52,861 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,866 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:21:52,873 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:52,873 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:52,874 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,997 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:52,997 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,997 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2014946656]
[2025-04-28 21:21:52,997 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2014946656] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,997 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1549662485]
[2025-04-28 21:21:52,997 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:52,998 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,000 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,002 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:53,006 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,050 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:21:53,067 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:53,068 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:53,068 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,069 INFO  L256         TraceCheckSpWp]: Trace formula consists of 108 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,070 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,163 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:53,163 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,987 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:53,987 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1549662485] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,987 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,987 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 14
[2025-04-28 21:21:53,987 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [972433851]
[2025-04-28 21:21:53,987 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,988 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:53,988 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,988 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:53,989 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=145, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:53,989 INFO  L87              Difference]: Start difference. First operand 49 states and 93 transitions. Second operand  has 14 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 14 states have internal predecessors, (18), 8 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 8 states have call successors, (12)
[2025-04-28 21:21:54,348 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,348 INFO  L93              Difference]: Finished difference Result 95 states and 149 transitions.
[2025-04-28 21:21:54,349 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:54,349 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 14 states have internal predecessors, (18), 8 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 8 states have call successors, (12) Word has length 24
[2025-04-28 21:21:54,349 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,350 INFO  L225             Difference]: With dead ends: 95
[2025-04-28 21:21:54,352 INFO  L226             Difference]: Without dead ends: 73
[2025-04-28 21:21:54,352 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 63 GetRequests, 42 SyntacticMatches, 1 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 59 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=112, Invalid=350, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:54,353 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 18 mSDsluCounter, 147 mSDsCounter, 0 mSdLazyCounter, 206 mSolverCounterSat, 58 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 179 SdHoareTripleChecker+Invalid, 264 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 58 IncrementalHoareTripleChecker+Valid, 206 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,354 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 179 Invalid, 264 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [58 Valid, 206 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:54,354 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 73 states.
[2025-04-28 21:21:54,369 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 73 to 51.
[2025-04-28 21:21:54,370 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 51 states, 20 states have (on average 1.65) internal successors, (33), 30 states have internal predecessors, (33), 17 states have call successors, (17), 7 states have call predecessors, (17), 13 states have return successors, (34), 13 states have call predecessors, (34), 17 states have call successors, (34)
[2025-04-28 21:21:54,370 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 51 states to 51 states and 84 transitions.
[2025-04-28 21:21:54,370 INFO  L79                 Accepts]: Start accepts. Automaton has 51 states and 84 transitions. Word has length 24
[2025-04-28 21:21:54,371 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,371 INFO  L485      AbstractCegarLoop]: Abstraction has 51 states and 84 transitions.
[2025-04-28 21:21:54,371 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 14 states have internal predecessors, (18), 8 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 8 states have call successors, (12)
[2025-04-28 21:21:54,371 INFO  L278                IsEmpty]: Start isEmpty. Operand 51 states and 84 transitions.
[2025-04-28 21:21:54,372 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:54,372 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,372 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,379 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:54,572 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,572 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,573 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,573 INFO  L85        PathProgramCache]: Analyzing trace with hash 558911249, now seen corresponding path program 1 times
[2025-04-28 21:21:54,573 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,573 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [255444241]
[2025-04-28 21:21:54,573 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,573 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,577 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:54,584 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:54,584 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,584 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,704 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:54,704 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,704 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [255444241]
[2025-04-28 21:21:54,704 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [255444241] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,704 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [914868820]
[2025-04-28 21:21:54,704 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,704 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,707 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,709 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:54,711 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,759 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:54,774 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:54,774 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,775 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,775 INFO  L256         TraceCheckSpWp]: Trace formula consists of 108 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,778 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,867 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:54,867 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,189 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:56,190 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [914868820] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,190 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:56,190 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [8, 8] total 15
[2025-04-28 21:21:56,190 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1052132860]
[2025-04-28 21:21:56,190 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,190 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:56,190 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,192 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:56,193 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=41, Invalid=169, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:56,193 INFO  L87              Difference]: Start difference. First operand 51 states and 84 transitions. Second operand  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:56,306 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,306 INFO  L93              Difference]: Finished difference Result 55 states and 91 transitions.
[2025-04-28 21:21:56,307 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:56,308 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 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:56,308 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,309 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:56,309 INFO  L226             Difference]: Without dead ends: 50
[2025-04-28 21:21:56,309 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 40 SyntacticMatches, 3 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 28 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=41, Invalid=169, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:56,309 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 2 mSDsluCounter, 93 mSDsCounter, 0 mSdLazyCounter, 88 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 121 SdHoareTripleChecker+Invalid, 92 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 88 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,310 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 121 Invalid, 92 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 88 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,310 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-04-28 21:21:56,316 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 46.
[2025-04-28 21:21:56,321 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 18 states have (on average 1.6666666666666667) internal successors, (30), 27 states have internal predecessors, (30), 16 states have call successors, (16), 7 states have call predecessors, (16), 11 states have return successors, (28), 11 states have call predecessors, (28), 16 states have call successors, (28)
[2025-04-28 21:21:56,321 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 74 transitions.
[2025-04-28 21:21:56,322 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 74 transitions. Word has length 24
[2025-04-28 21:21:56,322 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,322 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 74 transitions.
[2025-04-28 21:21:56,322 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:56,322 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 74 transitions.
[2025-04-28 21:21:56,323 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:56,323 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,323 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,328 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:56,523 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:21:56,523 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,524 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,524 INFO  L85        PathProgramCache]: Analyzing trace with hash 483595390, now seen corresponding path program 1 times
[2025-04-28 21:21:56,524 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,524 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [176336434]
[2025-04-28 21:21:56,524 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,524 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,529 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:56,535 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:56,535 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,535 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,657 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:56,657 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,657 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [176336434]
[2025-04-28 21:21:56,658 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [176336434] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,658 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [588710928]
[2025-04-28 21:21:56,658 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,658 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,660 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,662 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:56,666 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,724 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:56,741 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:56,741 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,741 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,743 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,744 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,857 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:56,858 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,081 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:58,081 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [588710928] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:58,081 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:58,081 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 15
[2025-04-28 21:21:58,081 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1511333948]
[2025-04-28 21:21:58,081 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,081 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:58,082 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,082 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:58,082 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=172, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:58,082 INFO  L87              Difference]: Start difference. First operand 46 states and 74 transitions. Second operand  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:58,233 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,233 INFO  L93              Difference]: Finished difference Result 68 states and 106 transitions.
[2025-04-28 21:21:58,234 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:58,234 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12) Word has length 24
[2025-04-28 21:21:58,234 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,235 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:21:58,235 INFO  L226             Difference]: Without dead ends: 58
[2025-04-28 21:21:58,235 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 57 GetRequests, 40 SyntacticMatches, 3 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 31 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=45, Invalid=195, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:58,236 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 6 mSDsluCounter, 178 mSDsCounter, 0 mSdLazyCounter, 148 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 206 SdHoareTripleChecker+Invalid, 156 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 148 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,236 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 206 Invalid, 156 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 148 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:58,237 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-04-28 21:21:58,242 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 46.
[2025-04-28 21:21:58,242 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 18 states have (on average 1.6666666666666667) internal successors, (30), 27 states have internal predecessors, (30), 16 states have call successors, (16), 7 states have call predecessors, (16), 11 states have return successors, (27), 11 states have call predecessors, (27), 16 states have call successors, (27)
[2025-04-28 21:21:58,246 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 73 transitions.
[2025-04-28 21:21:58,246 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 73 transitions. Word has length 24
[2025-04-28 21:21:58,247 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,247 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 73 transitions.
[2025-04-28 21:21:58,247 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:58,247 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 73 transitions.
[2025-04-28 21:21:58,248 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:58,248 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,248 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,254 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:58,449 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable10
[2025-04-28 21:21:58,449 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,449 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,449 INFO  L85        PathProgramCache]: Analyzing trace with hash 1677347535, now seen corresponding path program 1 times
[2025-04-28 21:21:58,449 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,449 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1236292689]
[2025-04-28 21:21:58,449 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,450 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,453 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:58,457 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:58,457 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,457 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,560 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:58,560 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,560 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1236292689]
[2025-04-28 21:21:58,560 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1236292689] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,560 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [162759645]
[2025-04-28 21:21:58,560 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,560 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,563 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:58,565 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:58,569 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,633 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:58,649 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:58,650 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,650 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,651 INFO  L256         TraceCheckSpWp]: Trace formula consists of 108 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,652 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,722 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:58,722 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,465 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:59,465 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [162759645] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,466 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,466 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 16
[2025-04-28 21:21:59,466 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [271586644]
[2025-04-28 21:21:59,466 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,467 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:59,468 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,468 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:59,468 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=45, Invalid=195, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:59,469 INFO  L87              Difference]: Start difference. First operand 46 states and 73 transitions. Second operand  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:59,676 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,676 INFO  L93              Difference]: Finished difference Result 66 states and 108 transitions.
[2025-04-28 21:21:59,677 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:59,677 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13) Word has length 24
[2025-04-28 21:21:59,677 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,677 INFO  L225             Difference]: With dead ends: 66
[2025-04-28 21:21:59,678 INFO  L226             Difference]: Without dead ends: 64
[2025-04-28 21:21:59,678 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 59 GetRequests, 40 SyntacticMatches, 3 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 41 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=56, Invalid=250, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:59,678 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 7 mSDsluCounter, 209 mSDsCounter, 0 mSdLazyCounter, 253 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 240 SdHoareTripleChecker+Invalid, 265 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 253 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,679 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 240 Invalid, 265 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 253 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:59,679 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 64 states.
[2025-04-28 21:21:59,684 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 64 to 48.
[2025-04-28 21:21:59,684 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 19 states have (on average 1.631578947368421) internal successors, (31), 28 states have internal predecessors, (31), 16 states have call successors, (16), 7 states have call predecessors, (16), 12 states have return successors, (28), 12 states have call predecessors, (28), 16 states have call successors, (28)
[2025-04-28 21:21:59,685 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 75 transitions.
[2025-04-28 21:21:59,685 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 75 transitions. Word has length 24
[2025-04-28 21:21:59,685 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,685 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 75 transitions.
[2025-04-28 21:21:59,685 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:59,685 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 75 transitions.
[2025-04-28 21:21:59,686 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:59,686 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,686 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,691 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:59,890 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-04-28 21:21:59,890 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,890 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,890 INFO  L85        PathProgramCache]: Analyzing trace with hash -1994961437, now seen corresponding path program 1 times
[2025-04-28 21:21:59,890 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,891 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [684328316]
[2025-04-28 21:21:59,891 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,891 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,894 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:59,901 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:59,901 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,901 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,186 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:00,186 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,186 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [684328316]
[2025-04-28 21:22:00,186 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [684328316] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,187 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [510586932]
[2025-04-28 21:22:00,187 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,187 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,189 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,191 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:00,193 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,268 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:00,289 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:00,289 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,289 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,291 INFO  L256         TraceCheckSpWp]: Trace formula consists of 138 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,293 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,554 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:22:00,555 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,768 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:22:01,769 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [510586932] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,769 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,769 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 12, 12] total 24
[2025-04-28 21:22:01,769 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [797642530]
[2025-04-28 21:22:01,769 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,769 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:22:01,769 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,770 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:22:01,770 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=72, Invalid=480, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:22:01,770 INFO  L87              Difference]: Start difference. First operand 48 states and 75 transitions. Second operand  has 24 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 23 states have internal predecessors, (27), 14 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (17), 9 states have call predecessors, (17), 14 states have call successors, (17)
[2025-04-28 21:22:02,384 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,384 INFO  L93              Difference]: Finished difference Result 94 states and 149 transitions.
[2025-04-28 21:22:02,385 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 22 states. 
[2025-04-28 21:22:02,385 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 23 states have internal predecessors, (27), 14 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (17), 9 states have call predecessors, (17), 14 states have call successors, (17) Word has length 28
[2025-04-28 21:22:02,385 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,386 INFO  L225             Difference]: With dead ends: 94
[2025-04-28 21:22:02,386 INFO  L226             Difference]: Without dead ends: 90
[2025-04-28 21:22:02,386 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 79 GetRequests, 45 SyntacticMatches, 0 SemanticMatches, 34 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 218 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=177, Invalid=1083, Unknown=0, NotChecked=0, Total=1260
[2025-04-28 21:22:02,386 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 19 mSDsluCounter, 273 mSDsCounter, 0 mSdLazyCounter, 373 mSolverCounterSat, 23 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 33 SdHoareTripleChecker+Valid, 301 SdHoareTripleChecker+Invalid, 396 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 23 IncrementalHoareTripleChecker+Valid, 373 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,387 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [33 Valid, 301 Invalid, 396 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [23 Valid, 373 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:02,387 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-04-28 21:22:02,393 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 52.
[2025-04-28 21:22:02,394 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 21 states have (on average 1.5714285714285714) internal successors, (33), 30 states have internal predecessors, (33), 16 states have call successors, (16), 7 states have call predecessors, (16), 14 states have return successors, (34), 14 states have call predecessors, (34), 16 states have call successors, (34)
[2025-04-28 21:22:02,394 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 83 transitions.
[2025-04-28 21:22:02,394 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 83 transitions. Word has length 28
[2025-04-28 21:22:02,395 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:02,395 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 83 transitions.
[2025-04-28 21:22:02,395 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 23 states have internal predecessors, (27), 14 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (17), 9 states have call predecessors, (17), 14 states have call successors, (17)
[2025-04-28 21:22:02,395 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 83 transitions.
[2025-04-28 21:22:02,396 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:02,396 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:02,396 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:02,402 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:22:02,600 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:22:02,600 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,600 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,600 INFO  L85        PathProgramCache]: Analyzing trace with hash 954857288, now seen corresponding path program 1 times
[2025-04-28 21:22:02,600 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,600 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [749937483]
[2025-04-28 21:22:02,600 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:02,601 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,604 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:02,608 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:02,609 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,609 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,736 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:22:02,737 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,737 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [749937483]
[2025-04-28 21:22:02,737 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [749937483] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,737 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1271870230]
[2025-04-28 21:22:02,737 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:02,737 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,739 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:02,742 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:02,746 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,832 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:02,853 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:02,853 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,853 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,854 INFO  L256         TraceCheckSpWp]: Trace formula consists of 142 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,855 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,939 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:22:02,939 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:03,951 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:22:03,951 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1271870230] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:03,951 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:03,951 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 17
[2025-04-28 21:22:03,951 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1541841145]
[2025-04-28 21:22:03,952 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,952 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:22:03,952 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,952 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:22:03,953 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=47, Invalid=225, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:22:03,953 INFO  L87              Difference]: Start difference. First operand 52 states and 83 transitions. Second operand  has 17 states, 8 states have (on average 2.625) internal successors, (21), 17 states have internal predecessors, (21), 10 states have call successors, (12), 1 states have call predecessors, (12), 7 states have return successors, (14), 6 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:22:04,322 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,322 INFO  L93              Difference]: Finished difference Result 88 states and 137 transitions.
[2025-04-28 21:22:04,322 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:22:04,323 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.625) internal successors, (21), 17 states have internal predecessors, (21), 10 states have call successors, (12), 1 states have call predecessors, (12), 7 states have return successors, (14), 6 states have call predecessors, (14), 10 states have call successors, (14) Word has length 28
[2025-04-28 21:22:04,323 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,324 INFO  L225             Difference]: With dead ends: 88
[2025-04-28 21:22:04,324 INFO  L226             Difference]: Without dead ends: 86
[2025-04-28 21:22:04,324 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 72 GetRequests, 48 SyntacticMatches, 2 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 75 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=105, Invalid=447, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:22:04,325 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 13 mSDsluCounter, 204 mSDsCounter, 0 mSdLazyCounter, 292 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 235 SdHoareTripleChecker+Invalid, 326 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 292 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,325 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 235 Invalid, 326 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 292 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:04,326 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-04-28 21:22:04,336 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 60.
[2025-04-28 21:22:04,337 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 60 states, 25 states have (on average 1.48) internal successors, (37), 34 states have internal predecessors, (37), 16 states have call successors, (16), 7 states have call predecessors, (16), 18 states have return successors, (44), 18 states have call predecessors, (44), 16 states have call successors, (44)
[2025-04-28 21:22:04,337 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 60 states to 60 states and 97 transitions.
[2025-04-28 21:22:04,337 INFO  L79                 Accepts]: Start accepts. Automaton has 60 states and 97 transitions. Word has length 28
[2025-04-28 21:22:04,337 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,340 INFO  L485      AbstractCegarLoop]: Abstraction has 60 states and 97 transitions.
[2025-04-28 21:22:04,340 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.625) internal successors, (21), 17 states have internal predecessors, (21), 10 states have call successors, (12), 1 states have call predecessors, (12), 7 states have return successors, (14), 6 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:22:04,340 INFO  L278                IsEmpty]: Start isEmpty. Operand 60 states and 97 transitions.
[2025-04-28 21:22:04,341 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:04,341 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,341 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:04,345 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-04-28 21:22:04,542 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,542 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,542 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,542 INFO  L85        PathProgramCache]: Analyzing trace with hash 1734441497, now seen corresponding path program 2 times
[2025-04-28 21:22:04,542 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,542 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [741186871]
[2025-04-28 21:22:04,542 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:04,543 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,546 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:22:04,550 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:04,551 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:04,551 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,704 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:04,704 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,704 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [741186871]
[2025-04-28 21:22:04,705 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [741186871] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:04,705 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1478816237]
[2025-04-28 21:22:04,705 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:04,705 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,707 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:04,709 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:04,713 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:22:04,800 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:22:04,818 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:04,818 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:04,819 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,820 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:04,821 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:04,931 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:04,931 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:06,751 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:06,752 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1478816237] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:06,752 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:06,752 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 8, 8] total 17
[2025-04-28 21:22:06,752 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1618671820]
[2025-04-28 21:22:06,752 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:06,752 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:22:06,752 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:06,753 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:22:06,753 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=39, Invalid=233, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:22:06,753 INFO  L87              Difference]: Start difference. First operand 60 states and 97 transitions. Second operand  has 17 states, 9 states have (on average 2.5555555555555554) internal successors, (23), 17 states have internal predecessors, (23), 9 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (15), 8 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:22:07,019 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,019 INFO  L93              Difference]: Finished difference Result 68 states and 105 transitions.
[2025-04-28 21:22:07,020 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:07,020 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 9 states have (on average 2.5555555555555554) internal successors, (23), 17 states have internal predecessors, (23), 9 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (15), 8 states have call predecessors, (15), 9 states have call successors, (15) Word has length 28
[2025-04-28 21:22:07,020 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,021 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:22:07,021 INFO  L226             Difference]: Without dead ends: 63
[2025-04-28 21:22:07,021 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 73 GetRequests, 52 SyntacticMatches, 0 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 34 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=83, Invalid=423, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:22:07,022 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 13 mSDsluCounter, 186 mSDsCounter, 0 mSdLazyCounter, 184 mSolverCounterSat, 32 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 213 SdHoareTripleChecker+Invalid, 216 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 32 IncrementalHoareTripleChecker+Valid, 184 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,023 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 213 Invalid, 216 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [32 Valid, 184 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:07,024 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 63 states.
[2025-04-28 21:22:07,030 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 63 to 59.
[2025-04-28 21:22:07,030 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 59 states, 25 states have (on average 1.44) internal successors, (36), 33 states have internal predecessors, (36), 15 states have call successors, (15), 7 states have call predecessors, (15), 18 states have return successors, (43), 18 states have call predecessors, (43), 15 states have call successors, (43)
[2025-04-28 21:22:07,031 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 59 states to 59 states and 94 transitions.
[2025-04-28 21:22:07,031 INFO  L79                 Accepts]: Start accepts. Automaton has 59 states and 94 transitions. Word has length 28
[2025-04-28 21:22:07,031 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,031 INFO  L485      AbstractCegarLoop]: Abstraction has 59 states and 94 transitions.
[2025-04-28 21:22:07,032 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 9 states have (on average 2.5555555555555554) internal successors, (23), 17 states have internal predecessors, (23), 9 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (15), 8 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:22:07,032 INFO  L278                IsEmpty]: Start isEmpty. Operand 59 states and 94 transitions.
[2025-04-28 21:22:07,033 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:07,033 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,033 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:07,039 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Ended with exit code 0
[2025-04-28 21:22:07,237 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable14
[2025-04-28 21:22:07,237 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,237 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,237 INFO  L85        PathProgramCache]: Analyzing trace with hash -478910543, now seen corresponding path program 1 times
[2025-04-28 21:22:07,237 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,238 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [677960379]
[2025-04-28 21:22:07,238 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,238 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,242 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:07,248 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:07,248 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,248 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,289 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:22:07,289 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,289 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [677960379]
[2025-04-28 21:22:07,289 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [677960379] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:07,289 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:07,289 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:07,290 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1306202281]
[2025-04-28 21:22:07,290 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,291 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:07,291 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,291 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:07,291 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:07,292 INFO  L87              Difference]: Start difference. First operand 59 states and 94 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), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:22:07,365 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,365 INFO  L93              Difference]: Finished difference Result 82 states and 137 transitions.
[2025-04-28 21:22:07,367 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:07,367 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), 2 states have call predecessors, (7), 3 states have call successors, (7) Word has length 32
[2025-04-28 21:22:07,367 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,368 INFO  L225             Difference]: With dead ends: 82
[2025-04-28 21:22:07,369 INFO  L226             Difference]: Without dead ends: 82
[2025-04-28 21:22:07,369 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:07,370 INFO  L437           NwaCegarLoop]: 37 mSDtfsCounter, 5 mSDsluCounter, 49 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 86 SdHoareTripleChecker+Invalid, 47 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 44 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,372 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 86 Invalid, 47 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:07,372 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-04-28 21:22:07,379 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 68.
[2025-04-28 21:22:07,379 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 68 states, 29 states have (on average 1.4827586206896552) internal successors, (43), 39 states have internal predecessors, (43), 17 states have call successors, (17), 8 states have call predecessors, (17), 21 states have return successors, (55), 20 states have call predecessors, (55), 17 states have call successors, (55)
[2025-04-28 21:22:07,380 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 68 states to 68 states and 115 transitions.
[2025-04-28 21:22:07,381 INFO  L79                 Accepts]: Start accepts. Automaton has 68 states and 115 transitions. Word has length 32
[2025-04-28 21:22:07,381 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,381 INFO  L485      AbstractCegarLoop]: Abstraction has 68 states and 115 transitions.
[2025-04-28 21:22:07,381 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), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:22:07,381 INFO  L278                IsEmpty]: Start isEmpty. Operand 68 states and 115 transitions.
[2025-04-28 21:22:07,385 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:07,385 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,385 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:07,385 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:22:07,386 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,386 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,386 INFO  L85        PathProgramCache]: Analyzing trace with hash 1709851734, now seen corresponding path program 1 times
[2025-04-28 21:22:07,386 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,386 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2134645405]
[2025-04-28 21:22:07,386 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,386 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,392 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:07,398 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:07,398 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,399 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,442 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:22:07,443 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,443 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2134645405]
[2025-04-28 21:22:07,443 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2134645405] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:07,443 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:07,443 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:07,443 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1175198507]
[2025-04-28 21:22:07,443 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,444 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:07,444 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,444 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:07,445 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:07,445 INFO  L87              Difference]: Start difference. First operand 68 states and 115 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), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:22:07,518 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,519 INFO  L93              Difference]: Finished difference Result 76 states and 127 transitions.
[2025-04-28 21:22:07,519 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:07,520 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), 2 states have call predecessors, (7), 3 states have call successors, (7) Word has length 32
[2025-04-28 21:22:07,520 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,522 INFO  L225             Difference]: With dead ends: 76
[2025-04-28 21:22:07,522 INFO  L226             Difference]: Without dead ends: 72
[2025-04-28 21:22:07,522 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:07,523 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 5 mSDsluCounter, 47 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 83 SdHoareTripleChecker+Invalid, 44 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,523 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 83 Invalid, 44 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:07,524 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 72 states.
[2025-04-28 21:22:07,531 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 72 to 64.
[2025-04-28 21:22:07,531 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 64 states, 27 states have (on average 1.4814814814814814) internal successors, (40), 36 states have internal predecessors, (40), 17 states have call successors, (17), 8 states have call predecessors, (17), 19 states have return successors, (49), 19 states have call predecessors, (49), 17 states have call successors, (49)
[2025-04-28 21:22:07,532 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 64 states to 64 states and 106 transitions.
[2025-04-28 21:22:07,533 INFO  L79                 Accepts]: Start accepts. Automaton has 64 states and 106 transitions. Word has length 32
[2025-04-28 21:22:07,533 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,533 INFO  L485      AbstractCegarLoop]: Abstraction has 64 states and 106 transitions.
[2025-04-28 21:22:07,533 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), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:22:07,533 INFO  L278                IsEmpty]: Start isEmpty. Operand 64 states and 106 transitions.
[2025-04-28 21:22:07,534 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:07,535 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,535 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:07,535 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:22:07,535 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,536 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,536 INFO  L85        PathProgramCache]: Analyzing trace with hash 1682701229, now seen corresponding path program 2 times
[2025-04-28 21:22:07,536 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,536 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1980330558]
[2025-04-28 21:22:07,536 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:07,536 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,541 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:22:07,549 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:07,549 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:07,549 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,684 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 12 proven. 3 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:07,684 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,684 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1980330558]
[2025-04-28 21:22:07,684 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1980330558] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,684 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [313480015]
[2025-04-28 21:22:07,685 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:07,685 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,687 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:07,688 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:07,691 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,797 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:22:07,818 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:07,818 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:07,818 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,820 INFO  L256         TraceCheckSpWp]: Trace formula consists of 160 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,821 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:07,933 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 12 proven. 3 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:07,933 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:09,723 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 12 proven. 3 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:09,723 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [313480015] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:09,723 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:09,723 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 12] total 20
[2025-04-28 21:22:09,723 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1477591023]
[2025-04-28 21:22:09,723 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:09,724 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:22:09,724 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:09,724 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:22:09,724 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=64, Invalid=316, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:22:09,725 INFO  L87              Difference]: Start difference. First operand 64 states and 106 transitions. Second operand  has 20 states, 10 states have (on average 2.5) internal successors, (25), 20 states have internal predecessors, (25), 11 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:22:10,083 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:10,083 INFO  L93              Difference]: Finished difference Result 98 states and 155 transitions.
[2025-04-28 21:22:10,083 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:22:10,084 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.5) internal successors, (25), 20 states have internal predecessors, (25), 11 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17) Word has length 32
[2025-04-28 21:22:10,084 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:10,085 INFO  L225             Difference]: With dead ends: 98
[2025-04-28 21:22:10,085 INFO  L226             Difference]: Without dead ends: 90
[2025-04-28 21:22:10,085 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 81 GetRequests, 55 SyntacticMatches, 2 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 100 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=125, Invalid=525, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:22:10,086 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 15 mSDsluCounter, 247 mSDsCounter, 0 mSdLazyCounter, 297 mSolverCounterSat, 36 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 278 SdHoareTripleChecker+Invalid, 333 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 36 IncrementalHoareTripleChecker+Valid, 297 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:10,086 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 278 Invalid, 333 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [36 Valid, 297 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:10,086 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-04-28 21:22:10,099 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 72.
[2025-04-28 21:22:10,099 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 72 states, 31 states have (on average 1.4193548387096775) internal successors, (44), 40 states have internal predecessors, (44), 17 states have call successors, (17), 8 states have call predecessors, (17), 23 states have return successors, (55), 23 states have call predecessors, (55), 17 states have call successors, (55)
[2025-04-28 21:22:10,100 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 72 states to 72 states and 116 transitions.
[2025-04-28 21:22:10,100 INFO  L79                 Accepts]: Start accepts. Automaton has 72 states and 116 transitions. Word has length 32
[2025-04-28 21:22:10,100 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:10,100 INFO  L485      AbstractCegarLoop]: Abstraction has 72 states and 116 transitions.
[2025-04-28 21:22:10,100 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.5) internal successors, (25), 20 states have internal predecessors, (25), 11 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:22:10,100 INFO  L278                IsEmpty]: Start isEmpty. Operand 72 states and 116 transitions.
[2025-04-28 21:22:10,103 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:10,103 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:10,103 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:10,110 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:10,304 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 13 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable17
[2025-04-28 21:22:10,304 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:10,304 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:10,304 INFO  L85        PathProgramCache]: Analyzing trace with hash -1097877785, now seen corresponding path program 1 times
[2025-04-28 21:22:10,304 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:10,304 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [860614582]
[2025-04-28 21:22:10,304 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:10,304 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:10,309 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:10,316 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:10,316 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:10,316 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,499 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:10,499 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:10,499 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [860614582]
[2025-04-28 21:22:10,499 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [860614582] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:10,499 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1340842309]
[2025-04-28 21:22:10,499 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:10,499 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:10,502 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:10,504 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:10,507 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Waiting until timeout for monitored process
[2025-04-28 21:22:10,647 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:10,668 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:10,668 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:10,668 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,670 INFO  L256         TraceCheckSpWp]: Trace formula consists of 160 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:10,671 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:10,779 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:10,779 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:12,836 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:12,836 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1340842309] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:12,836 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:12,836 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 14] total 22
[2025-04-28 21:22:12,836 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1887346254]
[2025-04-28 21:22:12,836 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,836 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:12,837 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,837 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:12,837 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=73, Invalid=389, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:12,837 INFO  L87              Difference]: Start difference. First operand 72 states and 116 transitions. Second operand  has 22 states, 11 states have (on average 2.272727272727273) internal successors, (25), 21 states have internal predecessors, (25), 12 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (18), 9 states have call predecessors, (18), 12 states have call successors, (18)
[2025-04-28 21:22:13,261 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:13,261 INFO  L93              Difference]: Finished difference Result 120 states and 197 transitions.
[2025-04-28 21:22:13,261 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:22:13,262 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 2.272727272727273) internal successors, (25), 21 states have internal predecessors, (25), 12 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (18), 9 states have call predecessors, (18), 12 states have call successors, (18) Word has length 32
[2025-04-28 21:22:13,262 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:13,264 INFO  L225             Difference]: With dead ends: 120
[2025-04-28 21:22:13,264 INFO  L226             Difference]: Without dead ends: 112
[2025-04-28 21:22:13,264 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 83 GetRequests, 53 SyntacticMatches, 4 SemanticMatches, 26 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 140 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=114, Invalid=642, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:22:13,265 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 12 mSDsluCounter, 247 mSDsCounter, 0 mSdLazyCounter, 377 mSolverCounterSat, 32 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 281 SdHoareTripleChecker+Invalid, 409 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 32 IncrementalHoareTripleChecker+Valid, 377 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:13,265 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 281 Invalid, 409 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [32 Valid, 377 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:13,266 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-04-28 21:22:13,274 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 84.
[2025-04-28 21:22:13,274 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 37 states have (on average 1.3513513513513513) internal successors, (50), 46 states have internal predecessors, (50), 17 states have call successors, (17), 8 states have call predecessors, (17), 29 states have return successors, (71), 29 states have call predecessors, (71), 17 states have call successors, (71)
[2025-04-28 21:22:13,275 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 138 transitions.
[2025-04-28 21:22:13,275 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 138 transitions. Word has length 32
[2025-04-28 21:22:13,275 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,275 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 138 transitions.
[2025-04-28 21:22:13,275 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 2.272727272727273) internal successors, (25), 21 states have internal predecessors, (25), 12 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (18), 9 states have call predecessors, (18), 12 states have call successors, (18)
[2025-04-28 21:22:13,276 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 138 transitions.
[2025-04-28 21:22:13,277 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:13,277 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,277 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:13,287 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Ended with exit code 0
[2025-04-28 21:22:13,477 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,14 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,478 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,478 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,478 INFO  L85        PathProgramCache]: Analyzing trace with hash 1250685809, now seen corresponding path program 2 times
[2025-04-28 21:22:13,478 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,478 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [700128440]
[2025-04-28 21:22:13,478 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:13,478 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,482 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:22:13,489 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:13,489 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:13,489 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,670 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:22:13,670 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,670 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [700128440]
[2025-04-28 21:22:13,670 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [700128440] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:13,670 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1459874601]
[2025-04-28 21:22:13,670 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:13,670 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,673 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:13,675 INFO  L229       MonitoredProcess]: Starting monitored process 15 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:13,678 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Waiting until timeout for monitored process
[2025-04-28 21:22:13,830 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:22:13,854 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:13,854 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:13,854 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,855 INFO  L256         TraceCheckSpWp]: Trace formula consists of 168 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:13,856 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:14,088 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 2 proven. 11 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:14,088 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:16,180 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 2 proven. 12 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:16,181 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1459874601] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:16,181 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:16,181 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 13, 14] total 26
[2025-04-28 21:22:16,181 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [872010454]
[2025-04-28 21:22:16,181 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:16,181 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:22:16,182 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:16,182 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:22:16,182 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=76, Invalid=574, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:22:16,183 INFO  L87              Difference]: Start difference. First operand 84 states and 138 transitions. Second operand  has 26 states, 12 states have (on average 2.5) internal successors, (30), 26 states have internal predecessors, (30), 15 states have call successors, (17), 1 states have call predecessors, (17), 11 states have return successors, (20), 10 states have call predecessors, (20), 15 states have call successors, (20)
[2025-04-28 21:22:16,952 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:16,952 INFO  L93              Difference]: Finished difference Result 152 states and 241 transitions.
[2025-04-28 21:22:16,952 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 27 states. 
[2025-04-28 21:22:16,953 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 12 states have (on average 2.5) internal successors, (30), 26 states have internal predecessors, (30), 15 states have call successors, (17), 1 states have call predecessors, (17), 11 states have return successors, (20), 10 states have call predecessors, (20), 15 states have call successors, (20) Word has length 32
[2025-04-28 21:22:16,953 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:16,954 INFO  L225             Difference]: With dead ends: 152
[2025-04-28 21:22:16,954 INFO  L226             Difference]: Without dead ends: 121
[2025-04-28 21:22:16,955 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 96 GetRequests, 48 SyntacticMatches, 4 SemanticMatches, 44 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 341 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=292, Invalid=1778, Unknown=0, NotChecked=0, Total=2070
[2025-04-28 21:22:16,955 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 23 mSDsluCounter, 335 mSDsCounter, 0 mSdLazyCounter, 419 mSolverCounterSat, 62 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 366 SdHoareTripleChecker+Invalid, 481 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 62 IncrementalHoareTripleChecker+Valid, 419 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:16,956 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 366 Invalid, 481 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [62 Valid, 419 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:16,956 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 121 states.
[2025-04-28 21:22:16,968 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 121 to 69.
[2025-04-28 21:22:16,968 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 69 states, 31 states have (on average 1.2903225806451613) internal successors, (40), 37 states have internal predecessors, (40), 13 states have call successors, (13), 7 states have call predecessors, (13), 24 states have return successors, (55), 24 states have call predecessors, (55), 13 states have call successors, (55)
[2025-04-28 21:22:16,970 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 69 states to 69 states and 108 transitions.
[2025-04-28 21:22:16,970 INFO  L79                 Accepts]: Start accepts. Automaton has 69 states and 108 transitions. Word has length 32
[2025-04-28 21:22:16,970 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:16,970 INFO  L485      AbstractCegarLoop]: Abstraction has 69 states and 108 transitions.
[2025-04-28 21:22:16,971 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 12 states have (on average 2.5) internal successors, (30), 26 states have internal predecessors, (30), 15 states have call successors, (17), 1 states have call predecessors, (17), 11 states have return successors, (20), 10 states have call predecessors, (20), 15 states have call successors, (20)
[2025-04-28 21:22:16,971 INFO  L278                IsEmpty]: Start isEmpty. Operand 69 states and 108 transitions.
[2025-04-28 21:22:16,972 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:16,972 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:16,972 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:16,980 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Ended with exit code 0
[2025-04-28 21:22:17,173 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19,15 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:17,173 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:17,174 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:17,174 INFO  L85        PathProgramCache]: Analyzing trace with hash 631718567, now seen corresponding path program 2 times
[2025-04-28 21:22:17,174 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:17,174 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [507313392]
[2025-04-28 21:22:17,174 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:17,174 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:17,178 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:22:17,184 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:17,184 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:17,184 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:17,226 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:22:17,226 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:17,226 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [507313392]
[2025-04-28 21:22:17,226 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [507313392] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:17,226 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:17,227 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:17,227 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [163324820]
[2025-04-28 21:22:17,227 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:17,227 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:17,227 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:17,227 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:17,228 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:17,228 INFO  L87              Difference]: Start difference. First operand 69 states and 108 transitions. Second operand  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:22:17,291 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:17,291 INFO  L93              Difference]: Finished difference Result 82 states and 118 transitions.
[2025-04-28 21:22:17,291 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:17,291 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:22:17,291 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:17,292 INFO  L225             Difference]: With dead ends: 82
[2025-04-28 21:22:17,292 INFO  L226             Difference]: Without dead ends: 75
[2025-04-28 21:22:17,292 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:17,293 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 4 mSDsluCounter, 42 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 77 SdHoareTripleChecker+Invalid, 46 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 44 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:17,293 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 77 Invalid, 46 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:17,294 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 75 states.
[2025-04-28 21:22:17,297 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 75 to 71.
[2025-04-28 21:22:17,298 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 71 states, 32 states have (on average 1.34375) internal successors, (43), 39 states have internal predecessors, (43), 14 states have call successors, (14), 8 states have call predecessors, (14), 24 states have return successors, (44), 24 states have call predecessors, (44), 14 states have call successors, (44)
[2025-04-28 21:22:17,298 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 71 states to 71 states and 101 transitions.
[2025-04-28 21:22:17,298 INFO  L79                 Accepts]: Start accepts. Automaton has 71 states and 101 transitions. Word has length 32
[2025-04-28 21:22:17,299 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:17,299 INFO  L485      AbstractCegarLoop]: Abstraction has 71 states and 101 transitions.
[2025-04-28 21:22:17,299 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:22:17,299 INFO  L278                IsEmpty]: Start isEmpty. Operand 71 states and 101 transitions.
[2025-04-28 21:22:17,300 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:17,300 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:17,300 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:17,300 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-04-28 21:22:17,300 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:17,300 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:17,301 INFO  L85        PathProgramCache]: Analyzing trace with hash -1015320527, now seen corresponding path program 1 times
[2025-04-28 21:22:17,301 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:17,301 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1614777315]
[2025-04-28 21:22:17,301 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:17,301 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:17,306 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
