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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:16,055 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:16,133 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3c1987df-6745-4699-a10a-2302a1cab0b1/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:16,138 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:16,138 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:16,158 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:16,159 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:16,159 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:16,159 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:16,159 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:16,160 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:16,160 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:16,160 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:16,160 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:16,160 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:16,160 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:16,160 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:16,160 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:16,160 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:16,161 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:16,161 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:16,161 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:16,161 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:16,161 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:16,161 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:16,162 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:16,162 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:16,462 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:16,472 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:16,474 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:16,475 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:16,476 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:16,477 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3c1987df-6745-4699-a10a-2302a1cab0b1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-044.smt2
[2025-04-28 21:21:16,481 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:16,485 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:16,741 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3c1987df-6745-4699-a10a-2302a1cab0b1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-044.smt2
[2025-04-28 21:21:16,744 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:16,745 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:16,746 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:16,746 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:16,746 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:16,749 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,799 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16 Unit
[2025-04-28 21:21:16,800 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:16,801 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:16,801 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:16,801 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:16,816 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,816 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,841 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,842 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,845 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,846 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,848 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,849 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,850 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,865 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:16,865 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:16,866 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:16,866 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:16,866 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,869 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:16,880 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:16,893 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:16,896 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:16,911 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:16,912 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:16,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:16,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:16,912 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:16,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:16,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb44.i given in one single declaration
[2025-04-28 21:21:16,913 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb44.i
[2025-04-28 21:21:16,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb44.i
[2025-04-28 21:21:16,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb30.i given in one single declaration
[2025-04-28 21:21:16,913 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb30.i
[2025-04-28 21:21:16,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb30.i
[2025-04-28 21:21:16,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATbb13.i given in one single declaration
[2025-04-28 21:21:16,913 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATbb13.i
[2025-04-28 21:21:16,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATbb13.i
[2025-04-28 21:21:16,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:16,915 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:16,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:16,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:16,915 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:16,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:16,989 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:16,992 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:17,230 INFO  L?                        ?]: Removed 68 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:17,230 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:17,245 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:17,245 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:17,245 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17 BoogieIcfgContainer
[2025-04-28 21:21:17,246 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:17,252 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:17,252 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:17,256 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:17,256 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:16" (1/3) ...
[2025-04-28 21:21:17,256 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5907d43 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,257 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (2/3) ...
[2025-04-28 21:21:17,258 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5907d43 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,258 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17" (3/3) ...
[2025-04-28 21:21:17,260 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:17,278 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:17,281 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 29 locations, 43 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:17,322 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:17,333 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;@6b02c22f, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:17,334 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:17,337 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 29 states, 12 states have (on average 1.3333333333333333) internal successors, (16), 16 states have internal predecessors, (16), 9 states have call successors, (9), 6 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 9 states have call successors, (9)
[2025-04-28 21:21:17,345 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-04-28 21:21:17,345 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,346 INFO  L218           NwaCegarLoop]: trace histogram [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:17,346 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,351 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,351 INFO  L85        PathProgramCache]: Analyzing trace with hash 368567960, now seen corresponding path program 1 times
[2025-04-28 21:21:17,359 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,359 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [681454753]
[2025-04-28 21:21:17,359 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,360 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,391 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:17,428 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:17,429 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,429 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,876 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:17,876 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,876 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [681454753]
[2025-04-28 21:21:17,877 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [681454753] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,877 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,879 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:17,881 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2136780889]
[2025-04-28 21:21:17,882 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,885 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:17,885 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,915 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:17,916 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:17,917 INFO  L87              Difference]: Start difference. First operand  has 29 states, 12 states have (on average 1.3333333333333333) internal successors, (16), 16 states have internal predecessors, (16), 9 states have call successors, (9), 6 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 9 states have call successors, (9) Second operand  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:18,058 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,059 INFO  L93              Difference]: Finished difference Result 33 states and 40 transitions.
[2025-04-28 21:21:18,060 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:18,061 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6) Word has length 23
[2025-04-28 21:21:18,062 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,099 INFO  L225             Difference]: With dead ends: 33
[2025-04-28 21:21:18,100 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:21:18,105 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:18,111 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 3 mSDsluCounter, 101 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 130 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:18,112 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 130 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:18,131 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:21:18,163 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 31.
[2025-04-28 21:21:18,165 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 13 states have (on average 1.2307692307692308) internal successors, (16), 16 states have internal predecessors, (16), 9 states have call successors, (9), 6 states have call predecessors, (9), 8 states have return successors, (12), 8 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:18,172 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 37 transitions.
[2025-04-28 21:21:18,173 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 37 transitions. Word has length 23
[2025-04-28 21:21:18,174 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,174 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 37 transitions.
[2025-04-28 21:21:18,174 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:18,174 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 37 transitions.
[2025-04-28 21:21:18,188 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 28
[2025-04-28 21:21:18,190 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,190 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]
[2025-04-28 21:21:18,190 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:18,191 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,192 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,192 INFO  L85        PathProgramCache]: Analyzing trace with hash -175825482, now seen corresponding path program 1 times
[2025-04-28 21:21:18,192 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,193 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1774537491]
[2025-04-28 21:21:18,193 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,193 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,215 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 27 statements into 1 equivalence classes.
[2025-04-28 21:21:18,252 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:18,256 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,256 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,567 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:18,567 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,567 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1774537491]
[2025-04-28 21:21:18,568 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1774537491] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,568 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,568 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:18,568 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1947071719]
[2025-04-28 21:21:18,568 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,569 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:18,570 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,570 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:18,570 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:18,571 INFO  L87              Difference]: Start difference. First operand 31 states and 37 transitions. Second operand  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:18,710 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,710 INFO  L93              Difference]: Finished difference Result 43 states and 53 transitions.
[2025-04-28 21:21:18,711 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:18,711 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 5 states have call successors, (7) Word has length 27
[2025-04-28 21:21:18,712 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,713 INFO  L225             Difference]: With dead ends: 43
[2025-04-28 21:21:18,713 INFO  L226             Difference]: Without dead ends: 43
[2025-04-28 21:21:18,714 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:18,715 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 5 mSDsluCounter, 139 mSDsCounter, 0 mSdLazyCounter, 56 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 166 SdHoareTripleChecker+Invalid, 56 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 56 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,719 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 166 Invalid, 56 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 56 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:18,719 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 43 states.
[2025-04-28 21:21:18,726 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 43 to 35.
[2025-04-28 21:21:18,728 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 15 states have (on average 1.2) internal successors, (18), 18 states have internal predecessors, (18), 9 states have call successors, (9), 6 states have call predecessors, (9), 10 states have return successors, (16), 10 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:18,730 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 43 transitions.
[2025-04-28 21:21:18,731 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 43 transitions. Word has length 27
[2025-04-28 21:21:18,731 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,731 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 43 transitions.
[2025-04-28 21:21:18,732 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:18,733 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 43 transitions.
[2025-04-28 21:21:18,733 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 28
[2025-04-28 21:21:18,734 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,734 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]
[2025-04-28 21:21:18,734 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:18,734 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,735 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,735 INFO  L85        PathProgramCache]: Analyzing trace with hash -2060801022, now seen corresponding path program 1 times
[2025-04-28 21:21:18,735 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,735 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [842416015]
[2025-04-28 21:21:18,735 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,735 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,751 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 27 statements into 1 equivalence classes.
[2025-04-28 21:21:18,768 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 27 of 27 statements.
[2025-04-28 21:21:18,768 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,768 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,973 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:18,974 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,974 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [842416015]
[2025-04-28 21:21:18,974 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [842416015] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,974 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,974 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:18,974 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1030970530]
[2025-04-28 21:21:18,974 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,975 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:18,975 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,975 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:18,979 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:18,979 INFO  L87              Difference]: Start difference. First operand 35 states and 43 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:19,078 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,078 INFO  L93              Difference]: Finished difference Result 39 states and 47 transitions.
[2025-04-28 21:21:19,078 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:19,079 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7) Word has length 27
[2025-04-28 21:21:19,079 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,080 INFO  L225             Difference]: With dead ends: 39
[2025-04-28 21:21:19,081 INFO  L226             Difference]: Without dead ends: 39
[2025-04-28 21:21:19,081 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:19,082 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 2 mSDsluCounter, 93 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 121 SdHoareTripleChecker+Invalid, 36 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,083 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 121 Invalid, 36 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:19,084 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 39 states.
[2025-04-28 21:21:19,092 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 39 to 37.
[2025-04-28 21:21:19,094 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 37 states, 16 states have (on average 1.1875) internal successors, (19), 19 states have internal predecessors, (19), 9 states have call successors, (9), 6 states have call predecessors, (9), 11 states have return successors, (16), 11 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:19,095 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 37 states to 37 states and 44 transitions.
[2025-04-28 21:21:19,096 INFO  L79                 Accepts]: Start accepts. Automaton has 37 states and 44 transitions. Word has length 27
[2025-04-28 21:21:19,096 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,096 INFO  L485      AbstractCegarLoop]: Abstraction has 37 states and 44 transitions.
[2025-04-28 21:21:19,096 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:19,097 INFO  L278                IsEmpty]: Start isEmpty. Operand 37 states and 44 transitions.
[2025-04-28 21:21:19,098 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 32
[2025-04-28 21:21:19,099 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,099 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]
[2025-04-28 21:21:19,099 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:19,099 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,100 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,101 INFO  L85        PathProgramCache]: Analyzing trace with hash 1224160939, now seen corresponding path program 1 times
[2025-04-28 21:21:19,101 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,101 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [396641693]
[2025-04-28 21:21:19,101 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,104 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,122 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 31 statements into 1 equivalence classes.
[2025-04-28 21:21:19,180 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 31 of 31 statements.
[2025-04-28 21:21:19,182 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,183 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,743 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:20,745 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,745 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [396641693]
[2025-04-28 21:21:20,745 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [396641693] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:20,745 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1796737608]
[2025-04-28 21:21:20,745 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,745 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:20,748 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:20,754 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:20,756 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:20,827 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 31 statements into 1 equivalence classes.
[2025-04-28 21:21:20,872 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 31 of 31 statements.
[2025-04-28 21:21:20,872 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,873 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,876 INFO  L256         TraceCheckSpWp]: Trace formula consists of 204 conjuncts, 76 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:20,888 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:21,029 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 12 treesize of output 11
[2025-04-28 21:21:21,105 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 12 treesize of output 1
[2025-04-28 21:21:21,108 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 12 treesize of output 11
[2025-04-28 21:21:21,288 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 15 treesize of output 11
[2025-04-28 21:21:21,381 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:21,381 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:24,553 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:24,553 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 9 treesize of output 8
[2025-04-28 21:21:24,566 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 9 treesize of output 1
[2025-04-28 21:21:25,308 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 9 treesize of output 1
[2025-04-28 21:21:25,315 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:25,316 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 9 treesize of output 8
[2025-04-28 21:21:25,760 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:25,769 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:25,769 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 1 case distinctions, treesize of input 9 treesize of output 8
[2025-04-28 21:21:25,828 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:21:26,060 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:26,060 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 9 treesize of output 8
[2025-04-28 21:21:26,065 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 9 treesize of output 1
[2025-04-28 21:21:26,215 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:26,220 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:26,236 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 18 treesize of output 14
[2025-04-28 21:21:26,240 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 9 treesize of output 1
[2025-04-28 21:21:26,251 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:26,252 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1796737608] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:26,252 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:26,252 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 12, 12] total 25
[2025-04-28 21:21:26,252 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [471758417]
[2025-04-28 21:21:26,252 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,252 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:21:26,253 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,253 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:21:26,254 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=537, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:26,254 INFO  L87              Difference]: Start difference. First operand 37 states and 44 transitions. Second operand  has 25 states, 11 states have (on average 2.8181818181818183) internal successors, (31), 25 states have internal predecessors, (31), 17 states have call successors, (19), 1 states have call predecessors, (19), 11 states have return successors, (19), 11 states have call predecessors, (19), 17 states have call successors, (19)
[2025-04-28 21:21:27,006 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,006 INFO  L93              Difference]: Finished difference Result 55 states and 67 transitions.
[2025-04-28 21:21:27,007 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:27,007 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 11 states have (on average 2.8181818181818183) internal successors, (31), 25 states have internal predecessors, (31), 17 states have call successors, (19), 1 states have call predecessors, (19), 11 states have return successors, (19), 11 states have call predecessors, (19), 17 states have call successors, (19) Word has length 31
[2025-04-28 21:21:27,007 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,008 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:27,008 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:27,009 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 86 GetRequests, 50 SyntacticMatches, 0 SemanticMatches, 36 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 146 ImplicationChecksByTransitivity, 1.0s TimeCoverageRelationStatistics Valid=150, Invalid=1256, Unknown=0, NotChecked=0, Total=1406
[2025-04-28 21:21:27,010 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 16 mSDsluCounter, 434 mSDsCounter, 0 mSdLazyCounter, 280 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 466 SdHoareTripleChecker+Invalid, 306 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 280 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,010 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 466 Invalid, 306 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 280 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:27,011 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:27,016 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 39.
[2025-04-28 21:21:27,016 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 39 states, 17 states have (on average 1.1764705882352942) internal successors, (20), 20 states have internal predecessors, (20), 9 states have call successors, (9), 6 states have call predecessors, (9), 12 states have return successors, (18), 12 states have call predecessors, (18), 9 states have call successors, (18)
[2025-04-28 21:21:27,017 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 39 states to 39 states and 47 transitions.
[2025-04-28 21:21:27,018 INFO  L79                 Accepts]: Start accepts. Automaton has 39 states and 47 transitions. Word has length 31
[2025-04-28 21:21:27,018 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,018 INFO  L485      AbstractCegarLoop]: Abstraction has 39 states and 47 transitions.
[2025-04-28 21:21:27,018 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 11 states have (on average 2.8181818181818183) internal successors, (31), 25 states have internal predecessors, (31), 17 states have call successors, (19), 1 states have call predecessors, (19), 11 states have return successors, (19), 11 states have call predecessors, (19), 17 states have call successors, (19)
[2025-04-28 21:21:27,018 INFO  L278                IsEmpty]: Start isEmpty. Operand 39 states and 47 transitions.
[2025-04-28 21:21:27,019 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 32
[2025-04-28 21:21:27,019 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,019 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]
[2025-04-28 21:21:27,025 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:27,223 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,223 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,224 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,224 INFO  L85        PathProgramCache]: Analyzing trace with hash -1523650144, now seen corresponding path program 1 times
[2025-04-28 21:21:27,224 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,224 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1172972687]
[2025-04-28 21:21:27,224 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,224 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,234 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 31 statements into 1 equivalence classes.
[2025-04-28 21:21:27,251 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 31 of 31 statements.
[2025-04-28 21:21:27,252 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,252 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,490 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:27,490 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,490 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1172972687]
[2025-04-28 21:21:27,490 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1172972687] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,490 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,491 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:27,491 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1389352607]
[2025-04-28 21:21:27,491 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,491 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:27,491 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,492 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:27,492 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:27,492 INFO  L87              Difference]: Start difference. First operand 39 states and 47 transitions. Second operand  has 10 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 6 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:27,622 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,622 INFO  L93              Difference]: Finished difference Result 45 states and 54 transitions.
[2025-04-28 21:21:27,622 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:27,622 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 6 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 6 states have call successors, (8) Word has length 31
[2025-04-28 21:21:27,623 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,623 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:21:27,623 INFO  L226             Difference]: Without dead ends: 37
[2025-04-28 21:21:27,624 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 15 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=38, Invalid=144, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:27,624 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 7 mSDsluCounter, 178 mSDsCounter, 0 mSdLazyCounter, 84 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 205 SdHoareTripleChecker+Invalid, 86 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 84 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,625 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 205 Invalid, 86 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 84 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:27,625 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 37 states.
[2025-04-28 21:21:27,629 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 37 to 35.
[2025-04-28 21:21:27,629 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 15 states have (on average 1.2) internal successors, (18), 18 states have internal predecessors, (18), 9 states have call successors, (9), 6 states have call predecessors, (9), 10 states have return successors, (14), 10 states have call predecessors, (14), 9 states have call successors, (14)
[2025-04-28 21:21:27,630 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 41 transitions.
[2025-04-28 21:21:27,630 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 41 transitions. Word has length 31
[2025-04-28 21:21:27,630 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,630 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 41 transitions.
[2025-04-28 21:21:27,630 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 6 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:27,630 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 41 transitions.
[2025-04-28 21:21:27,631 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 36
[2025-04-28 21:21:27,631 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,631 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, 1, 1, 1, 1]
[2025-04-28 21:21:27,631 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:27,631 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,632 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,632 INFO  L85        PathProgramCache]: Analyzing trace with hash 1086576393, now seen corresponding path program 2 times
[2025-04-28 21:21:27,632 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,632 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2127973826]
[2025-04-28 21:21:27,632 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:27,632 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,641 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 35 statements into 2 equivalence classes.
[2025-04-28 21:21:27,651 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 35 of 35 statements.
[2025-04-28 21:21:27,651 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:27,651 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,954 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:27,955 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,955 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2127973826]
[2025-04-28 21:21:27,955 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2127973826] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,955 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1744866417]
[2025-04-28 21:21:27,955 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:27,955 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,958 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,961 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:27,963 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,049 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 35 statements into 2 equivalence classes.
[2025-04-28 21:21:28,087 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 35 of 35 statements.
[2025-04-28 21:21:28,087 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:28,087 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,089 INFO  L256         TraceCheckSpWp]: Trace formula consists of 242 conjuncts, 31 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,091 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,216 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 4 proven. 5 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:28,216 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:31,189 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:31,189 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1744866417] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:31,189 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:31,189 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 20
[2025-04-28 21:21:31,189 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1466779765]
[2025-04-28 21:21:31,189 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,190 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:31,190 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,191 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:31,191 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=61, Invalid=319, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:31,191 INFO  L87              Difference]: Start difference. First operand 35 states and 41 transitions. Second operand  has 20 states, 10 states have (on average 2.8) internal successors, (28), 20 states have internal predecessors, (28), 13 states have call successors, (16), 1 states have call predecessors, (16), 10 states have return successors, (18), 9 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:21:31,343 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,344 INFO  L93              Difference]: Finished difference Result 41 states and 48 transitions.
[2025-04-28 21:21:31,345 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:31,345 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.8) internal successors, (28), 20 states have internal predecessors, (28), 13 states have call successors, (16), 1 states have call predecessors, (16), 10 states have return successors, (18), 9 states have call predecessors, (18), 13 states have call successors, (18) Word has length 35
[2025-04-28 21:21:31,347 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,348 INFO  L225             Difference]: With dead ends: 41
[2025-04-28 21:21:31,348 INFO  L226             Difference]: Without dead ends: 41
[2025-04-28 21:21:31,348 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 83 GetRequests, 59 SyntacticMatches, 2 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 103 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=93, Invalid=459, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:31,349 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 8 mSDsluCounter, 314 mSDsCounter, 0 mSdLazyCounter, 129 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 344 SdHoareTripleChecker+Invalid, 135 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 129 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,349 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 344 Invalid, 135 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 129 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:31,350 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 41 states.
[2025-04-28 21:21:31,355 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 41 to 41.
[2025-04-28 21:21:31,359 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 18 states have (on average 1.1666666666666667) internal successors, (21), 21 states have internal predecessors, (21), 9 states have call successors, (9), 6 states have call predecessors, (9), 13 states have return successors, (18), 13 states have call predecessors, (18), 9 states have call successors, (18)
[2025-04-28 21:21:31,360 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 48 transitions.
[2025-04-28 21:21:31,362 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 48 transitions. Word has length 35
[2025-04-28 21:21:31,363 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,363 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 48 transitions.
[2025-04-28 21:21:31,363 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.8) internal successors, (28), 20 states have internal predecessors, (28), 13 states have call successors, (16), 1 states have call predecessors, (16), 10 states have return successors, (18), 9 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:21:31,363 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 48 transitions.
[2025-04-28 21:21:31,364 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 36
[2025-04-28 21:21:31,364 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,364 INFO  L218           NwaCegarLoop]: trace histogram [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:31,372 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:31,564 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,565 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,565 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,565 INFO  L85        PathProgramCache]: Analyzing trace with hash 1275592533, now seen corresponding path program 1 times
[2025-04-28 21:21:31,565 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,565 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [777557146]
[2025-04-28 21:21:31,566 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,566 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,580 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 35 statements into 1 equivalence classes.
[2025-04-28 21:21:31,594 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 35 of 35 statements.
[2025-04-28 21:21:31,594 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,594 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,908 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:31,908 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,908 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [777557146]
[2025-04-28 21:21:31,908 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [777557146] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,908 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1844388750]
[2025-04-28 21:21:31,908 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,909 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,911 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,913 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:31,916 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:32,026 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 35 statements into 1 equivalence classes.
[2025-04-28 21:21:32,061 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 35 of 35 statements.
[2025-04-28 21:21:32,061 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,061 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,063 INFO  L256         TraceCheckSpWp]: Trace formula consists of 238 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:32,065 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,234 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:32,234 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:34,222 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:34,222 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1844388750] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:34,222 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:34,222 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 10, 10] total 25
[2025-04-28 21:21:34,222 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1803760642]
[2025-04-28 21:21:34,222 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,225 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:21:34,225 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,226 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:21:34,226 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=75, Invalid=525, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:34,226 INFO  L87              Difference]: Start difference. First operand 41 states and 48 transitions. Second operand  has 25 states, 13 states have (on average 2.6153846153846154) internal successors, (34), 25 states have internal predecessors, (34), 16 states have call successors, (20), 1 states have call predecessors, (20), 13 states have return successors, (21), 13 states have call predecessors, (21), 16 states have call successors, (21)
[2025-04-28 21:21:34,522 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,523 INFO  L93              Difference]: Finished difference Result 45 states and 53 transitions.
[2025-04-28 21:21:34,523 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:21:34,523 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 13 states have (on average 2.6153846153846154) internal successors, (34), 25 states have internal predecessors, (34), 16 states have call successors, (20), 1 states have call predecessors, (20), 13 states have return successors, (21), 13 states have call predecessors, (21), 16 states have call successors, (21) Word has length 35
[2025-04-28 21:21:34,524 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,524 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:21:34,524 INFO  L226             Difference]: Without dead ends: 37
[2025-04-28 21:21:34,525 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 90 GetRequests, 58 SyntacticMatches, 1 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 159 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=133, Invalid=923, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:34,526 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 16 mSDsluCounter, 336 mSDsCounter, 0 mSdLazyCounter, 220 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 32 SdHoareTripleChecker+Valid, 365 SdHoareTripleChecker+Invalid, 228 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 220 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,526 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [32 Valid, 365 Invalid, 228 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 220 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:34,526 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 37 states.
[2025-04-28 21:21:34,531 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 37 to 35.
[2025-04-28 21:21:34,531 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 15 states have (on average 1.2) internal successors, (18), 18 states have internal predecessors, (18), 9 states have call successors, (9), 6 states have call predecessors, (9), 10 states have return successors, (13), 10 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:34,532 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 40 transitions.
[2025-04-28 21:21:34,535 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 40 transitions. Word has length 35
[2025-04-28 21:21:34,535 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,535 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 40 transitions.
[2025-04-28 21:21:34,535 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 13 states have (on average 2.6153846153846154) internal successors, (34), 25 states have internal predecessors, (34), 16 states have call successors, (20), 1 states have call predecessors, (20), 13 states have return successors, (21), 13 states have call predecessors, (21), 16 states have call successors, (21)
[2025-04-28 21:21:34,535 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 40 transitions.
[2025-04-28 21:21:34,536 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 40
[2025-04-28 21:21:34,538 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,539 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,545 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:34,739 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,740 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,740 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,740 INFO  L85        PathProgramCache]: Analyzing trace with hash 774068862, now seen corresponding path program 3 times
[2025-04-28 21:21:34,740 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,740 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1104144024]
[2025-04-28 21:21:34,740 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:34,741 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,758 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 39 statements into 3 equivalence classes.
[2025-04-28 21:21:34,811 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:34,811 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:34,811 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,252 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 14 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:36,253 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,253 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1104144024]
[2025-04-28 21:21:36,253 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1104144024] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,253 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [905234771]
[2025-04-28 21:21:36,253 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:36,253 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,255 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,257 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:36,281 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,412 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 39 statements into 3 equivalence classes.
[2025-04-28 21:21:36,456 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:36,456 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:36,456 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,461 INFO  L256         TraceCheckSpWp]: Trace formula consists of 287 conjuncts, 119 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,467 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,554 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 12 treesize of output 11
[2025-04-28 21:21:36,686 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 12 treesize of output 1
[2025-04-28 21:21:36,689 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 12 treesize of output 11
[2025-04-28 21:21:36,795 INFO  L325             Elim1Store]: treesize reduction 16, result has 36.0 percent of original size
[2025-04-28 21:21:36,795 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 22 treesize of output 15
[2025-04-28 21:21:36,814 INFO  L325             Elim1Store]: treesize reduction 16, result has 36.0 percent of original size
[2025-04-28 21:21:36,814 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 19
[2025-04-28 21:21:36,932 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 19 treesize of output 15
[2025-04-28 21:21:37,002 INFO  L325             Elim1Store]: treesize reduction 19, result has 20.8 percent of original size
[2025-04-28 21:21:37,002 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 24 treesize of output 15
[2025-04-28 21:21:37,082 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 14 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:37,082 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,364 INFO  L325             Elim1Store]: treesize reduction 20, result has 28.6 percent of original size
[2025-04-28 21:21:45,364 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 18 treesize of output 8
[2025-04-28 21:21:45,372 INFO  L172   IndexEqualityManager]: detected equality via solver
[2025-04-28 21:21:45,374 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 20 treesize of output 1
[2025-04-28 21:21:47,556 INFO  L172   IndexEqualityManager]: detected equality via solver
[2025-04-28 21:21:47,563 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:21:47,565 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 1 case distinctions, treesize of input 14 treesize of output 8
[2025-04-28 21:21:47,572 INFO  L172   IndexEqualityManager]: detected equality via solver
[2025-04-28 21:21:47,574 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 14 treesize of output 1
