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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:40,060 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:40,139 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e4bc8058-ac30-4677-ac1d-7fbaf29e1a42/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:40,143 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:40,143 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:40,165 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:40,165 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:40,165 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:40,166 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:40,166 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:40,166 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:40,166 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:40,166 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:40,166 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:40,166 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:40,167 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:40,167 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:40,167 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:40,167 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,167 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:40,167 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:40,167 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:40,168 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:40,168 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:40,168 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:40,168 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:40,169 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:40,492 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:40,504 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:40,506 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:40,507 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:40,509 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:40,510 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e4bc8058-ac30-4677-ac1d-7fbaf29e1a42/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-169.smt2
[2025-04-28 21:21:40,512 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:40,519 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:40,730 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e4bc8058-ac30-4677-ac1d-7fbaf29e1a42/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-169.smt2
[2025-04-28 21:21:40,733 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:40,736 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:40,738 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:40,738 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:40,738 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:40,744 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,768 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40 Unit
[2025-04-28 21:21:40,769 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:40,770 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:40,771 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:40,771 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:40,787 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,787 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,820 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,820 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,822 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,824 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,826 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,827 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,831 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,847 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:40,848 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:40,849 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:40,849 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:40,850 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,853 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,868 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,883 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:40,890 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:40,902 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:40,902 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:40,902 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:40,902 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure END_QUERY given in one single declaration
[2025-04-28 21:21:40,902 INFO  L130     BoogieDeclarations]: Found specification of procedure END_QUERY
[2025-04-28 21:21:40,902 INFO  L138     BoogieDeclarations]: Found implementation of procedure END_QUERY
[2025-04-28 21:21:40,903 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_42 given in one single declaration
[2025-04-28 21:21:40,903 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_42
[2025-04-28 21:21:40,903 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_42
[2025-04-28 21:21:40,903 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:40,903 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:40,903 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:40,953 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:40,955 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:41,079 INFO  L?                        ?]: Removed 2 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:41,081 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:41,094 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:41,095 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:41,095 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41 BoogieIcfgContainer
[2025-04-28 21:21:41,096 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:41,099 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:41,099 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:41,105 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:41,105 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/3) ...
[2025-04-28 21:21:41,106 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@23662722 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,106 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (2/3) ...
[2025-04-28 21:21:41,106 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@23662722 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,107 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41" (3/3) ...
[2025-04-28 21:21:41,113 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:41,132 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:41,135 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 18 locations, 29 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:41,182 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:41,194 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;@52436190, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:41,194 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:41,201 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 18 states, 7 states have (on average 1.5714285714285714) internal successors, (11), 11 states have internal predecessors, (11), 6 states have call successors, (6), 3 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 6 states have call successors, (6)
[2025-04-28 21:21:41,211 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:41,211 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,212 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,213 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,220 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,220 INFO  L85        PathProgramCache]: Analyzing trace with hash -2047640260, now seen corresponding path program 1 times
[2025-04-28 21:21:41,229 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,230 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1743318324]
[2025-04-28 21:21:41,230 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,231 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,271 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:41,314 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:41,315 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,315 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,615 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:41,616 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,616 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1743318324]
[2025-04-28 21:21:41,619 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1743318324] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,620 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,625 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:41,627 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1441123082]
[2025-04-28 21:21:41,632 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,636 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:41,637 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,671 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:41,671 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:41,673 INFO  L87              Difference]: Start difference. First operand  has 18 states, 7 states have (on average 1.5714285714285714) internal successors, (11), 11 states have internal predecessors, (11), 6 states have call successors, (6), 3 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 6 states have call successors, (6) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:41,767 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,768 INFO  L93              Difference]: Finished difference Result 18 states and 25 transitions.
[2025-04-28 21:21:41,774 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:41,775 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:41,775 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,784 INFO  L225             Difference]: With dead ends: 18
[2025-04-28 21:21:41,784 INFO  L226             Difference]: Without dead ends: 18
[2025-04-28 21:21:41,786 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:41,789 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 1 mSDsluCounter, 26 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 44 SdHoareTripleChecker+Invalid, 16 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,790 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 44 Invalid, 16 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:41,804 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 18 states.
[2025-04-28 21:21:41,849 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 18 to 18.
[2025-04-28 21:21:41,852 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 18 states, 7 states have (on average 1.4285714285714286) internal successors, (10), 10 states have internal predecessors, (10), 6 states have call successors, (6), 3 states have call predecessors, (6), 4 states have return successors, (9), 5 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:21:41,857 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 18 states to 18 states and 25 transitions.
[2025-04-28 21:21:41,859 INFO  L79                 Accepts]: Start accepts. Automaton has 18 states and 25 transitions. Word has length 12
[2025-04-28 21:21:41,862 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,862 INFO  L485      AbstractCegarLoop]: Abstraction has 18 states and 25 transitions.
[2025-04-28 21:21:41,862 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:41,863 INFO  L278                IsEmpty]: Start isEmpty. Operand 18 states and 25 transitions.
[2025-04-28 21:21:41,864 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:41,865 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,865 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,866 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:41,867 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,868 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,868 INFO  L85        PathProgramCache]: Analyzing trace with hash 1531061121, now seen corresponding path program 1 times
[2025-04-28 21:21:41,869 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,869 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [808647478]
[2025-04-28 21:21:41,869 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,869 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,883 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:41,898 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:41,898 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,898 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,217 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:42,218 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,218 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [808647478]
[2025-04-28 21:21:42,218 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [808647478] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,218 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [745639113]
[2025-04-28 21:21:42,218 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,219 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,223 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,230 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:42,231 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,287 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:42,319 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:42,319 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,319 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,323 INFO  L256         TraceCheckSpWp]: Trace formula consists of 68 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,334 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,454 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:42,454 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,006 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:43,006 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [745639113] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,007 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,011 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:43,012 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1381852691]
[2025-04-28 21:21:43,012 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,013 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:43,013 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,015 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:43,015 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=65, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:43,016 INFO  L87              Difference]: Start difference. First operand 18 states and 25 transitions. Second operand  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:43,197 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,197 INFO  L93              Difference]: Finished difference Result 26 states and 43 transitions.
[2025-04-28 21:21:43,198 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:43,198 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8) Word has length 16
[2025-04-28 21:21:43,199 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,199 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:43,200 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:43,200 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 29 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=78, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:43,201 INFO  L437           NwaCegarLoop]: 19 mSDtfsCounter, 4 mSDsluCounter, 69 mSDsCounter, 0 mSdLazyCounter, 85 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 88 SdHoareTripleChecker+Invalid, 93 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 85 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,202 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 88 Invalid, 93 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 85 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:43,202 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:43,209 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 22.
[2025-04-28 21:21:43,209 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 9 states have (on average 1.3333333333333333) internal successors, (12), 12 states have internal predecessors, (12), 6 states have call successors, (6), 3 states have call predecessors, (6), 6 states have return successors, (15), 6 states have call predecessors, (15), 6 states have call successors, (15)
[2025-04-28 21:21:43,210 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 33 transitions.
[2025-04-28 21:21:43,210 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 33 transitions. Word has length 16
[2025-04-28 21:21:43,210 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,210 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 33 transitions.
[2025-04-28 21:21:43,210 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:43,210 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 33 transitions.
[2025-04-28 21:21:43,211 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:43,211 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,212 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,217 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:43,412 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,412 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,413 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,413 INFO  L85        PathProgramCache]: Analyzing trace with hash 1810027230, now seen corresponding path program 1 times
[2025-04-28 21:21:43,413 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,413 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1012207937]
[2025-04-28 21:21:43,413 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,413 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,418 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:43,427 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:43,427 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,427 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,609 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:43,610 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,610 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1012207937]
[2025-04-28 21:21:43,610 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1012207937] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,610 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1870933667]
[2025-04-28 21:21:43,610 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,610 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,613 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,616 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,617 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,646 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:43,663 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:43,663 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,663 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,664 INFO  L256         TraceCheckSpWp]: Trace formula consists of 72 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,666 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,878 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:43,882 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,491 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:45,491 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1870933667] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,492 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,493 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 11
[2025-04-28 21:21:45,493 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [705492913]
[2025-04-28 21:21:45,493 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,493 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:45,493 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,494 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:45,494 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=84, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:45,494 INFO  L87              Difference]: Start difference. First operand 22 states and 33 transitions. Second operand  has 11 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 6 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:45,692 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,692 INFO  L93              Difference]: Finished difference Result 34 states and 59 transitions.
[2025-04-28 21:21:45,692 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:45,693 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 6 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8) Word has length 16
[2025-04-28 21:21:45,693 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,694 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:45,694 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:45,694 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 39 GetRequests, 27 SyntacticMatches, 1 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 13 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=40, Invalid=116, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:45,695 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 4 mSDsluCounter, 76 mSDsCounter, 0 mSdLazyCounter, 102 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 94 SdHoareTripleChecker+Invalid, 112 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 102 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,696 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 94 Invalid, 112 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 102 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,697 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:45,704 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 24.
[2025-04-28 21:21:45,705 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 10 states have (on average 1.3) internal successors, (13), 13 states have internal predecessors, (13), 6 states have call successors, (6), 3 states have call predecessors, (6), 7 states have return successors, (19), 7 states have call predecessors, (19), 6 states have call successors, (19)
[2025-04-28 21:21:45,706 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 38 transitions.
[2025-04-28 21:21:45,706 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 38 transitions. Word has length 16
[2025-04-28 21:21:45,706 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,706 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 38 transitions.
[2025-04-28 21:21:45,706 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 6 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:45,706 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 38 transitions.
[2025-04-28 21:21:45,707 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:45,708 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,708 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,712 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:45,911 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,912 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,912 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,913 INFO  L85        PathProgramCache]: Analyzing trace with hash -1709338129, now seen corresponding path program 1 times
[2025-04-28 21:21:45,913 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,913 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1669166727]
[2025-04-28 21:21:45,913 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,913 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,919 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:45,926 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,926 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,926 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,989 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:45,989 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,989 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1669166727]
[2025-04-28 21:21:45,989 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1669166727] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,990 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,990 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:45,990 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1921890793]
[2025-04-28 21:21:45,990 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,990 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:45,990 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,991 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:45,991 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:45,991 INFO  L87              Difference]: Start difference. First operand 24 states and 38 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 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,090 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,091 INFO  L93              Difference]: Finished difference Result 41 states and 68 transitions.
[2025-04-28 21:21:46,092 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:46,092 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 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,093 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,094 INFO  L225             Difference]: With dead ends: 41
[2025-04-28 21:21:46,096 INFO  L226             Difference]: Without dead ends: 41
[2025-04-28 21:21:46,097 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:21:46,098 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 5 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 45 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 44 SdHoareTripleChecker+Invalid, 48 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 45 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,098 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 44 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 45 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:46,099 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 41 states.
[2025-04-28 21:21:46,112 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 41 to 31.
[2025-04-28 21:21:46,115 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 13 states have (on average 1.4615384615384615) internal successors, (19), 18 states have internal predecessors, (19), 8 states have call successors, (8), 4 states have call predecessors, (8), 9 states have return successors, (24), 8 states have call predecessors, (24), 8 states have call successors, (24)
[2025-04-28 21:21:46,116 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 51 transitions.
[2025-04-28 21:21:46,117 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 51 transitions. Word has length 20
[2025-04-28 21:21:46,117 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,117 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 51 transitions.
[2025-04-28 21:21:46,118 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 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,118 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 51 transitions.
[2025-04-28 21:21:46,119 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:46,121 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,121 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,121 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:46,121 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,122 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,122 INFO  L85        PathProgramCache]: Analyzing trace with hash 196578566, now seen corresponding path program 2 times
[2025-04-28 21:21:46,122 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,122 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [740809746]
[2025-04-28 21:21:46,122 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,122 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,133 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:46,145 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:46,149 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:46,150 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,483 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:46,484 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,484 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [740809746]
[2025-04-28 21:21:46,484 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [740809746] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,484 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1552110024]
[2025-04-28 21:21:46,484 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,484 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,487 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,489 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:46,492 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,535 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:46,550 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:46,550 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:46,550 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,551 INFO  L256         TraceCheckSpWp]: Trace formula consists of 90 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,553 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,723 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:46,723 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:49,302 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:49,302 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1552110024] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:49,303 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:49,303 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 17
[2025-04-28 21:21:49,303 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1498379374]
[2025-04-28 21:21:49,303 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,303 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:49,304 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,304 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:49,304 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=49, Invalid=223, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:49,305 INFO  L87              Difference]: Start difference. First operand 31 states and 51 transitions. Second operand  has 17 states, 10 states have (on average 2.1) internal successors, (21), 16 states have internal predecessors, (21), 8 states have call successors, (9), 1 states have call predecessors, (9), 9 states have return successors, (11), 6 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:49,669 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,669 INFO  L93              Difference]: Finished difference Result 43 states and 75 transitions.
[2025-04-28 21:21:49,670 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:49,670 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 10 states have (on average 2.1) internal successors, (21), 16 states have internal predecessors, (21), 8 states have call successors, (9), 1 states have call predecessors, (9), 9 states have return successors, (11), 6 states have call predecessors, (11), 8 states have call successors, (11) Word has length 20
[2025-04-28 21:21:49,671 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,672 INFO  L225             Difference]: With dead ends: 43
[2025-04-28 21:21:49,672 INFO  L226             Difference]: Without dead ends: 43
[2025-04-28 21:21:49,673 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 53 GetRequests, 32 SyntacticMatches, 0 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 62 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=111, Invalid=395, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:49,673 INFO  L437           NwaCegarLoop]: 19 mSDtfsCounter, 10 mSDsluCounter, 100 mSDsCounter, 0 mSdLazyCounter, 134 mSolverCounterSat, 19 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 119 SdHoareTripleChecker+Invalid, 153 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 19 IncrementalHoareTripleChecker+Valid, 134 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,674 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 119 Invalid, 153 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [19 Valid, 134 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:49,676 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 43 states.
[2025-04-28 21:21:49,690 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 43 to 31.
[2025-04-28 21:21:49,691 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 13 states have (on average 1.4615384615384615) internal successors, (19), 18 states have internal predecessors, (19), 8 states have call successors, (8), 4 states have call predecessors, (8), 9 states have return successors, (24), 8 states have call predecessors, (24), 8 states have call successors, (24)
[2025-04-28 21:21:49,692 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 51 transitions.
[2025-04-28 21:21:49,692 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 51 transitions. Word has length 20
[2025-04-28 21:21:49,692 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,692 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 51 transitions.
[2025-04-28 21:21:49,692 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 10 states have (on average 2.1) internal successors, (21), 16 states have internal predecessors, (21), 8 states have call successors, (9), 1 states have call predecessors, (9), 9 states have return successors, (11), 6 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:49,693 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 51 transitions.
[2025-04-28 21:21:49,696 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:49,697 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,697 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,703 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:49,897 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,897 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,898 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,898 INFO  L85        PathProgramCache]: Analyzing trace with hash -1625775872, now seen corresponding path program 2 times
[2025-04-28 21:21:49,898 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,898 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2076739591]
[2025-04-28 21:21:49,898 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:49,898 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,903 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:49,913 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:49,913 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:49,913 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,178 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:50,178 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,178 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2076739591]
[2025-04-28 21:21:50,178 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2076739591] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,178 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [61622059]
[2025-04-28 21:21:50,178 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:50,179 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,181 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,183 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:50,186 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,239 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:50,258 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:50,258 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:50,258 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,260 INFO  L256         TraceCheckSpWp]: Trace formula consists of 98 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,261 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,508 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:50,510 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,165 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:53,165 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [61622059] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,165 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,165 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 16
[2025-04-28 21:21:53,165 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1147209820]
[2025-04-28 21:21:53,165 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,166 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:53,166 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,167 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:53,167 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=202, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:53,167 INFO  L87              Difference]: Start difference. First operand 31 states and 51 transitions. Second operand  has 16 states, 8 states have (on average 2.375) internal successors, (19), 15 states have internal predecessors, (19), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:53,512 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,512 INFO  L93              Difference]: Finished difference Result 61 states and 108 transitions.
[2025-04-28 21:21:53,513 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:53,514 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.375) internal successors, (19), 15 states have internal predecessors, (19), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11) Word has length 20
[2025-04-28 21:21:53,514 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,515 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:53,515 INFO  L226             Difference]: Without dead ends: 61
[2025-04-28 21:21:53,516 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 52 GetRequests, 32 SyntacticMatches, 1 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 34 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=89, Invalid=331, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:53,516 INFO  L437           NwaCegarLoop]: 20 mSDtfsCounter, 9 mSDsluCounter, 129 mSDsCounter, 0 mSdLazyCounter, 192 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 149 SdHoareTripleChecker+Invalid, 214 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 192 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,517 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 149 Invalid, 214 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 192 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:53,517 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 61 states.
[2025-04-28 21:21:53,528 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 61 to 31.
[2025-04-28 21:21:53,528 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 13 states have (on average 1.4615384615384615) internal successors, (19), 18 states have internal predecessors, (19), 8 states have call successors, (8), 4 states have call predecessors, (8), 9 states have return successors, (24), 9 states have call predecessors, (24), 8 states have call successors, (24)
[2025-04-28 21:21:53,529 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 51 transitions.
[2025-04-28 21:21:53,529 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 51 transitions. Word has length 20
[2025-04-28 21:21:53,529 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,530 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 51 transitions.
[2025-04-28 21:21:53,530 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.375) internal successors, (19), 15 states have internal predecessors, (19), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:53,530 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 51 transitions.
[2025-04-28 21:21:53,531 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:53,531 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,531 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,536 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:53,735 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,735 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,736 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,736 INFO  L85        PathProgramCache]: Analyzing trace with hash 2105626380, now seen corresponding path program 1 times
[2025-04-28 21:21:53,736 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,736 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1912217025]
[2025-04-28 21:21:53,736 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,736 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,740 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:53,744 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:53,745 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,745 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,777 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:53,777 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,777 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1912217025]
[2025-04-28 21:21:53,778 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1912217025] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,778 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,778 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:53,778 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [944825924]
[2025-04-28 21:21:53,778 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,778 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:53,778 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,780 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:53,780 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:53,780 INFO  L87              Difference]: Start difference. First operand 31 states and 51 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 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:53,861 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,861 INFO  L93              Difference]: Finished difference Result 52 states and 84 transitions.
[2025-04-28 21:21:53,861 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:53,862 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 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:53,862 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,863 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:53,863 INFO  L226             Difference]: Without dead ends: 47
[2025-04-28 21:21:53,863 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:21:53,864 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 4 mSDsluCounter, 24 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 47 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,864 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 47 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:53,864 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 47 states.
[2025-04-28 21:21:53,873 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 47 to 39.
[2025-04-28 21:21:53,873 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 39 states, 17 states have (on average 1.411764705882353) internal successors, (24), 22 states have internal predecessors, (24), 9 states have call successors, (9), 5 states have call predecessors, (9), 12 states have return successors, (30), 12 states have call predecessors, (30), 9 states have call successors, (30)
[2025-04-28 21:21:53,874 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 39 states to 39 states and 63 transitions.
[2025-04-28 21:21:53,874 INFO  L79                 Accepts]: Start accepts. Automaton has 39 states and 63 transitions. Word has length 20
[2025-04-28 21:21:53,874 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,874 INFO  L485      AbstractCegarLoop]: Abstraction has 39 states and 63 transitions.
[2025-04-28 21:21:53,874 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 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:53,874 INFO  L278                IsEmpty]: Start isEmpty. Operand 39 states and 63 transitions.
[2025-04-28 21:21:53,875 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:53,875 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,876 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,876 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:53,876 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,876 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,876 INFO  L85        PathProgramCache]: Analyzing trace with hash 1995036963, now seen corresponding path program 1 times
[2025-04-28 21:21:53,876 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,876 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1787333708]
[2025-04-28 21:21:53,877 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,877 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,880 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:53,888 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:53,888 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,888 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,060 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:54,060 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,060 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1787333708]
[2025-04-28 21:21:54,060 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1787333708] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,060 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [683040648]
[2025-04-28 21:21:54,060 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,060 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,063 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,065 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:54,068 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,130 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:54,143 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:54,143 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,143 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,144 INFO  L256         TraceCheckSpWp]: Trace formula consists of 94 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,145 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,220 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:54,220 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,662 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:54,663 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [683040648] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,663 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,663 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 13
[2025-04-28 21:21:54,663 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1032095475]
[2025-04-28 21:21:54,663 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,663 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:54,664 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,665 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:54,665 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=35, Invalid=121, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:54,665 INFO  L87              Difference]: Start difference. First operand 39 states and 63 transitions. Second operand  has 13 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 12 states have internal predecessors, (16), 7 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (11), 5 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:54,888 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,888 INFO  L93              Difference]: Finished difference Result 73 states and 123 transitions.
[2025-04-28 21:21:54,889 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:54,889 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 12 states have internal predecessors, (16), 7 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (11), 5 states have call predecessors, (11), 7 states have call successors, (11) Word has length 20
[2025-04-28 21:21:54,889 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,890 INFO  L225             Difference]: With dead ends: 73
[2025-04-28 21:21:54,890 INFO  L226             Difference]: Without dead ends: 73
[2025-04-28 21:21:54,891 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 53 GetRequests, 36 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 51 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=82, Invalid=260, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:54,891 INFO  L437           NwaCegarLoop]: 21 mSDtfsCounter, 9 mSDsluCounter, 105 mSDsCounter, 0 mSdLazyCounter, 149 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 126 SdHoareTripleChecker+Invalid, 160 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 149 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,892 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 126 Invalid, 160 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 149 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:54,892 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 73 states.
[2025-04-28 21:21:54,901 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 73 to 47.
[2025-04-28 21:21:54,902 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 47 states, 21 states have (on average 1.3333333333333333) internal successors, (28), 26 states have internal predecessors, (28), 9 states have call successors, (9), 5 states have call predecessors, (9), 16 states have return successors, (42), 16 states have call predecessors, (42), 9 states have call successors, (42)
[2025-04-28 21:21:54,903 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 47 states to 47 states and 79 transitions.
[2025-04-28 21:21:54,903 INFO  L79                 Accepts]: Start accepts. Automaton has 47 states and 79 transitions. Word has length 20
[2025-04-28 21:21:54,903 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,903 INFO  L485      AbstractCegarLoop]: Abstraction has 47 states and 79 transitions.
[2025-04-28 21:21:54,904 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 12 states have internal predecessors, (16), 7 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (11), 5 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:54,904 INFO  L278                IsEmpty]: Start isEmpty. Operand 47 states and 79 transitions.
[2025-04-28 21:21:54,905 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:54,905 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,905 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,910 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:55,105 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:55,106 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,106 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,106 INFO  L85        PathProgramCache]: Analyzing trace with hash -642257304, now seen corresponding path program 2 times
[2025-04-28 21:21:55,106 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,106 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1189054539]
[2025-04-28 21:21:55,106 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:55,106 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,110 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:21:55,117 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:55,117 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:55,117 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,149 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 11 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:55,149 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,149 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1189054539]
[2025-04-28 21:21:55,149 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1189054539] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,149 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,149 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:55,149 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [523751634]
[2025-04-28 21:21:55,149 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,150 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:55,150 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,150 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:55,150 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:55,150 INFO  L87              Difference]: Start difference. First operand 47 states and 79 transitions. Second operand  has 4 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 4 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:55,210 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,212 INFO  L93              Difference]: Finished difference Result 41 states and 54 transitions.
[2025-04-28 21:21:55,213 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:55,213 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 4 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:55,213 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,214 INFO  L225             Difference]: With dead ends: 41
[2025-04-28 21:21:55,214 INFO  L226             Difference]: Without dead ends: 35
[2025-04-28 21:21:55,214 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:21:55,215 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 4 mSDsluCounter, 20 mSDsCounter, 0 mSdLazyCounter, 38 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 44 SdHoareTripleChecker+Invalid, 40 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 38 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,215 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 44 Invalid, 40 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 38 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:55,215 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 35 states.
[2025-04-28 21:21:55,221 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 35 to 29.
[2025-04-28 21:21:55,223 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 12 states have (on average 1.5) internal successors, (18), 16 states have internal predecessors, (18), 9 states have call successors, (9), 5 states have call predecessors, (9), 7 states have return successors, (11), 8 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:55,224 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 38 transitions.
[2025-04-28 21:21:55,224 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 38 transitions. Word has length 24
[2025-04-28 21:21:55,224 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,224 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 38 transitions.
[2025-04-28 21:21:55,224 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 4 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:55,225 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 38 transitions.
[2025-04-28 21:21:55,227 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:55,227 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,227 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,227 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:55,227 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,228 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,228 INFO  L85        PathProgramCache]: Analyzing trace with hash 1777033896, now seen corresponding path program 3 times
[2025-04-28 21:21:55,228 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,228 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1556265644]
[2025-04-28 21:21:55,231 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:55,231 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,237 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:55,252 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 22 of 24 statements.
[2025-04-28 21:21:55,252 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:55,252 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,615 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 13 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:55,616 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,617 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1556265644]
[2025-04-28 21:21:55,617 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1556265644] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,617 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [261334383]
[2025-04-28 21:21:55,617 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:55,617 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,620 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,622 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:55,625 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,688 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:55,708 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 22 of 24 statements.
[2025-04-28 21:21:55,708 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:55,708 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,709 INFO  L256         TraceCheckSpWp]: Trace formula consists of 114 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,711 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,924 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 2 proven. 11 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:55,924 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,760 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 6 proven. 7 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:59,765 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [261334383] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,765 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,765 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 21
[2025-04-28 21:21:59,765 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1603867815]
[2025-04-28 21:21:59,765 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,766 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:59,766 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,766 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:59,766 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=61, Invalid=359, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:59,767 INFO  L87              Difference]: Start difference. First operand 29 states and 38 transitions. Second operand  has 21 states, 12 states have (on average 2.0) internal successors, (24), 20 states have internal predecessors, (24), 10 states have call successors, (11), 1 states have call predecessors, (11), 11 states have return successors, (14), 9 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:22:00,333 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,334 INFO  L93              Difference]: Finished difference Result 45 states and 63 transitions.
[2025-04-28 21:22:00,334 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:22:00,334 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 12 states have (on average 2.0) internal successors, (24), 20 states have internal predecessors, (24), 10 states have call successors, (11), 1 states have call predecessors, (11), 11 states have return successors, (14), 9 states have call predecessors, (14), 10 states have call successors, (14) Word has length 24
[2025-04-28 21:22:00,335 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,335 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:22:00,335 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:22:00,335 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 68 GetRequests, 38 SyntacticMatches, 0 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 85 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=182, Invalid=810, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:22:00,336 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 26 mSDsluCounter, 95 mSDsCounter, 0 mSdLazyCounter, 163 mSolverCounterSat, 50 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 30 SdHoareTripleChecker+Valid, 112 SdHoareTripleChecker+Invalid, 213 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 50 IncrementalHoareTripleChecker+Valid, 163 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,336 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [30 Valid, 112 Invalid, 213 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [50 Valid, 163 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:00,337 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:22:00,337 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:22:00,337 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:22:00,337 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:22:00,337 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 24
[2025-04-28 21:22:00,337 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,337 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:22:00,337 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 12 states have (on average 2.0) internal successors, (24), 20 states have internal predecessors, (24), 10 states have call successors, (11), 1 states have call predecessors, (11), 11 states have return successors, (14), 9 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:22:00,337 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:22:00,338 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:22:00,340 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:22:00,344 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:22:00,542 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,545 INFO  L422         BasicCegarLoop]: Path program histogram: [3, 2, 2, 1, 1, 1]
[2025-04-28 21:22:00,547 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:22:00,550 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:22:00 BoogieIcfgContainer
[2025-04-28 21:22:00,551 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:22:00,551 INFO  L158              Benchmark]: Toolchain (without parser) took 19815.96ms. Allocated memory was 234.9MB in the beginning and 201.3MB in the end (delta: -33.6MB). Free memory was 164.6MB in the beginning and 102.9MB in the end (delta: 61.7MB). Peak memory consumption was 26.8MB. Max. memory is 33.6GB.
[2025-04-28 21:22:00,552 INFO  L158              Benchmark]: SmtParser took 0.39ms. Allocated memory is still 234.9MB. Free memory is still 171.3MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:00,552 INFO  L158              Benchmark]: ChcToBoogie took 31.21ms. Allocated memory is still 234.9MB. Free memory was 164.6MB in the beginning and 163.5MB in the end (delta: 1.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:00,552 INFO  L158              Benchmark]: Boogie Preprocessor took 78.06ms. Allocated memory is still 234.9MB. Free memory was 163.5MB in the beginning and 161.3MB in the end (delta: 2.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:00,552 INFO  L158              Benchmark]: RCFGBuilder took 247.51ms. Allocated memory is still 234.9MB. Free memory was 161.3MB in the beginning and 152.9MB in the end (delta: 8.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:00,553 INFO  L158              Benchmark]: TraceAbstraction took 19451.52ms. Allocated memory was 234.9MB in the beginning and 201.3MB in the end (delta: -33.6MB). Free memory was 152.3MB in the beginning and 102.9MB in the end (delta: 49.4MB). Peak memory consumption was 10.1MB. Max. memory is 33.6GB.
[2025-04-28 21:22:00,556 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.39ms. Allocated memory is still 234.9MB. Free memory is still 171.3MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 31.21ms. Allocated memory is still 234.9MB. Free memory was 164.6MB in the beginning and 163.5MB in the end (delta: 1.1MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 78.06ms. Allocated memory is still 234.9MB. Free memory was 163.5MB in the beginning and 161.3MB in the end (delta: 2.2MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 247.51ms. Allocated memory is still 234.9MB. Free memory was 161.3MB in the beginning and 152.9MB in the end (delta: 8.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * TraceAbstraction took 19451.52ms. Allocated memory was 234.9MB in the beginning and 201.3MB in the end (delta: -33.6MB). Free memory was 152.3MB in the beginning and 102.9MB in the end (delta: 49.4MB). Peak memory consumption was 10.1MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 4 procedures, 18 locations, 29 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 19.4s, OverallIterations: 10, TraceHistogramMax: 4, PathProgramHistogramMax: 3, EmptinessCheckTime: 0.0s, AutomataDifference: 2.3s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 130 SdHoareTripleChecker+Valid, 1.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 76 mSDsluCounter, 867 SdHoareTripleChecker+Invalid, 1.1s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 665 mSDsCounter, 130 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 962 IncrementalHoareTripleChecker+Invalid, 1092 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 130 mSolverCounterUnsat, 202 mSDtfsCounter, 962 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 325 GetRequests, 205 SyntacticMatches, 2 SemanticMatches, 118 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 252 ImplicationChecksByTransitivity, 2.2s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=47occurred in iteration=8, InterpolantAutomatonStates: 83, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 10 MinimizatonAttempts, 106 StatesRemovedByMinimization, 8 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.3s SatisfiabilityAnalysisTime, 14.8s InterpolantComputationTime, 308 NumberOfCodeBlocks, 304 NumberOfCodeBlocksAsserted, 25 NumberOfCheckSat, 402 ConstructedInterpolants, 0 QuantifiedInterpolants, 1824 SizeOfPredicates, 60 NumberOfNonLiveVariables, 536 ConjunctsInSsa, 117 ConjunctsInUnsatCore, 22 InterpolantComputations, 4 PerfectInterpolantSequences, 108/199 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:22:00,574 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
sat
