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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:30,046 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:30,128 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fd6cbfb7-9793-4743-8351-de66e574f9fa/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:30,136 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:30,138 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:30,161 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:30,162 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:30,162 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:30,163 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:30,163 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:30,163 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:30,163 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:30,163 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:30,164 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:30,164 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:30,164 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:30,164 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:30,164 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:30,164 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:30,165 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:30,165 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:30,165 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:30,165 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:30,165 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:30,165 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:30,166 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:30,166 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:30,559 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:30,571 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:30,574 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:30,576 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:30,577 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:30,578 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fd6cbfb7-9793-4743-8351-de66e574f9fa/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-001.smt2
[2025-04-28 21:21:30,581 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:30,584 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:30,942 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fd6cbfb7-9793-4743-8351-de66e574f9fa/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-001.smt2
[2025-04-28 21:21:30,949 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:30,950 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:30,952 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:30,952 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:30,952 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:30,955 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,990 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30 Unit
[2025-04-28 21:21:30,990 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:30,992 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:30,992 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:30,992 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:31,010 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,010 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,035 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,036 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,039 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,040 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,043 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,044 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,045 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,061 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:31,062 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:31,062 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:31,062 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:31,063 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,066 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:31,081 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,100 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:31,106 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:31,124 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:31,124 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:31,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:31,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry.split given in one single declaration
[2025-04-28 21:21:31,125 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry.split
[2025-04-28 21:21:31,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry.split
[2025-04-28 21:21:31,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:31,125 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:31,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:31,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure applyHanoi given in one single declaration
[2025-04-28 21:21:31,125 INFO  L130     BoogieDeclarations]: Found specification of procedure applyHanoi
[2025-04-28 21:21:31,125 INFO  L138     BoogieDeclarations]: Found implementation of procedure applyHanoi
[2025-04-28 21:21:31,125 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure applyHanoi.ATtailrecurse._crit_edge given in one single declaration
[2025-04-28 21:21:31,126 INFO  L130     BoogieDeclarations]: Found specification of procedure applyHanoi.ATtailrecurse._crit_edge
[2025-04-28 21:21:31,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure applyHanoi.ATtailrecurse._crit_edge
[2025-04-28 21:21:31,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure applyHanoi.ATtailrecurse given in one single declaration
[2025-04-28 21:21:31,126 INFO  L130     BoogieDeclarations]: Found specification of procedure applyHanoi.ATtailrecurse
[2025-04-28 21:21:31,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure applyHanoi.ATtailrecurse
[2025-04-28 21:21:31,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure applyHanoi.AT_1 given in one single declaration
[2025-04-28 21:21:31,126 INFO  L130     BoogieDeclarations]: Found specification of procedure applyHanoi.AT_1
[2025-04-28 21:21:31,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure applyHanoi.AT_1
[2025-04-28 21:21:31,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure hanoi given in one single declaration
[2025-04-28 21:21:31,126 INFO  L130     BoogieDeclarations]: Found specification of procedure hanoi
[2025-04-28 21:21:31,126 INFO  L138     BoogieDeclarations]: Found implementation of procedure hanoi
[2025-04-28 21:21:31,126 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure hanoi.ATUnifiedReturnBlock.split given in one single declaration
[2025-04-28 21:21:31,127 INFO  L130     BoogieDeclarations]: Found specification of procedure hanoi.ATUnifiedReturnBlock.split
[2025-04-28 21:21:31,127 INFO  L138     BoogieDeclarations]: Found implementation of procedure hanoi.ATUnifiedReturnBlock.split
[2025-04-28 21:21:31,127 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure hanoi.AT_1 given in one single declaration
[2025-04-28 21:21:31,127 INFO  L130     BoogieDeclarations]: Found specification of procedure hanoi.AT_1
[2025-04-28 21:21:31,127 INFO  L138     BoogieDeclarations]: Found implementation of procedure hanoi.AT_1
[2025-04-28 21:21:31,127 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:31,127 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:31,127 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:31,235 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:31,237 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:31,460 INFO  L?                        ?]: Removed 51 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:31,460 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:31,475 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:31,476 INFO  L312             CfgBuilder]: Removed 4 assume(true) statements.
[2025-04-28 21:21:31,476 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:31 BoogieIcfgContainer
[2025-04-28 21:21:31,477 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:31,486 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:31,486 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:31,490 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:31,490 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:30" (1/3) ...
[2025-04-28 21:21:31,492 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@66bd4b4e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:31, skipping insertion in model container
[2025-04-28 21:21:31,492 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (2/3) ...
[2025-04-28 21:21:31,492 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@66bd4b4e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:31, skipping insertion in model container
[2025-04-28 21:21:31,493 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:31" (3/3) ...
[2025-04-28 21:21:31,494 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:31,513 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:31,517 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 11 procedures, 45 locations, 72 edges, 11 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:31,578 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:31,602 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;@11c7a5fd, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:31,602 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:31,610 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 45 states, 18 states have (on average 1.5) internal successors, (27), 23 states have internal predecessors, (27), 15 states have call successors, (15), 10 states have call predecessors, (15), 10 states have return successors, (15), 13 states have call predecessors, (15), 15 states have call successors, (15)
[2025-04-28 21:21:31,623 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:31,623 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,624 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,624 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,633 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,634 INFO  L85        PathProgramCache]: Analyzing trace with hash 539096567, now seen corresponding path program 1 times
[2025-04-28 21:21:31,643 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,644 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1522769916]
[2025-04-28 21:21:31,645 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,645 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,696 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:31,717 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:31,718 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,718 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,859 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:31,859 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,859 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1522769916]
[2025-04-28 21:21:31,860 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1522769916] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:31,860 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:31,863 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:31,865 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1408347910]
[2025-04-28 21:21:31,866 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,870 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:31,871 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,906 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:31,907 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:31,909 INFO  L87              Difference]: Start difference. First operand  has 45 states, 18 states have (on average 1.5) internal successors, (27), 23 states have internal predecessors, (27), 15 states have call successors, (15), 10 states have call predecessors, (15), 10 states have return successors, (15), 13 states have call predecessors, (15), 15 states have call successors, (15) Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 1 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:31,961 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,961 INFO  L93              Difference]: Finished difference Result 45 states and 57 transitions.
[2025-04-28 21:21:31,963 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:31,965 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 1 states have call predecessors, (5), 3 states have call successors, (5) Word has length 19
[2025-04-28 21:21:31,965 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,974 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:21:31,974 INFO  L226             Difference]: Without dead ends: 45
[2025-04-28 21:21:31,976 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:31,979 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 1 mSDsluCounter, 97 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 151 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,980 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 151 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:31,996 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 45 states.
[2025-04-28 21:21:32,047 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 45 to 45.
[2025-04-28 21:21:32,049 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 45 states, 18 states have (on average 1.4444444444444444) internal successors, (26), 23 states have internal predecessors, (26), 15 states have call successors, (15), 10 states have call predecessors, (15), 11 states have return successors, (16), 13 states have call predecessors, (16), 15 states have call successors, (16)
[2025-04-28 21:21:32,053 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 45 states to 45 states and 57 transitions.
[2025-04-28 21:21:32,055 INFO  L79                 Accepts]: Start accepts. Automaton has 45 states and 57 transitions. Word has length 19
[2025-04-28 21:21:32,056 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,056 INFO  L485      AbstractCegarLoop]: Abstraction has 45 states and 57 transitions.
[2025-04-28 21:21:32,056 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 1 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:32,056 INFO  L278                IsEmpty]: Start isEmpty. Operand 45 states and 57 transitions.
[2025-04-28 21:21:32,058 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:32,058 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,058 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,058 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:32,059 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,059 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,060 INFO  L85        PathProgramCache]: Analyzing trace with hash 1363583983, now seen corresponding path program 1 times
[2025-04-28 21:21:32,061 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,061 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [69291403]
[2025-04-28 21:21:32,062 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,062 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,075 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:32,098 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:32,098 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,098 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,208 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:32,208 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,209 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [69291403]
[2025-04-28 21:21:32,210 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [69291403] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,210 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:32,210 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:32,210 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1371523759]
[2025-04-28 21:21:32,210 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,211 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:32,212 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,212 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:32,213 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:32,244 INFO  L87              Difference]: Start difference. First operand 45 states and 57 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 1 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:32,275 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,275 INFO  L93              Difference]: Finished difference Result 49 states and 61 transitions.
[2025-04-28 21:21:32,276 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:32,277 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 1 states have call predecessors, (5), 3 states have call successors, (5) Word has length 19
[2025-04-28 21:21:32,277 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,278 INFO  L225             Difference]: With dead ends: 49
[2025-04-28 21:21:32,278 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:21:32,278 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:32,279 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 1 mSDsluCounter, 100 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 156 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,280 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 156 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:32,284 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:21:32,290 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 45.
[2025-04-28 21:21:32,291 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 45 states, 18 states have (on average 1.4444444444444444) internal successors, (26), 22 states have internal predecessors, (26), 15 states have call successors, (15), 10 states have call predecessors, (15), 11 states have return successors, (16), 13 states have call predecessors, (16), 15 states have call successors, (16)
[2025-04-28 21:21:32,292 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 45 states to 45 states and 57 transitions.
[2025-04-28 21:21:32,292 INFO  L79                 Accepts]: Start accepts. Automaton has 45 states and 57 transitions. Word has length 19
[2025-04-28 21:21:32,292 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,292 INFO  L485      AbstractCegarLoop]: Abstraction has 45 states and 57 transitions.
[2025-04-28 21:21:32,293 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 1 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:32,293 INFO  L278                IsEmpty]: Start isEmpty. Operand 45 states and 57 transitions.
[2025-04-28 21:21:32,294 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:32,294 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,294 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,294 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:32,295 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,295 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,295 INFO  L85        PathProgramCache]: Analyzing trace with hash 841970921, now seen corresponding path program 1 times
[2025-04-28 21:21:32,295 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,296 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1170599770]
[2025-04-28 21:21:32,296 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,296 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,308 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:32,322 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:32,326 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,327 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,452 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:32,452 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,452 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1170599770]
[2025-04-28 21:21:32,452 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1170599770] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,452 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:32,453 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:32,453 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [334303372]
[2025-04-28 21:21:32,453 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,453 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:32,454 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,454 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:32,455 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:32,456 INFO  L87              Difference]: Start difference. First operand 45 states and 57 transitions. Second operand  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:32,479 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,479 INFO  L93              Difference]: Finished difference Result 47 states and 58 transitions.
[2025-04-28 21:21:32,480 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:32,480 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:32,480 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,481 INFO  L225             Difference]: With dead ends: 47
[2025-04-28 21:21:32,482 INFO  L226             Difference]: Without dead ends: 45
[2025-04-28 21:21:32,482 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:32,483 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 1 mSDsluCounter, 100 mSDsCounter, 0 mSdLazyCounter, 4 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 155 SdHoareTripleChecker+Invalid, 5 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 4 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,483 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 155 Invalid, 5 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 4 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:32,484 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 45 states.
[2025-04-28 21:21:32,491 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 45 to 45.
[2025-04-28 21:21:32,491 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 45 states, 18 states have (on average 1.3333333333333333) internal successors, (24), 22 states have internal predecessors, (24), 15 states have call successors, (15), 10 states have call predecessors, (15), 11 states have return successors, (16), 13 states have call predecessors, (16), 15 states have call successors, (16)
[2025-04-28 21:21:32,492 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 45 states to 45 states and 55 transitions.
[2025-04-28 21:21:32,492 INFO  L79                 Accepts]: Start accepts. Automaton has 45 states and 55 transitions. Word has length 30
[2025-04-28 21:21:32,493 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,493 INFO  L485      AbstractCegarLoop]: Abstraction has 45 states and 55 transitions.
[2025-04-28 21:21:32,493 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:32,493 INFO  L278                IsEmpty]: Start isEmpty. Operand 45 states and 55 transitions.
[2025-04-28 21:21:32,494 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:32,494 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,495 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,495 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:32,495 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,495 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,496 INFO  L85        PathProgramCache]: Analyzing trace with hash -992188703, now seen corresponding path program 1 times
[2025-04-28 21:21:32,496 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,496 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [179831050]
[2025-04-28 21:21:32,496 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,496 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,516 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:32,535 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:32,535 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,536 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,653 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:32,653 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,653 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [179831050]
[2025-04-28 21:21:32,654 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [179831050] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,654 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:32,654 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:32,654 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1436820222]
[2025-04-28 21:21:32,654 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,654 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:32,654 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,655 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:32,655 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:32,656 INFO  L87              Difference]: Start difference. First operand 45 states and 55 transitions. Second operand  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:32,728 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,729 INFO  L93              Difference]: Finished difference Result 47 states and 58 transitions.
[2025-04-28 21:21:32,729 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:32,729 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:32,730 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,731 INFO  L225             Difference]: With dead ends: 47
[2025-04-28 21:21:32,731 INFO  L226             Difference]: Without dead ends: 47
[2025-04-28 21:21:32,731 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:32,732 INFO  L437           NwaCegarLoop]: 51 mSDtfsCounter, 1 mSDsluCounter, 90 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 141 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,737 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 141 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:32,737 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 47 states.
[2025-04-28 21:21:32,743 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 47 to 47.
[2025-04-28 21:21:32,743 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 47 states, 19 states have (on average 1.3157894736842106) internal successors, (25), 24 states have internal predecessors, (25), 15 states have call successors, (15), 10 states have call predecessors, (15), 12 states have return successors, (18), 13 states have call predecessors, (18), 15 states have call successors, (18)
[2025-04-28 21:21:32,745 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 47 states to 47 states and 58 transitions.
[2025-04-28 21:21:32,749 INFO  L79                 Accepts]: Start accepts. Automaton has 47 states and 58 transitions. Word has length 30
[2025-04-28 21:21:32,749 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,749 INFO  L485      AbstractCegarLoop]: Abstraction has 47 states and 58 transitions.
[2025-04-28 21:21:32,749 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:32,749 INFO  L278                IsEmpty]: Start isEmpty. Operand 47 states and 58 transitions.
[2025-04-28 21:21:32,750 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:32,751 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,751 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,751 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:32,751 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,752 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,754 INFO  L85        PathProgramCache]: Analyzing trace with hash 1900649437, now seen corresponding path program 1 times
[2025-04-28 21:21:32,754 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,754 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1152751532]
[2025-04-28 21:21:32,754 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,754 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,773 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:32,786 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:32,787 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,788 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,875 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:32,875 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,875 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1152751532]
[2025-04-28 21:21:32,875 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1152751532] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,876 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:32,876 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:32,876 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2098945535]
[2025-04-28 21:21:32,876 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,876 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:32,876 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,877 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:32,877 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:32,877 INFO  L87              Difference]: Start difference. First operand 47 states and 58 transitions. Second operand  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:32,921 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,921 INFO  L93              Difference]: Finished difference Result 51 states and 64 transitions.
[2025-04-28 21:21:32,923 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:32,923 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:32,923 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,924 INFO  L225             Difference]: With dead ends: 51
[2025-04-28 21:21:32,926 INFO  L226             Difference]: Without dead ends: 51
[2025-04-28 21:21:32,927 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:32,928 INFO  L437           NwaCegarLoop]: 51 mSDtfsCounter, 1 mSDsluCounter, 90 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 141 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,929 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 141 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:32,930 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 51 states.
[2025-04-28 21:21:32,938 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 51 to 47.
[2025-04-28 21:21:32,940 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 47 states, 19 states have (on average 1.3157894736842106) internal successors, (25), 23 states have internal predecessors, (25), 15 states have call successors, (15), 10 states have call predecessors, (15), 12 states have return successors, (18), 13 states have call predecessors, (18), 15 states have call successors, (18)
[2025-04-28 21:21:32,941 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 47 states to 47 states and 58 transitions.
[2025-04-28 21:21:32,943 INFO  L79                 Accepts]: Start accepts. Automaton has 47 states and 58 transitions. Word has length 30
[2025-04-28 21:21:32,943 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,943 INFO  L485      AbstractCegarLoop]: Abstraction has 47 states and 58 transitions.
[2025-04-28 21:21:32,943 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:32,944 INFO  L278                IsEmpty]: Start isEmpty. Operand 47 states and 58 transitions.
[2025-04-28 21:21:32,945 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:32,946 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,946 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,946 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:32,947 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,947 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,948 INFO  L85        PathProgramCache]: Analyzing trace with hash -150581590, now seen corresponding path program 1 times
[2025-04-28 21:21:32,948 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,948 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1662438126]
[2025-04-28 21:21:32,948 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,948 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,963 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:32,981 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:32,982 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,982 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,180 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:33,180 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,180 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1662438126]
[2025-04-28 21:21:33,180 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1662438126] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,180 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,180 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:33,180 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1310726914]
[2025-04-28 21:21:33,181 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,181 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:33,181 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,181 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:33,182 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:33,182 INFO  L87              Difference]: Start difference. First operand 47 states and 58 transitions. Second operand  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 4 states have call successors, (10), 1 states have call predecessors, (10), 4 states have return successors, (10), 5 states have call predecessors, (10), 4 states have call successors, (10)
[2025-04-28 21:21:33,235 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,236 INFO  L93              Difference]: Finished difference Result 51 states and 63 transitions.
[2025-04-28 21:21:33,238 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:33,239 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 4 states have call successors, (10), 1 states have call predecessors, (10), 4 states have return successors, (10), 5 states have call predecessors, (10), 4 states have call successors, (10) Word has length 37
[2025-04-28 21:21:33,239 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,240 INFO  L225             Difference]: With dead ends: 51
[2025-04-28 21:21:33,240 INFO  L226             Difference]: Without dead ends: 51
[2025-04-28 21:21:33,243 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:33,244 INFO  L437           NwaCegarLoop]: 53 mSDtfsCounter, 1 mSDsluCounter, 148 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 201 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,245 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 201 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:33,245 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 51 states.
[2025-04-28 21:21:33,253 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 51 to 49.
[2025-04-28 21:21:33,254 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 49 states, 20 states have (on average 1.3) internal successors, (26), 24 states have internal predecessors, (26), 15 states have call successors, (15), 10 states have call predecessors, (15), 13 states have return successors, (19), 15 states have call predecessors, (19), 15 states have call successors, (19)
[2025-04-28 21:21:33,255 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 49 states to 49 states and 60 transitions.
[2025-04-28 21:21:33,258 INFO  L79                 Accepts]: Start accepts. Automaton has 49 states and 60 transitions. Word has length 37
[2025-04-28 21:21:33,258 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,259 INFO  L485      AbstractCegarLoop]: Abstraction has 49 states and 60 transitions.
[2025-04-28 21:21:33,259 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 4 states have call successors, (10), 1 states have call predecessors, (10), 4 states have return successors, (10), 5 states have call predecessors, (10), 4 states have call successors, (10)
[2025-04-28 21:21:33,259 INFO  L278                IsEmpty]: Start isEmpty. Operand 49 states and 60 transitions.
[2025-04-28 21:21:33,260 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:21:33,260 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,260 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,261 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:33,261 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,264 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,264 INFO  L85        PathProgramCache]: Analyzing trace with hash -506658214, now seen corresponding path program 1 times
[2025-04-28 21:21:33,265 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,265 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1057518028]
[2025-04-28 21:21:33,265 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,265 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,291 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:33,305 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:33,305 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,305 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,388 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:33,389 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,389 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1057518028]
[2025-04-28 21:21:33,389 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1057518028] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,389 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,389 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:33,389 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1540691038]
[2025-04-28 21:21:33,389 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,390 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:33,390 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,390 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:33,390 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:33,391 INFO  L87              Difference]: Start difference. First operand 49 states and 60 transitions. Second operand  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:33,422 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,423 INFO  L93              Difference]: Finished difference Result 51 states and 62 transitions.
[2025-04-28 21:21:33,423 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:33,423 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12) Word has length 45
[2025-04-28 21:21:33,424 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,425 INFO  L225             Difference]: With dead ends: 51
[2025-04-28 21:21:33,425 INFO  L226             Difference]: Without dead ends: 51
[2025-04-28 21:21:33,425 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:33,426 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 1 mSDsluCounter, 96 mSDsCounter, 0 mSdLazyCounter, 9 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 150 SdHoareTripleChecker+Invalid, 10 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 9 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,426 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 150 Invalid, 10 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 9 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:33,430 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 51 states.
[2025-04-28 21:21:33,438 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 51 to 51.
[2025-04-28 21:21:33,439 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 51 states, 21 states have (on average 1.2857142857142858) internal successors, (27), 26 states have internal predecessors, (27), 15 states have call successors, (15), 10 states have call predecessors, (15), 14 states have return successors, (20), 15 states have call predecessors, (20), 15 states have call successors, (20)
[2025-04-28 21:21:33,440 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 51 states to 51 states and 62 transitions.
[2025-04-28 21:21:33,440 INFO  L79                 Accepts]: Start accepts. Automaton has 51 states and 62 transitions. Word has length 45
[2025-04-28 21:21:33,440 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,440 INFO  L485      AbstractCegarLoop]: Abstraction has 51 states and 62 transitions.
[2025-04-28 21:21:33,442 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:33,442 INFO  L278                IsEmpty]: Start isEmpty. Operand 51 states and 62 transitions.
[2025-04-28 21:21:33,443 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:21:33,444 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,444 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,444 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:33,444 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,445 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,445 INFO  L85        PathProgramCache]: Analyzing trace with hash 2053069142, now seen corresponding path program 1 times
[2025-04-28 21:21:33,445 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,445 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1721346038]
[2025-04-28 21:21:33,445 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,445 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,464 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:33,474 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:33,474 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,475 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,535 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:33,535 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,535 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1721346038]
[2025-04-28 21:21:33,535 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1721346038] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,535 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,537 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:33,537 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1409952075]
[2025-04-28 21:21:33,538 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,538 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:33,538 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,539 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:33,539 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:33,539 INFO  L87              Difference]: Start difference. First operand 51 states and 62 transitions. Second operand  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:33,569 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,570 INFO  L93              Difference]: Finished difference Result 55 states and 66 transitions.
[2025-04-28 21:21:33,573 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:33,574 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12) Word has length 45
[2025-04-28 21:21:33,574 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,575 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:33,575 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:33,575 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:33,576 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 1 mSDsluCounter, 97 mSDsCounter, 0 mSdLazyCounter, 8 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 151 SdHoareTripleChecker+Invalid, 9 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 8 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,576 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 151 Invalid, 9 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 8 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:33,577 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:33,583 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 51.
[2025-04-28 21:21:33,586 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 51 states, 21 states have (on average 1.2857142857142858) internal successors, (27), 25 states have internal predecessors, (27), 15 states have call successors, (15), 10 states have call predecessors, (15), 14 states have return successors, (20), 15 states have call predecessors, (20), 15 states have call successors, (20)
[2025-04-28 21:21:33,588 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 51 states to 51 states and 62 transitions.
[2025-04-28 21:21:33,588 INFO  L79                 Accepts]: Start accepts. Automaton has 51 states and 62 transitions. Word has length 45
[2025-04-28 21:21:33,589 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,589 INFO  L485      AbstractCegarLoop]: Abstraction has 51 states and 62 transitions.
[2025-04-28 21:21:33,589 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:33,589 INFO  L278                IsEmpty]: Start isEmpty. Operand 51 states and 62 transitions.
[2025-04-28 21:21:33,594 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:33,594 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,594 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,594 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:33,595 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,595 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,595 INFO  L85        PathProgramCache]: Analyzing trace with hash 579661463, now seen corresponding path program 1 times
[2025-04-28 21:21:33,595 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,595 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [946981742]
[2025-04-28 21:21:33,595 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,596 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,620 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:33,643 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:33,644 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,644 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,847 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:34,847 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,847 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [946981742]
[2025-04-28 21:21:34,848 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [946981742] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,848 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [250061511]
[2025-04-28 21:21:34,848 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,848 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,851 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,854 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:34,859 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,950 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:35,005 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:35,005 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,005 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,010 INFO  L256         TraceCheckSpWp]: Trace formula consists of 226 conjuncts, 57 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:35,023 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:35,081 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 6 treesize of output 5
[2025-04-28 21:21:35,528 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:35,528 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,463 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 14 treesize of output 12
[2025-04-28 21:21:38,806 INFO  L325             Elim1Store]: treesize reduction 12, result has 70.0 percent of original size
[2025-04-28 21:21:38,806 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 4 case distinctions, treesize of input 37 treesize of output 49
[2025-04-28 21:21:38,886 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:38,887 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 2 case distinctions, treesize of input 11 treesize of output 8
[2025-04-28 21:21:39,124 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:39,124 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [250061511] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:39,124 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:39,124 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 15, 15] total 23
[2025-04-28 21:21:39,125 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1335866506]
[2025-04-28 21:21:39,125 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,125 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:39,126 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,126 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:39,127 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=56, Invalid=450, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:39,127 INFO  L87              Difference]: Start difference. First operand 51 states and 62 transitions. Second operand  has 23 states, 12 states have (on average 2.3333333333333335) internal successors, (28), 18 states have internal predecessors, (28), 15 states have call successors, (20), 2 states have call predecessors, (20), 12 states have return successors, (23), 16 states have call predecessors, (23), 15 states have call successors, (23)
[2025-04-28 21:21:39,646 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,647 INFO  L93              Difference]: Finished difference Result 70 states and 90 transitions.
[2025-04-28 21:21:39,647 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:21:39,647 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 12 states have (on average 2.3333333333333335) internal successors, (28), 18 states have internal predecessors, (28), 15 states have call successors, (20), 2 states have call predecessors, (20), 12 states have return successors, (23), 16 states have call predecessors, (23), 15 states have call successors, (23) Word has length 52
[2025-04-28 21:21:39,647 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,648 INFO  L225             Difference]: With dead ends: 70
[2025-04-28 21:21:39,648 INFO  L226             Difference]: Without dead ends: 70
[2025-04-28 21:21:39,649 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 122 GetRequests, 96 SyntacticMatches, 1 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 66 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=89, Invalid=613, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:39,650 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 12 mSDsluCounter, 843 mSDsCounter, 0 mSdLazyCounter, 263 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 897 SdHoareTripleChecker+Invalid, 278 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 263 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,650 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 897 Invalid, 278 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 263 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:39,651 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-04-28 21:21:39,660 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 63.
[2025-04-28 21:21:39,660 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 63 states, 26 states have (on average 1.2307692307692308) internal successors, (32), 30 states have internal predecessors, (32), 17 states have call successors, (17), 10 states have call predecessors, (17), 19 states have return successors, (33), 22 states have call predecessors, (33), 17 states have call successors, (33)
[2025-04-28 21:21:39,661 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 63 states to 63 states and 82 transitions.
[2025-04-28 21:21:39,661 INFO  L79                 Accepts]: Start accepts. Automaton has 63 states and 82 transitions. Word has length 52
[2025-04-28 21:21:39,661 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,661 INFO  L485      AbstractCegarLoop]: Abstraction has 63 states and 82 transitions.
[2025-04-28 21:21:39,662 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 12 states have (on average 2.3333333333333335) internal successors, (28), 18 states have internal predecessors, (28), 15 states have call successors, (20), 2 states have call predecessors, (20), 12 states have return successors, (23), 16 states have call predecessors, (23), 15 states have call successors, (23)
[2025-04-28 21:21:39,662 INFO  L278                IsEmpty]: Start isEmpty. Operand 63 states and 82 transitions.
[2025-04-28 21:21:39,663 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 64
[2025-04-28 21:21:39,663 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,663 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,669 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:39,867 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:21:39,868 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,868 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,868 INFO  L85        PathProgramCache]: Analyzing trace with hash -1141765875, now seen corresponding path program 2 times
[2025-04-28 21:21:39,868 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,868 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [286761058]
[2025-04-28 21:21:39,869 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:39,869 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,882 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 63 statements into 2 equivalence classes.
[2025-04-28 21:21:39,893 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 63 of 63 statements.
[2025-04-28 21:21:39,893 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:39,893 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,462 INFO  L134       CoverageAnalysis]: Checked inductivity of 26 backedges. 3 proven. 12 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:40,462 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,462 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [286761058]
[2025-04-28 21:21:40,463 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [286761058] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,463 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [899607037]
[2025-04-28 21:21:40,463 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:40,463 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,466 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,469 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:40,477 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,563 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 63 statements into 2 equivalence classes.
[2025-04-28 21:21:40,610 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 63 of 63 statements.
[2025-04-28 21:21:40,611 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:40,611 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,612 INFO  L256         TraceCheckSpWp]: Trace formula consists of 280 conjuncts, 26 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,615 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,862 INFO  L134       CoverageAnalysis]: Checked inductivity of 26 backedges. 11 proven. 4 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:40,862 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:42,725 INFO  L134       CoverageAnalysis]: Checked inductivity of 26 backedges. 11 proven. 4 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:42,725 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [899607037] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:42,725 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:42,725 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 12, 12] total 26
[2025-04-28 21:21:42,725 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1600004678]
[2025-04-28 21:21:42,725 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,727 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:42,727 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,727 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:42,728 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=69, Invalid=581, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:42,728 INFO  L87              Difference]: Start difference. First operand 63 states and 82 transitions. Second operand  has 26 states, 17 states have (on average 2.6470588235294117) internal successors, (45), 24 states have internal predecessors, (45), 17 states have call successors, (28), 2 states have call predecessors, (28), 17 states have return successors, (32), 21 states have call predecessors, (32), 17 states have call successors, (32)
[2025-04-28 21:21:43,135 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,135 INFO  L93              Difference]: Finished difference Result 70 states and 92 transitions.
[2025-04-28 21:21:43,137 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:21:43,137 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 17 states have (on average 2.6470588235294117) internal successors, (45), 24 states have internal predecessors, (45), 17 states have call successors, (28), 2 states have call predecessors, (28), 17 states have return successors, (32), 21 states have call predecessors, (32), 17 states have call successors, (32) Word has length 63
[2025-04-28 21:21:43,138 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,139 INFO  L225             Difference]: With dead ends: 70
[2025-04-28 21:21:43,139 INFO  L226             Difference]: Without dead ends: 70
[2025-04-28 21:21:43,139 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 150 GetRequests, 116 SyntacticMatches, 5 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 206 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=104, Invalid=826, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:21:43,142 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 6 mSDsluCounter, 980 mSDsCounter, 0 mSdLazyCounter, 287 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 1036 SdHoareTripleChecker+Invalid, 292 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 287 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,142 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 1036 Invalid, 292 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 287 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:43,143 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-04-28 21:21:43,157 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 67.
[2025-04-28 21:21:43,157 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 67 states, 28 states have (on average 1.2142857142857142) internal successors, (34), 32 states have internal predecessors, (34), 17 states have call successors, (17), 10 states have call predecessors, (17), 21 states have return successors, (37), 24 states have call predecessors, (37), 17 states have call successors, (37)
[2025-04-28 21:21:43,158 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 67 states to 67 states and 88 transitions.
[2025-04-28 21:21:43,158 INFO  L79                 Accepts]: Start accepts. Automaton has 67 states and 88 transitions. Word has length 63
[2025-04-28 21:21:43,159 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,159 INFO  L485      AbstractCegarLoop]: Abstraction has 67 states and 88 transitions.
[2025-04-28 21:21:43,159 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 17 states have (on average 2.6470588235294117) internal successors, (45), 24 states have internal predecessors, (45), 17 states have call successors, (28), 2 states have call predecessors, (28), 17 states have return successors, (32), 21 states have call predecessors, (32), 17 states have call successors, (32)
[2025-04-28 21:21:43,159 INFO  L278                IsEmpty]: Start isEmpty. Operand 67 states and 88 transitions.
[2025-04-28 21:21:43,162 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 68
[2025-04-28 21:21:43,162 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,162 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,169 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:43,363 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,363 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,363 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,363 INFO  L85        PathProgramCache]: Analyzing trace with hash -1271759216, now seen corresponding path program 3 times
[2025-04-28 21:21:43,363 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,364 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1896961935]
[2025-04-28 21:21:43,364 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:43,364 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,379 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 67 statements into 3 equivalence classes.
[2025-04-28 21:21:43,391 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 67 of 67 statements.
[2025-04-28 21:21:43,392 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:43,392 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,571 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 15 proven. 2 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:43,571 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,571 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1896961935]
[2025-04-28 21:21:43,571 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1896961935] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,571 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1712040121]
[2025-04-28 21:21:43,571 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:43,571 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,574 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,576 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:43,579 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,690 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 67 statements into 3 equivalence classes.
[2025-04-28 21:21:43,743 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 67 of 67 statements.
[2025-04-28 21:21:43,743 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:43,743 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,750 INFO  L256         TraceCheckSpWp]: Trace formula consists of 301 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,753 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,798 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 15 proven. 2 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:43,798 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,986 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 15 proven. 2 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:44,986 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1712040121] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,986 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,986 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 6
[2025-04-28 21:21:44,986 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [417749131]
[2025-04-28 21:21:44,986 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,987 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:44,987 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,987 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:44,987 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:44,988 INFO  L87              Difference]: Start difference. First operand 67 states and 88 transitions. Second operand  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 5 states have call successors, (17), 2 states have call predecessors, (17), 5 states have return successors, (19), 6 states have call predecessors, (19), 5 states have call successors, (19)
[2025-04-28 21:21:45,043 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,043 INFO  L93              Difference]: Finished difference Result 63 states and 77 transitions.
[2025-04-28 21:21:45,044 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:45,044 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 5 states have call successors, (17), 2 states have call predecessors, (17), 5 states have return successors, (19), 6 states have call predecessors, (19), 5 states have call successors, (19) Word has length 67
[2025-04-28 21:21:45,045 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,046 INFO  L225             Difference]: With dead ends: 63
[2025-04-28 21:21:45,046 INFO  L226             Difference]: Without dead ends: 63
[2025-04-28 21:21:45,047 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 141 GetRequests, 136 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:45,048 INFO  L437           NwaCegarLoop]: 52 mSDtfsCounter, 1 mSDsluCounter, 192 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 244 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,048 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 244 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:45,049 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 63 states.
[2025-04-28 21:21:45,057 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 63 to 56.
[2025-04-28 21:21:45,059 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 23 states have (on average 1.2608695652173914) internal successors, (29), 27 states have internal predecessors, (29), 16 states have call successors, (16), 10 states have call predecessors, (16), 16 states have return successors, (23), 19 states have call predecessors, (23), 16 states have call successors, (23)
[2025-04-28 21:21:45,060 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 68 transitions.
[2025-04-28 21:21:45,060 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 68 transitions. Word has length 67
[2025-04-28 21:21:45,061 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,061 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 68 transitions.
[2025-04-28 21:21:45,061 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 5 states have call successors, (17), 2 states have call predecessors, (17), 5 states have return successors, (19), 6 states have call predecessors, (19), 5 states have call successors, (19)
[2025-04-28 21:21:45,061 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 68 transitions.
[2025-04-28 21:21:45,062 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 61
[2025-04-28 21:21:45,063 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,063 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,068 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:45,263 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,263 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,264 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,264 INFO  L85        PathProgramCache]: Analyzing trace with hash -1352263602, now seen corresponding path program 1 times
[2025-04-28 21:21:45,264 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,264 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1930303936]
[2025-04-28 21:21:45,264 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,264 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,275 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 60 statements into 1 equivalence classes.
[2025-04-28 21:21:45,281 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:45,282 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,282 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,323 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 8 proven. 2 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:45,324 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,324 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1930303936]
[2025-04-28 21:21:45,324 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1930303936] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,324 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [976302199]
[2025-04-28 21:21:45,324 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,324 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,327 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,329 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:45,333 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,441 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 60 statements into 1 equivalence classes.
[2025-04-28 21:21:45,487 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:45,487 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,487 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,489 INFO  L256         TraceCheckSpWp]: Trace formula consists of 274 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,490 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:45,507 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 9 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:45,507 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:45,507 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [976302199] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,507 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:45,507 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 4
[2025-04-28 21:21:45,507 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [232880090]
[2025-04-28 21:21:45,508 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,508 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:45,510 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,510 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:45,510 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:45,510 INFO  L87              Difference]: Start difference. First operand 56 states and 68 transitions. Second operand  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (16), 2 states have call predecessors, (16), 3 states have return successors, (16), 2 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:45,523 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,523 INFO  L93              Difference]: Finished difference Result 58 states and 69 transitions.
[2025-04-28 21:21:45,524 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:45,524 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (16), 2 states have call predecessors, (16), 3 states have return successors, (16), 2 states have call predecessors, (16), 3 states have call successors, (16) Word has length 60
[2025-04-28 21:21:45,524 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,524 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:21:45,525 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:45,525 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 63 GetRequests, 61 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:45,525 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 1 mSDsluCounter, 100 mSDsCounter, 0 mSdLazyCounter, 5 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 156 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 5 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,526 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 156 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 5 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:45,526 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:45,532 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 56.
[2025-04-28 21:21:45,535 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 23 states have (on average 1.173913043478261) internal successors, (27), 27 states have internal predecessors, (27), 16 states have call successors, (16), 10 states have call predecessors, (16), 16 states have return successors, (23), 19 states have call predecessors, (23), 16 states have call successors, (23)
[2025-04-28 21:21:45,536 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 66 transitions.
[2025-04-28 21:21:45,536 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 66 transitions. Word has length 60
[2025-04-28 21:21:45,536 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,537 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 66 transitions.
[2025-04-28 21:21:45,537 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (16), 2 states have call predecessors, (16), 3 states have return successors, (16), 2 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:45,538 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 66 transitions.
[2025-04-28 21:21:45,538 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 61
[2025-04-28 21:21:45,540 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,540 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,546 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:45,743 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:45,744 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,744 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,744 INFO  L85        PathProgramCache]: Analyzing trace with hash 2136168085, now seen corresponding path program 1 times
[2025-04-28 21:21:45,744 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,744 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1949491757]
[2025-04-28 21:21:45,744 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,744 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,757 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 60 statements into 1 equivalence classes.
[2025-04-28 21:21:45,763 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:45,765 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,765 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,805 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 8 proven. 2 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:45,805 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,805 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1949491757]
[2025-04-28 21:21:45,805 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1949491757] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,805 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2062019405]
[2025-04-28 21:21:45,805 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,805 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,808 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,810 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:45,813 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,927 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 60 statements into 1 equivalence classes.
[2025-04-28 21:21:45,969 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:45,969 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,970 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,971 INFO  L256         TraceCheckSpWp]: Trace formula consists of 274 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,975 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,002 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 9 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:46,002 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:46,002 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2062019405] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,002 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:46,003 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:21:46,003 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1238492097]
[2025-04-28 21:21:46,003 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,003 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:46,003 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,004 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:46,004 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:46,004 INFO  L87              Difference]: Start difference. First operand 56 states and 66 transitions. Second operand  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (16), 2 states have call predecessors, (16), 3 states have return successors, (16), 2 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:46,014 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,014 INFO  L93              Difference]: Finished difference Result 58 states and 67 transitions.
[2025-04-28 21:21:46,015 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:46,015 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (16), 2 states have call predecessors, (16), 3 states have return successors, (16), 2 states have call predecessors, (16), 3 states have call successors, (16) Word has length 60
[2025-04-28 21:21:46,015 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,016 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:21:46,016 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:46,016 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 63 GetRequests, 59 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:46,016 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 1 mSDsluCounter, 98 mSDsCounter, 0 mSdLazyCounter, 4 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 152 SdHoareTripleChecker+Invalid, 4 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 4 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,017 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 152 Invalid, 4 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 4 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:46,017 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:46,020 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 56.
[2025-04-28 21:21:46,021 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 23 states have (on average 1.1304347826086956) internal successors, (26), 26 states have internal predecessors, (26), 16 states have call successors, (16), 10 states have call predecessors, (16), 16 states have return successors, (23), 19 states have call predecessors, (23), 16 states have call successors, (23)
[2025-04-28 21:21:46,021 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 65 transitions.
[2025-04-28 21:21:46,021 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 65 transitions. Word has length 60
[2025-04-28 21:21:46,022 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,022 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 65 transitions.
[2025-04-28 21:21:46,022 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 3 states have call successors, (16), 2 states have call predecessors, (16), 3 states have return successors, (16), 2 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:46,022 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 65 transitions.
[2025-04-28 21:21:46,023 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 68
[2025-04-28 21:21:46,023 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,023 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,028 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:46,223 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,224 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,224 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,224 INFO  L85        PathProgramCache]: Analyzing trace with hash 23369421, now seen corresponding path program 1 times
[2025-04-28 21:21:46,224 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,224 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1382483914]
[2025-04-28 21:21:46,224 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,224 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,237 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 67 statements into 1 equivalence classes.
[2025-04-28 21:21:46,252 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 67 of 67 statements.
[2025-04-28 21:21:46,254 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,254 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,641 INFO  L134       CoverageAnalysis]: Checked inductivity of 34 backedges. 10 proven. 2 refuted. 0 times theorem prover too weak. 22 trivial. 0 not checked.
[2025-04-28 21:21:46,641 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,641 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1382483914]
[2025-04-28 21:21:46,642 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1382483914] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,642 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1967404207]
[2025-04-28 21:21:46,642 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,642 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,644 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,646 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:46,650 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,767 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 67 statements into 1 equivalence classes.
[2025-04-28 21:21:46,836 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 67 of 67 statements.
[2025-04-28 21:21:46,836 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,836 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,838 INFO  L256         TraceCheckSpWp]: Trace formula consists of 299 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,840 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,921 INFO  L134       CoverageAnalysis]: Checked inductivity of 34 backedges. 20 proven. 0 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:46,922 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:46,922 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1967404207] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,922 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:46,922 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [13] total 16
[2025-04-28 21:21:46,922 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [289154346]
[2025-04-28 21:21:46,922 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,923 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:46,923 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,924 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:46,924 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=31, Invalid=209, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:46,925 INFO  L87              Difference]: Start difference. First operand 56 states and 65 transitions. Second operand  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 4 states have call successors, (17), 2 states have call predecessors, (17), 4 states have return successors, (18), 4 states have call predecessors, (18), 4 states have call successors, (18)
[2025-04-28 21:21:46,949 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,950 INFO  L93              Difference]: Finished difference Result 56 states and 64 transitions.
[2025-04-28 21:21:46,951 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:46,951 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 4 states have call successors, (17), 2 states have call predecessors, (17), 4 states have return successors, (18), 4 states have call predecessors, (18), 4 states have call successors, (18) Word has length 67
[2025-04-28 21:21:46,952 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,953 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:46,953 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:46,953 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 79 GetRequests, 65 SyntacticMatches, 0 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 16 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=31, Invalid=209, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:46,954 INFO  L437           NwaCegarLoop]: 51 mSDtfsCounter, 1 mSDsluCounter, 143 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 194 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,954 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 194 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:46,954 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:46,957 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 56.
[2025-04-28 21:21:46,958 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 23 states have (on average 1.1304347826086956) internal successors, (26), 26 states have internal predecessors, (26), 16 states have call successors, (16), 10 states have call predecessors, (16), 16 states have return successors, (22), 19 states have call predecessors, (22), 16 states have call successors, (22)
[2025-04-28 21:21:46,958 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 64 transitions.
[2025-04-28 21:21:46,958 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 64 transitions. Word has length 67
[2025-04-28 21:21:46,959 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,959 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 64 transitions.
[2025-04-28 21:21:46,959 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 4 states have call successors, (17), 2 states have call predecessors, (17), 4 states have return successors, (18), 4 states have call predecessors, (18), 4 states have call successors, (18)
[2025-04-28 21:21:46,959 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 64 transitions.
[2025-04-28 21:21:46,960 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 83
[2025-04-28 21:21:46,960 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,960 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 4, 4, 4, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,966 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:47,164 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable14
[2025-04-28 21:21:47,165 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,165 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,165 INFO  L85        PathProgramCache]: Analyzing trace with hash 486719556, now seen corresponding path program 2 times
[2025-04-28 21:21:47,165 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,165 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [515792509]
[2025-04-28 21:21:47,165 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,165 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,177 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 82 statements into 2 equivalence classes.
[2025-04-28 21:21:47,189 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 82 of 82 statements.
[2025-04-28 21:21:47,189 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,189 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,658 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 20 proven. 3 refuted. 0 times theorem prover too weak. 47 trivial. 0 not checked.
[2025-04-28 21:21:47,658 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,658 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [515792509]
[2025-04-28 21:21:47,658 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [515792509] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,658 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [321148339]
[2025-04-28 21:21:47,658 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,658 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,661 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,663 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:47,670 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,797 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 82 statements into 2 equivalence classes.
[2025-04-28 21:21:47,852 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 82 of 82 statements.
[2025-04-28 21:21:47,852 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,852 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,854 INFO  L256         TraceCheckSpWp]: Trace formula consists of 374 conjuncts, 31 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,857 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,021 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 18 proven. 5 refuted. 0 times theorem prover too weak. 47 trivial. 0 not checked.
[2025-04-28 21:21:48,022 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,390 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 20 proven. 3 refuted. 0 times theorem prover too weak. 47 trivial. 0 not checked.
[2025-04-28 21:21:51,390 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [321148339] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,390 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,390 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 13, 13] total 23
[2025-04-28 21:21:51,390 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [417808485]
[2025-04-28 21:21:51,390 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,391 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:51,391 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,391 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:51,392 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=66, Invalid=440, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:51,392 INFO  L87              Difference]: Start difference. First operand 56 states and 64 transitions. Second operand  has 23 states, 13 states have (on average 3.0) internal successors, (39), 21 states have internal predecessors, (39), 16 states have call successors, (29), 2 states have call predecessors, (29), 13 states have return successors, (32), 18 states have call predecessors, (32), 16 states have call successors, (32)
[2025-04-28 21:21:51,636 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,637 INFO  L93              Difference]: Finished difference Result 61 states and 70 transitions.
[2025-04-28 21:21:51,637 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:51,638 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 13 states have (on average 3.0) internal successors, (39), 21 states have internal predecessors, (39), 16 states have call successors, (29), 2 states have call predecessors, (29), 13 states have return successors, (32), 18 states have call predecessors, (32), 16 states have call successors, (32) Word has length 82
[2025-04-28 21:21:51,638 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,640 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:51,640 INFO  L226             Difference]: Without dead ends: 60
[2025-04-28 21:21:51,641 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 181 GetRequests, 153 SyntacticMatches, 5 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 103 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=82, Invalid=518, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:51,642 INFO  L437           NwaCegarLoop]: 52 mSDtfsCounter, 6 mSDsluCounter, 600 mSDsCounter, 0 mSdLazyCounter, 180 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 652 SdHoareTripleChecker+Invalid, 186 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 180 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,642 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 652 Invalid, 186 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 180 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:51,642 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 60 states.
[2025-04-28 21:21:51,646 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 60 to 60.
[2025-04-28 21:21:51,646 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 60 states, 25 states have (on average 1.12) internal successors, (28), 28 states have internal predecessors, (28), 16 states have call successors, (16), 10 states have call predecessors, (16), 18 states have return successors, (24), 21 states have call predecessors, (24), 16 states have call successors, (24)
[2025-04-28 21:21:51,647 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 60 states to 60 states and 68 transitions.
[2025-04-28 21:21:51,647 INFO  L79                 Accepts]: Start accepts. Automaton has 60 states and 68 transitions. Word has length 82
[2025-04-28 21:21:51,648 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,648 INFO  L485      AbstractCegarLoop]: Abstraction has 60 states and 68 transitions.
[2025-04-28 21:21:51,648 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 13 states have (on average 3.0) internal successors, (39), 21 states have internal predecessors, (39), 16 states have call successors, (29), 2 states have call predecessors, (29), 13 states have return successors, (32), 18 states have call predecessors, (32), 16 states have call successors, (32)
[2025-04-28 21:21:51,648 INFO  L278                IsEmpty]: Start isEmpty. Operand 60 states and 68 transitions.
[2025-04-28 21:21:51,649 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 94
[2025-04-28 21:21:51,649 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,649 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 4, 4, 4, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,656 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:51,850 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-04-28 21:21:51,850 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,850 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,851 INFO  L85        PathProgramCache]: Analyzing trace with hash 1061857338, now seen corresponding path program 3 times
[2025-04-28 21:21:51,851 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,851 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1569680317]
[2025-04-28 21:21:51,851 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:51,851 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,865 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 93 statements into 4 equivalence classes.
[2025-04-28 21:21:51,887 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 93 of 93 statements.
[2025-04-28 21:21:51,887 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:51,887 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,556 INFO  L134       CoverageAnalysis]: Checked inductivity of 84 backedges. 1 proven. 35 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:21:53,556 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,557 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1569680317]
[2025-04-28 21:21:53,557 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1569680317] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,557 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1225890812]
[2025-04-28 21:21:53,557 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:53,557 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,559 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,566 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:53,568 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,730 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 93 statements into 4 equivalence classes.
[2025-04-28 21:21:53,795 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 93 of 93 statements.
[2025-04-28 21:21:53,796 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:53,796 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,806 INFO  L256         TraceCheckSpWp]: Trace formula consists of 428 conjuncts, 123 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,811 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,821 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 6 treesize of output 5
[2025-04-28 21:21:54,457 INFO  L134       CoverageAnalysis]: Checked inductivity of 84 backedges. 1 proven. 35 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:21:54,457 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
