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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:36,733 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:36,837 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_78feb7a3-b83b-4005-bd6c-7dc9195c43b0/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:36,842 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:36,843 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:36,866 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:36,867 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:36,867 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:36,867 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:36,867 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:36,868 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:36,868 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:36,868 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:36,868 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:36,868 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:36,868 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:36,868 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:36,868 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:36,869 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:36,869 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:36,869 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:36,869 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:36,869 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:36,869 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:36,869 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:36,870 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:36,870 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:37,179 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:37,192 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:37,196 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:37,200 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:37,200 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:37,202 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_78feb7a3-b83b-4005-bd6c-7dc9195c43b0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-081.smt2
[2025-04-28 21:21:37,205 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:37,209 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:37,513 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_78feb7a3-b83b-4005-bd6c-7dc9195c43b0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-081.smt2
[2025-04-28 21:21:37,517 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:37,518 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:37,519 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:37,519 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:37,519 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:37,522 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,557 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37 Unit
[2025-04-28 21:21:37,558 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:37,559 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:37,559 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:37,559 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:37,576 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,577 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,611 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,611 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,618 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,623 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,625 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,626 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,633 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,653 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:37,654 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:37,654 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:37,655 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:37,659 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,662 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:37,682 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,696 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:37,700 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:37,720 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:37,721 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:37,721 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:37,721 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:37,721 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:37,721 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:37,721 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb52.i given in one single declaration
[2025-04-28 21:21:37,721 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb52.i
[2025-04-28 21:21:37,721 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb52.i
[2025-04-28 21:21:37,722 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb18.i given in one single declaration
[2025-04-28 21:21:37,722 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb18.i
[2025-04-28 21:21:37,722 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb18.i
[2025-04-28 21:21:37,722 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:37,722 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:37,722 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:37,722 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:37,722 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:37,722 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:37,832 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:37,835 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:38,097 INFO  L?                        ?]: Removed 78 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:38,097 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:38,115 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:38,115 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:38,117 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:38 BoogieIcfgContainer
[2025-04-28 21:21:38,118 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:38,121 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:38,122 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:38,127 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:38,127 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:37" (1/3) ...
[2025-04-28 21:21:38,128 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@244f3afb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:38, skipping insertion in model container
[2025-04-28 21:21:38,128 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (2/3) ...
[2025-04-28 21:21:38,128 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@244f3afb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:38, skipping insertion in model container
[2025-04-28 21:21:38,128 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:38" (3/3) ...
[2025-04-28 21:21:38,130 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:38,148 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:38,151 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 6 procedures, 24 locations, 34 edges, 6 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:38,205 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:38,219 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;@2fcd2821, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:38,219 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:38,225 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 24 states, 10 states have (on average 1.3) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 5 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:38,236 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:38,236 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,237 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:38,238 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,244 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,246 INFO  L85        PathProgramCache]: Analyzing trace with hash -1702169744, now seen corresponding path program 1 times
[2025-04-28 21:21:38,255 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,255 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1415138719]
[2025-04-28 21:21:38,256 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,256 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,301 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:38,348 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:38,349 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,350 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,767 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:38,767 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,767 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1415138719]
[2025-04-28 21:21:38,768 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1415138719] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:38,768 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,775 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:38,777 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1563353918]
[2025-04-28 21:21:38,780 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,784 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:38,785 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,818 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:38,819 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:38,821 INFO  L87              Difference]: Start difference. First operand  has 24 states, 10 states have (on average 1.3) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 5 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 7 states have call successors, (7) Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:38,967 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,967 INFO  L93              Difference]: Finished difference Result 28 states and 33 transitions.
[2025-04-28 21:21:39,001 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:39,003 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 19
[2025-04-28 21:21:39,003 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,014 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:39,018 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:39,021 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:39,031 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 3 mSDsluCounter, 73 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 95 SdHoareTripleChecker+Invalid, 28 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,033 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 95 Invalid, 28 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:39,059 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:39,097 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 26.
[2025-04-28 21:21:39,099 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 5 states have call predecessors, (7), 7 states have return successors, (10), 7 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:39,104 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 30 transitions.
[2025-04-28 21:21:39,112 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 30 transitions. Word has length 19
[2025-04-28 21:21:39,113 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,113 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 30 transitions.
[2025-04-28 21:21:39,113 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:39,113 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 30 transitions.
[2025-04-28 21:21:39,115 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-04-28 21:21:39,116 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,117 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]
[2025-04-28 21:21:39,117 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:39,117 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,118 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,118 INFO  L85        PathProgramCache]: Analyzing trace with hash -864348446, now seen corresponding path program 1 times
[2025-04-28 21:21:39,118 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,118 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1467199362]
[2025-04-28 21:21:39,118 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,119 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,146 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:39,174 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:39,174 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,174 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,464 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:39,465 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,465 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1467199362]
[2025-04-28 21:21:39,465 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1467199362] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,465 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,465 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:39,466 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [191768890]
[2025-04-28 21:21:39,466 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,468 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:39,468 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,469 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:39,469 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:39,469 INFO  L87              Difference]: Start difference. First operand 26 states and 30 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:39,499 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,500 INFO  L93              Difference]: Finished difference Result 26 states and 30 transitions.
[2025-04-28 21:21:39,500 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:39,500 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6) Word has length 23
[2025-04-28 21:21:39,501 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,501 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:39,501 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:39,502 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:39,502 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 1 mSDsluCounter, 40 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 64 SdHoareTripleChecker+Invalid, 7 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,503 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 64 Invalid, 7 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:39,504 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:39,507 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 24.
[2025-04-28 21:21:39,507 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 10 states have (on average 1.2) internal successors, (12), 12 states have internal predecessors, (12), 7 states have call successors, (7), 5 states have call predecessors, (7), 6 states have return successors, (8), 6 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:39,508 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 27 transitions.
[2025-04-28 21:21:39,508 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 27 transitions. Word has length 23
[2025-04-28 21:21:39,509 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,509 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 27 transitions.
[2025-04-28 21:21:39,509 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:39,509 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 27 transitions.
[2025-04-28 21:21:39,510 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-04-28 21:21:39,510 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,510 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]
[2025-04-28 21:21:39,510 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:39,510 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,511 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,511 INFO  L85        PathProgramCache]: Analyzing trace with hash 1852032173, now seen corresponding path program 1 times
[2025-04-28 21:21:39,511 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,511 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2143770685]
[2025-04-28 21:21:39,511 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,512 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,527 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:39,590 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:39,590 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,590 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,612 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:40,612 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,612 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2143770685]
[2025-04-28 21:21:40,612 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2143770685] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,613 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [240947094]
[2025-04-28 21:21:40,613 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,613 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,617 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,622 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:40,623 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,718 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:40,764 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:40,765 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,765 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,769 INFO  L256         TraceCheckSpWp]: Trace formula consists of 182 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,776 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,041 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 1 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 12
[2025-04-28 21:21:41,424 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:41,424 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,904 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:45,904 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 1 new quantified variables, introduced 1 case distinctions, treesize of input 9 treesize of output 13
[2025-04-28 21:21:46,727 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:46,727 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 1 new quantified variables, introduced 1 case distinctions, treesize of input 9 treesize of output 13
[2025-04-28 21:21:47,077 INFO  L325             Elim1Store]: treesize reduction 5, result has 16.7 percent of original size
[2025-04-28 21:21:47,077 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 1 new quantified variables, introduced 1 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:47,092 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:47,092 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [240947094] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,092 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,092 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 15
[2025-04-28 21:21:47,093 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1778967608]
[2025-04-28 21:21:47,093 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,093 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:47,093 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,096 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:47,097 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=47, Invalid=163, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:47,097 INFO  L87              Difference]: Start difference. First operand 24 states and 27 transitions. Second operand  has 15 states, 8 states have (on average 2.375) internal successors, (19), 15 states have internal predecessors, (19), 10 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (13), 7 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:47,259 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,261 INFO  L93              Difference]: Finished difference Result 30 states and 35 transitions.
[2025-04-28 21:21:47,261 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:47,261 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 8 states have (on average 2.375) internal successors, (19), 15 states have internal predecessors, (19), 10 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (13), 7 states have call predecessors, (13), 10 states have call successors, (13) Word has length 23
[2025-04-28 21:21:47,262 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,262 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:47,263 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:47,264 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 40 SyntacticMatches, 0 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 39 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=54, Invalid=186, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:47,266 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 4 mSDsluCounter, 177 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 200 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,267 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 200 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:47,270 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:47,273 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 28.
[2025-04-28 21:21:47,273 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 5 states have call predecessors, (7), 8 states have return successors, (11), 8 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:47,276 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 32 transitions.
[2025-04-28 21:21:47,277 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 32 transitions. Word has length 23
[2025-04-28 21:21:47,277 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,277 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 32 transitions.
[2025-04-28 21:21:47,277 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 8 states have (on average 2.375) internal successors, (19), 15 states have internal predecessors, (19), 10 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (13), 7 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:47,278 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 32 transitions.
[2025-04-28 21:21:47,279 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 28
[2025-04-28 21:21:47,280 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,280 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]
[2025-04-28 21:21:47,286 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:47,480 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,481 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,481 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,481 INFO  L85        PathProgramCache]: Analyzing trace with hash -2119075617, now seen corresponding path program 1 times
[2025-04-28 21:21:47,482 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,482 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1062503986]
[2025-04-28 21:21:47,482 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,482 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,499 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 27 statements into 1 equivalence classes.
[2025-04-28 21:21:47,515 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:47,516 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,516 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,911 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:47,911 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,912 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1062503986]
[2025-04-28 21:21:47,912 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1062503986] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,912 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1669601083]
[2025-04-28 21:21:47,912 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,912 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,915 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,917 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:47,921 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,997 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 27 statements into 1 equivalence classes.
[2025-04-28 21:21:48,032 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:48,033 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,033 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,035 INFO  L256         TraceCheckSpWp]: Trace formula consists of 209 conjuncts, 31 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,037 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,218 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:48,219 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,003 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:52,004 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1669601083] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,004 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,004 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 20
[2025-04-28 21:21:52,004 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [709977742]
[2025-04-28 21:21:52,004 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,005 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:52,005 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,005 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:52,006 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=66, Invalid=314, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:52,006 INFO  L87              Difference]: Start difference. First operand 28 states and 32 transitions. Second operand  has 20 states, 10 states have (on average 2.4) internal successors, (24), 20 states have internal predecessors, (24), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (16), 9 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:52,162 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,162 INFO  L93              Difference]: Finished difference Result 32 states and 37 transitions.
[2025-04-28 21:21:52,163 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:52,163 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.4) internal successors, (24), 20 states have internal predecessors, (24), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (16), 9 states have call predecessors, (16), 13 states have call successors, (16) Word has length 27
[2025-04-28 21:21:52,163 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,164 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:52,164 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:52,164 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 43 SyntacticMatches, 2 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 101 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=90, Invalid=416, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:52,165 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 10 mSDsluCounter, 123 mSDsCounter, 0 mSdLazyCounter, 78 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 146 SdHoareTripleChecker+Invalid, 86 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 78 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,165 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 146 Invalid, 86 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 78 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:52,166 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:52,169 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 26.
[2025-04-28 21:21:52,169 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 5 states have call predecessors, (7), 7 states have return successors, (9), 7 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:52,170 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 29 transitions.
[2025-04-28 21:21:52,170 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 29 transitions. Word has length 27
[2025-04-28 21:21:52,171 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,171 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 29 transitions.
[2025-04-28 21:21:52,171 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.4) internal successors, (24), 20 states have internal predecessors, (24), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (16), 9 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:52,171 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 29 transitions.
[2025-04-28 21:21:52,172 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 28
[2025-04-28 21:21:52,172 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,172 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,176 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:52,372 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,373 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,373 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,373 INFO  L85        PathProgramCache]: Analyzing trace with hash -574323542, now seen corresponding path program 2 times
[2025-04-28 21:21:52,373 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,373 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [951368435]
[2025-04-28 21:21:52,374 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:52,374 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,390 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 27 statements into 2 equivalence classes.
[2025-04-28 21:21:52,428 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:52,428 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:52,428 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,579 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:53,579 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,580 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [951368435]
[2025-04-28 21:21:53,580 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [951368435] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,580 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [159897762]
[2025-04-28 21:21:53,580 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:53,580 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,583 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,584 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:53,588 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,687 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 27 statements into 2 equivalence classes.
[2025-04-28 21:21:53,731 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:53,732 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:53,732 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,734 INFO  L256         TraceCheckSpWp]: Trace formula consists of 260 conjuncts, 74 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,737 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,971 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 1 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 12
[2025-04-28 21:21:54,161 INFO  L325             Elim1Store]: treesize reduction 15, result has 37.5 percent of original size
[2025-04-28 21:21:54,161 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 1 case distinctions, treesize of input 26 treesize of output 21
[2025-04-28 21:21:54,245 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:54,245 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:04,410 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:04,410 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 1 new quantified variables, introduced 1 case distinctions, treesize of input 9 treesize of output 13
[2025-04-28 21:22:04,892 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:04,892 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 1 case distinctions, treesize of input 7 treesize of output 6
[2025-04-28 21:22:05,034 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:05,034 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 1 select indices, 1 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 2 case distinctions, treesize of input 15 treesize of output 18
[2025-04-28 21:22:07,293 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:07,294 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 1 new quantified variables, introduced 1 case distinctions, treesize of input 9 treesize of output 13
[2025-04-28 21:22:07,688 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:07,688 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 1 case distinctions, treesize of input 7 treesize of output 6
[2025-04-28 21:22:07,816 INFO  L172   IndexEqualityManager]: detected equality via solver
[2025-04-28 21:22:07,821 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:07,822 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 1 select indices, 1 select index equivalence classes, 2 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 2 case distinctions, treesize of input 15 treesize of output 18
[2025-04-28 21:22:08,522 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:08,522 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 1 new quantified variables, introduced 1 case distinctions, treesize of input 9 treesize of output 13
[2025-04-28 21:22:08,666 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 7 treesize of output 5
[2025-04-28 21:22:08,805 INFO  L325             Elim1Store]: treesize reduction 5, result has 16.7 percent of original size
[2025-04-28 21:22:08,806 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 1 new quantified variables, introduced 1 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:22:08,895 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:08,895 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [159897762] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,896 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,896 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 18
[2025-04-28 21:22:08,896 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [709323630]
[2025-04-28 21:22:08,896 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,896 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:22:08,896 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,897 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:22:08,897 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=59, Invalid=247, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:22:08,897 INFO  L87              Difference]: Start difference. First operand 26 states and 29 transitions. Second operand  has 18 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (15), 8 states have call predecessors, (15), 11 states have call successors, (15)
[2025-04-28 21:22:09,079 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:09,079 INFO  L93              Difference]: Finished difference Result 28 states and 31 transitions.
[2025-04-28 21:22:09,081 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:22:09,081 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (15), 8 states have call predecessors, (15), 11 states have call successors, (15) Word has length 27
[2025-04-28 21:22:09,082 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:09,082 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:22:09,082 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:22:09,083 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 47 SyntacticMatches, 0 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 59 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=90, Invalid=330, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:22:09,084 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 9 mSDsluCounter, 123 mSDsCounter, 0 mSdLazyCounter, 49 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 146 SdHoareTripleChecker+Invalid, 64 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 49 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:09,084 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 146 Invalid, 64 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 49 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:09,085 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:22:09,087 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 28.
[2025-04-28 21:22:09,087 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 5 states have call predecessors, (7), 8 states have return successors, (10), 8 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:22:09,088 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 31 transitions.
[2025-04-28 21:22:09,088 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 31 transitions. Word has length 27
[2025-04-28 21:22:09,088 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:09,089 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 31 transitions.
[2025-04-28 21:22:09,089 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (15), 8 states have call predecessors, (15), 11 states have call successors, (15)
[2025-04-28 21:22:09,089 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 31 transitions.
[2025-04-28 21:22:09,090 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 32
[2025-04-28 21:22:09,090 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:09,090 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:09,094 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:22:09,290 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,290 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,291 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,291 INFO  L85        PathProgramCache]: Analyzing trace with hash 131668380, now seen corresponding path program 2 times
[2025-04-28 21:22:09,291 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,291 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [594774114]
[2025-04-28 21:22:09,291 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:09,291 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,304 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 31 statements into 2 equivalence classes.
[2025-04-28 21:22:09,330 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 31 of 31 statements.
[2025-04-28 21:22:09,330 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:09,331 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
