./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-095.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:13,006 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:13,092 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5a4fabf5-179f-4fa6-81f5-ad1e855770fb/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:13,102 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:13,102 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:13,129 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:13,129 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:13,129 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:13,130 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:13,130 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:13,130 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:13,131 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:13,131 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:13,131 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:13,131 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:13,131 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:13,132 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:13,132 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:13,132 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:13,132 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:13,132 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:13,132 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:13,133 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:13,133 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:13,133 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:13,134 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:13,134 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:13,514 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:13,529 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:13,532 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:13,533 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:13,534 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:13,537 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5a4fabf5-179f-4fa6-81f5-ad1e855770fb/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-095.smt2
[2025-04-28 21:21:13,541 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:13,547 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:14,101 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5a4fabf5-179f-4fa6-81f5-ad1e855770fb/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-095.smt2
[2025-04-28 21:21:14,105 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:14,109 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:14,110 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:14,110 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:14,110 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:14,118 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,173 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14 Unit
[2025-04-28 21:21:14,176 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:14,177 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,178 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:14,178 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:14,196 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,196 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,234 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,234 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,246 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,248 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,253 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,257 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,259 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,275 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,276 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:14,276 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:14,276 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:14,278 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,282 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:14,302 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:14,321 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:14,326 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:14,342 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:14,343 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:14,343 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:14,343 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Start given in one single declaration
[2025-04-28 21:21:14,343 INFO  L130     BoogieDeclarations]: Found specification of procedure Start
[2025-04-28 21:21:14,343 INFO  L138     BoogieDeclarations]: Found implementation of procedure Start
[2025-04-28 21:21:14,343 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure NT7 given in one single declaration
[2025-04-28 21:21:14,343 INFO  L130     BoogieDeclarations]: Found specification of procedure NT7
[2025-04-28 21:21:14,344 INFO  L138     BoogieDeclarations]: Found implementation of procedure NT7
[2025-04-28 21:21:14,344 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure NT10 given in one single declaration
[2025-04-28 21:21:14,344 INFO  L130     BoogieDeclarations]: Found specification of procedure NT10
[2025-04-28 21:21:14,344 INFO  L138     BoogieDeclarations]: Found implementation of procedure NT10
[2025-04-28 21:21:14,345 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure NT6 given in one single declaration
[2025-04-28 21:21:14,345 INFO  L130     BoogieDeclarations]: Found specification of procedure NT6
[2025-04-28 21:21:14,345 INFO  L138     BoogieDeclarations]: Found implementation of procedure NT6
[2025-04-28 21:21:14,345 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure NT8 given in one single declaration
[2025-04-28 21:21:14,345 INFO  L130     BoogieDeclarations]: Found specification of procedure NT8
[2025-04-28 21:21:14,345 INFO  L138     BoogieDeclarations]: Found implementation of procedure NT8
[2025-04-28 21:21:14,345 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure NT3 given in one single declaration
[2025-04-28 21:21:14,346 INFO  L130     BoogieDeclarations]: Found specification of procedure NT3
[2025-04-28 21:21:14,346 INFO  L138     BoogieDeclarations]: Found implementation of procedure NT3
[2025-04-28 21:21:14,347 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure NT2 given in one single declaration
[2025-04-28 21:21:14,347 INFO  L130     BoogieDeclarations]: Found specification of procedure NT2
[2025-04-28 21:21:14,347 INFO  L138     BoogieDeclarations]: Found implementation of procedure NT2
[2025-04-28 21:21:14,347 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure NT4 given in one single declaration
[2025-04-28 21:21:14,347 INFO  L130     BoogieDeclarations]: Found specification of procedure NT4
[2025-04-28 21:21:14,347 INFO  L138     BoogieDeclarations]: Found implementation of procedure NT4
[2025-04-28 21:21:14,347 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure NT5 given in one single declaration
[2025-04-28 21:21:14,347 INFO  L130     BoogieDeclarations]: Found specification of procedure NT5
[2025-04-28 21:21:14,347 INFO  L138     BoogieDeclarations]: Found implementation of procedure NT5
[2025-04-28 21:21:14,347 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure NT1 given in one single declaration
[2025-04-28 21:21:14,348 INFO  L130     BoogieDeclarations]: Found specification of procedure NT1
[2025-04-28 21:21:14,348 INFO  L138     BoogieDeclarations]: Found implementation of procedure NT1
[2025-04-28 21:21:14,348 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:14,348 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:14,348 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:14,453 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:14,455 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:15,066 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:15,066 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:15,096 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:15,096 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:15,096 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:15 BoogieIcfgContainer
[2025-04-28 21:21:15,097 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:15,099 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:15,100 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:15,105 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:15,105 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:14" (1/3) ...
[2025-04-28 21:21:15,106 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6cd748a2 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:15, skipping insertion in model container
[2025-04-28 21:21:15,107 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (2/3) ...
[2025-04-28 21:21:15,107 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6cd748a2 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:15, skipping insertion in model container
[2025-04-28 21:21:15,107 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:15" (3/3) ...
[2025-04-28 21:21:15,113 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:15,132 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:15,135 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 12 procedures, 155 locations, 426 edges, 12 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:15,192 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:15,204 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;@c0d155d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:15,205 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:15,209 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 155 states, 24 states have (on average 3.0) internal successors, (72), 68 states have internal predecessors, (72), 118 states have call successors, (118), 11 states have call predecessors, (118), 11 states have return successors, (118), 77 states have call predecessors, (118), 118 states have call successors, (118)
[2025-04-28 21:21:15,233 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:15,233 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,234 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,235 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,241 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,242 INFO  L85        PathProgramCache]: Analyzing trace with hash -436056213, now seen corresponding path program 1 times
[2025-04-28 21:21:15,252 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,253 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1425731035]
[2025-04-28 21:21:15,254 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,254 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,281 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:15,299 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:15,300 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,300 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,412 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:15,413 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,413 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1425731035]
[2025-04-28 21:21:15,414 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1425731035] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:15,415 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:15,419 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:15,421 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [514798093]
[2025-04-28 21:21:15,423 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:15,427 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:15,428 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:15,465 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:15,466 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:15,470 INFO  L87              Difference]: Start difference. First operand  has 155 states, 24 states have (on average 3.0) internal successors, (72), 68 states have internal predecessors, (72), 118 states have call successors, (118), 11 states have call predecessors, (118), 11 states have return successors, (118), 77 states have call predecessors, (118), 118 states have call successors, (118) Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:15,631 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:15,632 INFO  L93              Difference]: Finished difference Result 155 states and 307 transitions.
[2025-04-28 21:21:15,634 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:15,636 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:15,636 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:15,655 INFO  L225             Difference]: With dead ends: 155
[2025-04-28 21:21:15,655 INFO  L226             Difference]: Without dead ends: 153
[2025-04-28 21:21:15,658 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:15,661 INFO  L437           NwaCegarLoop]: 306 mSDtfsCounter, 1 mSDsluCounter, 588 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 894 SdHoareTripleChecker+Invalid, 20 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:15,663 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 894 Invalid, 20 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:15,729 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-04-28 21:21:15,809 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 153.
[2025-04-28 21:21:15,812 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 153 states, 23 states have (on average 2.9130434782608696) internal successors, (67), 66 states have internal predecessors, (67), 118 states have call successors, (118), 11 states have call predecessors, (118), 11 states have return successors, (118), 77 states have call predecessors, (118), 118 states have call successors, (118)
[2025-04-28 21:21:15,827 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 153 states to 153 states and 303 transitions.
[2025-04-28 21:21:15,829 INFO  L79                 Accepts]: Start accepts. Automaton has 153 states and 303 transitions. Word has length 9
[2025-04-28 21:21:15,830 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:15,831 INFO  L485      AbstractCegarLoop]: Abstraction has 153 states and 303 transitions.
[2025-04-28 21:21:15,831 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:15,831 INFO  L278                IsEmpty]: Start isEmpty. Operand 153 states and 303 transitions.
[2025-04-28 21:21:15,838 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:15,840 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,840 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,841 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:15,841 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,842 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,842 INFO  L85        PathProgramCache]: Analyzing trace with hash -1523963951, now seen corresponding path program 1 times
[2025-04-28 21:21:15,843 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,843 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2072706805]
[2025-04-28 21:21:15,844 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,844 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,853 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:15,860 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:15,862 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,862 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,961 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:15,961 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,961 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2072706805]
[2025-04-28 21:21:15,961 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2072706805] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:15,961 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:15,962 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:15,962 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1663152946]
[2025-04-28 21:21:15,962 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:15,964 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:15,965 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:15,965 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:15,965 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:15,966 INFO  L87              Difference]: Start difference. First operand 153 states and 303 transitions. Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:16,060 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,062 INFO  L93              Difference]: Finished difference Result 155 states and 304 transitions.
[2025-04-28 21:21:16,063 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:16,063 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:16,064 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,071 INFO  L225             Difference]: With dead ends: 155
[2025-04-28 21:21:16,071 INFO  L226             Difference]: Without dead ends: 153
[2025-04-28 21:21:16,071 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:16,072 INFO  L437           NwaCegarLoop]: 303 mSDtfsCounter, 1 mSDsluCounter, 585 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 888 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,073 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 888 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:16,074 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-04-28 21:21:16,098 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 153.
[2025-04-28 21:21:16,099 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 153 states, 23 states have (on average 2.869565217391304) internal successors, (66), 65 states have internal predecessors, (66), 118 states have call successors, (118), 11 states have call predecessors, (118), 11 states have return successors, (118), 77 states have call predecessors, (118), 118 states have call successors, (118)
[2025-04-28 21:21:16,104 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 153 states to 153 states and 302 transitions.
[2025-04-28 21:21:16,104 INFO  L79                 Accepts]: Start accepts. Automaton has 153 states and 302 transitions. Word has length 9
[2025-04-28 21:21:16,104 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,104 INFO  L485      AbstractCegarLoop]: Abstraction has 153 states and 302 transitions.
[2025-04-28 21:21:16,105 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:16,105 INFO  L278                IsEmpty]: Start isEmpty. Operand 153 states and 302 transitions.
[2025-04-28 21:21:16,108 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:16,108 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,109 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,109 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:16,109 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,109 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,110 INFO  L85        PathProgramCache]: Analyzing trace with hash 187142249, now seen corresponding path program 1 times
[2025-04-28 21:21:16,110 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,110 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [313261609]
[2025-04-28 21:21:16,110 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,110 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,123 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:16,139 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:16,140 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,141 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,272 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:16,272 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,272 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [313261609]
[2025-04-28 21:21:16,272 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [313261609] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,272 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,272 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:16,272 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1727684544]
[2025-04-28 21:21:16,273 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,273 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:16,273 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,274 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:16,274 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:16,274 INFO  L87              Difference]: Start difference. First operand 153 states and 302 transitions. Second operand  has 7 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 4 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:16,917 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,917 INFO  L93              Difference]: Finished difference Result 163 states and 356 transitions.
[2025-04-28 21:21:16,918 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:16,918 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 4 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4) Word has length 17
[2025-04-28 21:21:16,919 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,922 INFO  L225             Difference]: With dead ends: 163
[2025-04-28 21:21:16,922 INFO  L226             Difference]: Without dead ends: 161
[2025-04-28 21:21:16,922 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:16,923 INFO  L437           NwaCegarLoop]: 259 mSDtfsCounter, 4 mSDsluCounter, 1170 mSDsCounter, 0 mSdLazyCounter, 371 mSolverCounterSat, 14 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 1429 SdHoareTripleChecker+Invalid, 385 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 14 IncrementalHoareTripleChecker+Valid, 371 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,923 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 1429 Invalid, 385 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [14 Valid, 371 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:16,924 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 161 states.
[2025-04-28 21:21:16,966 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 161 to 156.
[2025-04-28 21:21:16,967 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 156 states, 24 states have (on average 2.7916666666666665) internal successors, (67), 67 states have internal predecessors, (67), 119 states have call successors, (119), 11 states have call predecessors, (119), 12 states have return successors, (162), 78 states have call predecessors, (162), 119 states have call successors, (162)
[2025-04-28 21:21:16,971 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 156 states to 156 states and 348 transitions.
[2025-04-28 21:21:16,971 INFO  L79                 Accepts]: Start accepts. Automaton has 156 states and 348 transitions. Word has length 17
[2025-04-28 21:21:16,971 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,972 INFO  L485      AbstractCegarLoop]: Abstraction has 156 states and 348 transitions.
[2025-04-28 21:21:16,972 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 4 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:16,972 INFO  L278                IsEmpty]: Start isEmpty. Operand 156 states and 348 transitions.
[2025-04-28 21:21:16,975 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:16,975 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,975 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,975 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:16,975 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,976 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,976 INFO  L85        PathProgramCache]: Analyzing trace with hash 1244723041, now seen corresponding path program 1 times
[2025-04-28 21:21:16,976 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,976 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2081686662]
[2025-04-28 21:21:16,976 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,977 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,981 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:16,987 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:16,987 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,988 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,120 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:17,120 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,121 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2081686662]
[2025-04-28 21:21:17,121 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2081686662] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:17,121 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [784308333]
[2025-04-28 21:21:17,121 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,121 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:17,124 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:17,128 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:17,130 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:17,174 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:17,186 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:17,186 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,186 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,188 INFO  L256         TraceCheckSpWp]: Trace formula consists of 62 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:17,197 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:17,385 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:17,386 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:17,386 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [784308333] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,386 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:17,386 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [8] total 14
[2025-04-28 21:21:17,387 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [434085228]
[2025-04-28 21:21:17,387 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,387 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:17,387 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,388 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:17,389 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=27, Invalid=155, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:17,389 INFO  L87              Difference]: Start difference. First operand 156 states and 348 transitions. Second operand  has 8 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:18,221 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,221 INFO  L93              Difference]: Finished difference Result 166 states and 404 transitions.
[2025-04-28 21:21:18,222 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:18,222 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4) Word has length 17
[2025-04-28 21:21:18,222 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,227 INFO  L225             Difference]: With dead ends: 166
[2025-04-28 21:21:18,227 INFO  L226             Difference]: Without dead ends: 164
[2025-04-28 21:21:18,227 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 26 GetRequests, 12 SyntacticMatches, 0 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=37, Invalid=203, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:18,228 INFO  L437           NwaCegarLoop]: 260 mSDtfsCounter, 4 mSDsluCounter, 1174 mSDsCounter, 0 mSdLazyCounter, 609 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 27 SdHoareTripleChecker+Valid, 1434 SdHoareTripleChecker+Invalid, 625 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 609 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,230 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [27 Valid, 1434 Invalid, 625 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 609 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:18,231 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 164 states.
[2025-04-28 21:21:18,299 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 164 to 159.
[2025-04-28 21:21:18,301 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 159 states, 25 states have (on average 2.72) internal successors, (68), 68 states have internal predecessors, (68), 120 states have call successors, (120), 11 states have call predecessors, (120), 13 states have return successors, (207), 79 states have call predecessors, (207), 120 states have call successors, (207)
[2025-04-28 21:21:18,306 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 159 states to 159 states and 395 transitions.
[2025-04-28 21:21:18,306 INFO  L79                 Accepts]: Start accepts. Automaton has 159 states and 395 transitions. Word has length 17
[2025-04-28 21:21:18,307 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,307 INFO  L485      AbstractCegarLoop]: Abstraction has 159 states and 395 transitions.
[2025-04-28 21:21:18,308 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:18,308 INFO  L278                IsEmpty]: Start isEmpty. Operand 159 states and 395 transitions.
[2025-04-28 21:21:18,314 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:18,315 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,315 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,320 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:18,519 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:18,520 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,520 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,520 INFO  L85        PathProgramCache]: Analyzing trace with hash 1219804001, now seen corresponding path program 2 times
[2025-04-28 21:21:18,520 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,520 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [372569030]
[2025-04-28 21:21:18,520 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:18,520 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,532 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:18,538 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:18,538 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:18,538 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,646 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:18,646 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,646 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [372569030]
[2025-04-28 21:21:18,646 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [372569030] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,646 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,646 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:18,647 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1896334006]
[2025-04-28 21:21:18,647 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,647 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:18,647 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,648 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:18,648 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:18,648 INFO  L87              Difference]: Start difference. First operand 159 states and 395 transitions. Second operand  has 8 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:19,127 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,127 INFO  L93              Difference]: Finished difference Result 166 states and 402 transitions.
[2025-04-28 21:21:19,127 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:19,127 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4) Word has length 17
[2025-04-28 21:21:19,128 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,130 INFO  L225             Difference]: With dead ends: 166
[2025-04-28 21:21:19,131 INFO  L226             Difference]: Without dead ends: 164
[2025-04-28 21:21:19,131 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=24, Invalid=66, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:19,132 INFO  L437           NwaCegarLoop]: 258 mSDtfsCounter, 6 mSDsluCounter, 1169 mSDsCounter, 0 mSdLazyCounter, 363 mSolverCounterSat, 20 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 1427 SdHoareTripleChecker+Invalid, 383 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 20 IncrementalHoareTripleChecker+Valid, 363 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,132 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 1427 Invalid, 383 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [20 Valid, 363 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:19,133 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 164 states.
[2025-04-28 21:21:19,165 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 164 to 156.
[2025-04-28 21:21:19,166 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 156 states, 24 states have (on average 2.7916666666666665) internal successors, (67), 66 states have internal predecessors, (67), 119 states have call successors, (119), 11 states have call predecessors, (119), 12 states have return successors, (162), 78 states have call predecessors, (162), 119 states have call successors, (162)
[2025-04-28 21:21:19,169 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 156 states to 156 states and 348 transitions.
[2025-04-28 21:21:19,169 INFO  L79                 Accepts]: Start accepts. Automaton has 156 states and 348 transitions. Word has length 17
[2025-04-28 21:21:19,169 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,169 INFO  L485      AbstractCegarLoop]: Abstraction has 156 states and 348 transitions.
[2025-04-28 21:21:19,170 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:19,170 INFO  L278                IsEmpty]: Start isEmpty. Operand 156 states and 348 transitions.
[2025-04-28 21:21:19,172 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:19,173 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,173 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,173 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:19,173 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,173 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,175 INFO  L85        PathProgramCache]: Analyzing trace with hash 1715234999, now seen corresponding path program 1 times
[2025-04-28 21:21:19,175 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,175 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [438060995]
[2025-04-28 21:21:19,175 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,175 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,183 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:19,194 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:19,198 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,198 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,389 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:19,389 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,389 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [438060995]
[2025-04-28 21:21:19,390 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [438060995] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:19,390 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:19,390 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:19,390 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [249387416]
[2025-04-28 21:21:19,390 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,391 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:19,391 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,392 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:19,392 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:19,392 INFO  L87              Difference]: Start difference. First operand 156 states and 348 transitions. Second operand  has 9 states, 4 states have (on average 2.0) internal successors, (8), 6 states have internal predecessors, (8), 6 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 5 states have call predecessors, (6), 6 states have call successors, (6)
[2025-04-28 21:21:20,711 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,711 INFO  L93              Difference]: Finished difference Result 172 states and 505 transitions.
[2025-04-28 21:21:20,711 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:20,712 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 4 states have (on average 2.0) internal successors, (8), 6 states have internal predecessors, (8), 6 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 5 states have call predecessors, (6), 6 states have call successors, (6) Word has length 25
[2025-04-28 21:21:20,712 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,716 INFO  L225             Difference]: With dead ends: 172
[2025-04-28 21:21:20,716 INFO  L226             Difference]: Without dead ends: 170
[2025-04-28 21:21:20,716 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 16 GetRequests, 5 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=35, Invalid=121, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:20,717 INFO  L437           NwaCegarLoop]: 259 mSDtfsCounter, 9 mSDsluCounter, 1591 mSDsCounter, 0 mSdLazyCounter, 1157 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 38 SdHoareTripleChecker+Valid, 1850 SdHoareTripleChecker+Invalid, 1183 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 1157 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,717 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [38 Valid, 1850 Invalid, 1183 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 1157 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-04-28 21:21:20,718 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 170 states.
[2025-04-28 21:21:20,787 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 170 to 163.
[2025-04-28 21:21:20,789 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 163 states, 26 states have (on average 2.6538461538461537) internal successors, (69), 69 states have internal predecessors, (69), 122 states have call successors, (122), 11 states have call predecessors, (122), 14 states have return successors, (256), 82 states have call predecessors, (256), 122 states have call successors, (256)
[2025-04-28 21:21:20,791 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 163 states to 163 states and 447 transitions.
[2025-04-28 21:21:20,792 INFO  L79                 Accepts]: Start accepts. Automaton has 163 states and 447 transitions. Word has length 25
[2025-04-28 21:21:20,792 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,792 INFO  L485      AbstractCegarLoop]: Abstraction has 163 states and 447 transitions.
[2025-04-28 21:21:20,792 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 4 states have (on average 2.0) internal successors, (8), 6 states have internal predecessors, (8), 6 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 5 states have call predecessors, (6), 6 states have call successors, (6)
[2025-04-28 21:21:20,793 INFO  L278                IsEmpty]: Start isEmpty. Operand 163 states and 447 transitions.
[2025-04-28 21:21:20,796 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:20,796 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,797 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,797 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:20,797 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,798 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,798 INFO  L85        PathProgramCache]: Analyzing trace with hash -1555358801, now seen corresponding path program 1 times
[2025-04-28 21:21:20,798 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,798 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [84334816]
[2025-04-28 21:21:20,798 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,799 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,807 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:20,817 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:20,817 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,817 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,007 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:21,007 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,007 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [84334816]
[2025-04-28 21:21:21,007 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [84334816] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,007 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,007 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:21,008 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [866488464]
[2025-04-28 21:21:21,008 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,008 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:21,008 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,009 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:21,009 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:21,009 INFO  L87              Difference]: Start difference. First operand 163 states and 447 transitions. Second operand  has 10 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 5 states have call predecessors, (6), 6 states have call successors, (6)
[2025-04-28 21:21:22,494 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:22,494 INFO  L93              Difference]: Finished difference Result 175 states and 557 transitions.
[2025-04-28 21:21:22,495 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:22,495 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 5 states have call predecessors, (6), 6 states have call successors, (6) Word has length 25
[2025-04-28 21:21:22,495 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:22,500 INFO  L225             Difference]: With dead ends: 175
[2025-04-28 21:21:22,500 INFO  L226             Difference]: Without dead ends: 173
[2025-04-28 21:21:22,501 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 17 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 12 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=46, Invalid=164, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:22,501 INFO  L437           NwaCegarLoop]: 260 mSDtfsCounter, 10 mSDsluCounter, 1810 mSDsCounter, 0 mSdLazyCounter, 1424 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 45 SdHoareTripleChecker+Valid, 2070 SdHoareTripleChecker+Invalid, 1452 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 1424 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:22,502 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [45 Valid, 2070 Invalid, 1452 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 1424 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:22,502 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 173 states.
[2025-04-28 21:21:22,569 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 173 to 164.
[2025-04-28 21:21:22,570 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 164 states, 27 states have (on average 2.5925925925925926) internal successors, (70), 70 states have internal predecessors, (70), 121 states have call successors, (121), 11 states have call predecessors, (121), 15 states have return successors, (300), 82 states have call predecessors, (300), 121 states have call successors, (300)
[2025-04-28 21:21:22,573 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 164 states to 164 states and 491 transitions.
[2025-04-28 21:21:22,573 INFO  L79                 Accepts]: Start accepts. Automaton has 164 states and 491 transitions. Word has length 25
[2025-04-28 21:21:22,574 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:22,574 INFO  L485      AbstractCegarLoop]: Abstraction has 164 states and 491 transitions.
[2025-04-28 21:21:22,574 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 5 states have call predecessors, (6), 6 states have call successors, (6)
[2025-04-28 21:21:22,574 INFO  L278                IsEmpty]: Start isEmpty. Operand 164 states and 491 transitions.
[2025-04-28 21:21:22,578 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:22,578 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,579 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:22,579 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:22,579 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,579 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,580 INFO  L85        PathProgramCache]: Analyzing trace with hash 143126959, now seen corresponding path program 2 times
[2025-04-28 21:21:22,580 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,580 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [498749639]
[2025-04-28 21:21:22,580 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:22,581 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,589 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:22,601 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:22,602 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:22,602 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,793 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:22,793 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,793 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [498749639]
[2025-04-28 21:21:22,793 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [498749639] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:22,793 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [125655342]
[2025-04-28 21:21:22,794 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:22,794 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,797 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,800 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:22,804 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:22,849 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:22,864 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:22,864 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:22,865 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,866 INFO  L256         TraceCheckSpWp]: Trace formula consists of 94 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:22,867 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:23,084 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:23,084 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:24,008 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:24,008 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [125655342] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:24,008 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:24,009 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 23
[2025-04-28 21:21:24,009 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2100251832]
[2025-04-28 21:21:24,009 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:24,009 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:24,009 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:24,010 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:24,010 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=60, Invalid=446, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:24,010 INFO  L87              Difference]: Start difference. First operand 164 states and 491 transitions. Second operand  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:26,493 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,493 INFO  L93              Difference]: Finished difference Result 175 states and 554 transitions.
[2025-04-28 21:21:26,494 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:26,494 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16) Word has length 25
[2025-04-28 21:21:26,494 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,502 INFO  L225             Difference]: With dead ends: 175
[2025-04-28 21:21:26,503 INFO  L226             Difference]: Without dead ends: 173
[2025-04-28 21:21:26,504 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 71 GetRequests, 35 SyntacticMatches, 5 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 83 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=150, Invalid=906, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:26,505 INFO  L437           NwaCegarLoop]: 261 mSDtfsCounter, 19 mSDsluCounter, 3412 mSDsCounter, 0 mSdLazyCounter, 2509 mSolverCounterSat, 146 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 3673 SdHoareTripleChecker+Invalid, 2655 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 146 IncrementalHoareTripleChecker+Valid, 2509 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,506 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 3673 Invalid, 2655 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [146 Valid, 2509 Invalid, 0 Unknown, 0 Unchecked, 2.2s Time]
[2025-04-28 21:21:26,506 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 173 states.
[2025-04-28 21:21:26,551 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 173 to 163.
[2025-04-28 21:21:26,552 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 163 states, 26 states have (on average 2.6538461538461537) internal successors, (69), 69 states have internal predecessors, (69), 122 states have call successors, (122), 11 states have call predecessors, (122), 14 states have return successors, (257), 83 states have call predecessors, (257), 122 states have call successors, (257)
[2025-04-28 21:21:26,554 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 163 states to 163 states and 448 transitions.
[2025-04-28 21:21:26,555 INFO  L79                 Accepts]: Start accepts. Automaton has 163 states and 448 transitions. Word has length 25
[2025-04-28 21:21:26,555 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,555 INFO  L485      AbstractCegarLoop]: Abstraction has 163 states and 448 transitions.
[2025-04-28 21:21:26,555 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:26,555 INFO  L278                IsEmpty]: Start isEmpty. Operand 163 states and 448 transitions.
[2025-04-28 21:21:26,558 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:26,558 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,558 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,563 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:26,762 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:26,763 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,763 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,763 INFO  L85        PathProgramCache]: Analyzing trace with hash 1167500455, now seen corresponding path program 3 times
[2025-04-28 21:21:26,763 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,763 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1629826602]
[2025-04-28 21:21:26,763 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:26,763 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,768 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 25 statements into 4 equivalence classes.
[2025-04-28 21:21:26,775 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:26,775 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:26,775 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,914 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:26,914 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,914 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1629826602]
[2025-04-28 21:21:26,914 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1629826602] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:26,915 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1703289980]
[2025-04-28 21:21:26,915 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:26,915 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:26,918 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:26,920 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:26,923 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:26,981 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 25 statements into 4 equivalence classes.
[2025-04-28 21:21:26,998 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:26,998 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:26,998 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,999 INFO  L256         TraceCheckSpWp]: Trace formula consists of 94 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:27,001 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,202 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:27,202 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:28,010 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:28,010 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1703289980] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:28,010 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:28,011 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 23
[2025-04-28 21:21:28,011 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [689261945]
[2025-04-28 21:21:28,011 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,011 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:28,011 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,012 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:28,012 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=448, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:28,012 INFO  L87              Difference]: Start difference. First operand 163 states and 448 transitions. Second operand  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:32,730 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,730 INFO  L93              Difference]: Finished difference Result 208 states and 725 transitions.
[2025-04-28 21:21:32,731 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 23 states. 
[2025-04-28 21:21:32,731 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16) Word has length 25
[2025-04-28 21:21:32,731 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,735 INFO  L225             Difference]: With dead ends: 208
[2025-04-28 21:21:32,736 INFO  L226             Difference]: Without dead ends: 202
[2025-04-28 21:21:32,736 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 80 GetRequests, 35 SyntacticMatches, 5 SemanticMatches, 40 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 198 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=256, Invalid=1466, Unknown=0, NotChecked=0, Total=1722
[2025-04-28 21:21:32,737 INFO  L437           NwaCegarLoop]: 279 mSDtfsCounter, 21 mSDsluCounter, 4341 mSDsCounter, 0 mSdLazyCounter, 5417 mSolverCounterSat, 168 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 3.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 46 SdHoareTripleChecker+Valid, 4620 SdHoareTripleChecker+Invalid, 5585 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 168 IncrementalHoareTripleChecker+Valid, 5417 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 4.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,737 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [46 Valid, 4620 Invalid, 5585 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [168 Valid, 5417 Invalid, 0 Unknown, 0 Unchecked, 4.1s Time]
[2025-04-28 21:21:32,738 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 202 states.
[2025-04-28 21:21:32,809 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 202 to 163.
[2025-04-28 21:21:32,811 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 163 states, 26 states have (on average 2.6538461538461537) internal successors, (69), 69 states have internal predecessors, (69), 122 states have call successors, (122), 11 states have call predecessors, (122), 14 states have return successors, (256), 84 states have call predecessors, (256), 122 states have call successors, (256)
[2025-04-28 21:21:32,814 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 163 states to 163 states and 447 transitions.
[2025-04-28 21:21:32,814 INFO  L79                 Accepts]: Start accepts. Automaton has 163 states and 447 transitions. Word has length 25
[2025-04-28 21:21:32,815 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,815 INFO  L485      AbstractCegarLoop]: Abstraction has 163 states and 447 transitions.
[2025-04-28 21:21:32,815 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:32,815 INFO  L278                IsEmpty]: Start isEmpty. Operand 163 states and 447 transitions.
[2025-04-28 21:21:32,818 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:32,819 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,819 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,824 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:33,020 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,020 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,025 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,025 INFO  L85        PathProgramCache]: Analyzing trace with hash 1965733295, now seen corresponding path program 4 times
[2025-04-28 21:21:33,025 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,025 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [998671671]
[2025-04-28 21:21:33,025 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:33,025 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,030 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:33,038 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:33,038 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:33,038 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,190 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 6 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:33,190 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,190 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [998671671]
[2025-04-28 21:21:33,191 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [998671671] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,191 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1546780995]
[2025-04-28 21:21:33,191 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:33,191 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,193 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,195 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:33,198 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,247 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:33,261 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:33,261 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:33,261 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,262 INFO  L256         TraceCheckSpWp]: Trace formula consists of 94 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,263 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,435 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 6 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:33,435 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:34,275 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 6 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:34,275 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1546780995] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:34,275 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:34,275 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 23
[2025-04-28 21:21:34,275 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1638983820]
[2025-04-28 21:21:34,276 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,276 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:34,276 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,277 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:34,277 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=61, Invalid=445, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:34,277 INFO  L87              Difference]: Start difference. First operand 163 states and 447 transitions. Second operand  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:36,719 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,719 INFO  L93              Difference]: Finished difference Result 189 states and 856 transitions.
[2025-04-28 21:21:36,720 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:36,720 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16) Word has length 25
[2025-04-28 21:21:36,720 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,725 INFO  L225             Difference]: With dead ends: 189
[2025-04-28 21:21:36,725 INFO  L226             Difference]: Without dead ends: 187
[2025-04-28 21:21:36,726 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 70 GetRequests, 35 SyntacticMatches, 5 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 104 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=134, Invalid=858, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:36,727 INFO  L437           NwaCegarLoop]: 260 mSDtfsCounter, 19 mSDsluCounter, 4078 mSDsCounter, 0 mSdLazyCounter, 2914 mSolverCounterSat, 131 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 4338 SdHoareTripleChecker+Invalid, 3045 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 131 IncrementalHoareTripleChecker+Valid, 2914 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,727 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 4338 Invalid, 3045 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [131 Valid, 2914 Invalid, 0 Unknown, 0 Unchecked, 2.1s Time]
[2025-04-28 21:21:36,728 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 187 states.
[2025-04-28 21:21:36,829 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 187 to 171.
[2025-04-28 21:21:36,830 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 171 states, 29 states have (on average 2.4827586206896552) internal successors, (72), 72 states have internal predecessors, (72), 124 states have call successors, (124), 11 states have call predecessors, (124), 17 states have return successors, (401), 87 states have call predecessors, (401), 124 states have call successors, (401)
[2025-04-28 21:21:36,834 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 171 states to 171 states and 597 transitions.
[2025-04-28 21:21:36,834 INFO  L79                 Accepts]: Start accepts. Automaton has 171 states and 597 transitions. Word has length 25
[2025-04-28 21:21:36,834 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,834 INFO  L485      AbstractCegarLoop]: Abstraction has 171 states and 597 transitions.
[2025-04-28 21:21:36,835 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:36,835 INFO  L278                IsEmpty]: Start isEmpty. Operand 171 states and 597 transitions.
[2025-04-28 21:21:36,840 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:36,840 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,840 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,845 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:37,044 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable10
[2025-04-28 21:21:37,045 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,045 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,045 INFO  L85        PathProgramCache]: Analyzing trace with hash -1304860505, now seen corresponding path program 5 times
[2025-04-28 21:21:37,045 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,045 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1405506993]
[2025-04-28 21:21:37,045 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:37,045 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,050 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 25 statements into 4 equivalence classes.
[2025-04-28 21:21:37,056 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:37,056 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s)
[2025-04-28 21:21:37,056 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,213 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:37,213 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,213 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1405506993]
[2025-04-28 21:21:37,214 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1405506993] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,214 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [144476982]
[2025-04-28 21:21:37,214 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:37,214 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,226 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,229 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:37,233 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,287 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 25 statements into 4 equivalence classes.
[2025-04-28 21:21:37,300 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:37,301 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s)
[2025-04-28 21:21:37,301 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,301 INFO  L256         TraceCheckSpWp]: Trace formula consists of 94 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,303 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,469 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:37,469 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,190 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:38,191 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [144476982] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,192 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,192 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 23
[2025-04-28 21:21:38,192 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [23452089]
[2025-04-28 21:21:38,192 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,192 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:38,192 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,193 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:38,193 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=60, Invalid=446, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:38,193 INFO  L87              Difference]: Start difference. First operand 171 states and 597 transitions. Second operand  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:40,370 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,370 INFO  L93              Difference]: Finished difference Result 192 states and 878 transitions.
[2025-04-28 21:21:40,370 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:40,371 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16) Word has length 25
[2025-04-28 21:21:40,371 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,375 INFO  L225             Difference]: With dead ends: 192
[2025-04-28 21:21:40,375 INFO  L226             Difference]: Without dead ends: 190
[2025-04-28 21:21:40,376 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 70 GetRequests, 35 SyntacticMatches, 5 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 93 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=133, Invalid=859, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:40,377 INFO  L437           NwaCegarLoop]: 260 mSDtfsCounter, 24 mSDsluCounter, 3635 mSDsCounter, 0 mSdLazyCounter, 2455 mSolverCounterSat, 146 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 3895 SdHoareTripleChecker+Invalid, 2601 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 146 IncrementalHoareTripleChecker+Valid, 2455 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,377 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 3895 Invalid, 2601 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [146 Valid, 2455 Invalid, 0 Unknown, 0 Unchecked, 1.9s Time]
[2025-04-28 21:21:40,378 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 190 states.
[2025-04-28 21:21:40,485 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 190 to 176.
[2025-04-28 21:21:40,488 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 176 states, 30 states have (on average 2.433333333333333) internal successors, (73), 73 states have internal predecessors, (73), 127 states have call successors, (127), 11 states have call predecessors, (127), 18 states have return successors, (460), 91 states have call predecessors, (460), 127 states have call successors, (460)
[2025-04-28 21:21:40,492 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 176 states to 176 states and 660 transitions.
[2025-04-28 21:21:40,492 INFO  L79                 Accepts]: Start accepts. Automaton has 176 states and 660 transitions. Word has length 25
[2025-04-28 21:21:40,492 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,492 INFO  L485      AbstractCegarLoop]: Abstraction has 176 states and 660 transitions.
[2025-04-28 21:21:40,492 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 16 states have call successors, (16), 1 states have call predecessors, (16), 7 states have return successors, (16), 11 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:40,492 INFO  L278                IsEmpty]: Start isEmpty. Operand 176 states and 660 transitions.
[2025-04-28 21:21:40,496 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:40,496 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,496 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,501 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:40,697 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,697 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,697 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,697 INFO  L85        PathProgramCache]: Analyzing trace with hash 393625255, now seen corresponding path program 6 times
[2025-04-28 21:21:40,697 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,698 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [873769266]
[2025-04-28 21:21:40,698 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:40,698 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,703 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 25 statements into 4 equivalence classes.
[2025-04-28 21:21:40,731 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 4 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:40,732 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 4 check-sat command(s)
[2025-04-28 21:21:40,732 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,884 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:40,885 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,885 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [873769266]
[2025-04-28 21:21:40,885 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [873769266] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,885 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [499622060]
[2025-04-28 21:21:40,885 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:40,885 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,887 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,892 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:40,894 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,957 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 25 statements into 4 equivalence classes.
[2025-04-28 21:21:40,974 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 4 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:40,974 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 4 check-sat command(s)
[2025-04-28 21:21:40,974 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,975 INFO  L256         TraceCheckSpWp]: Trace formula consists of 94 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,976 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,168 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:41,168 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:41,169 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [499622060] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,169 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:41,169 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [11] total 20
[2025-04-28 21:21:41,169 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1317326052]
[2025-04-28 21:21:41,169 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,169 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:41,169 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,170 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:41,170 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=43, Invalid=337, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:41,170 INFO  L87              Difference]: Start difference. First operand 176 states and 660 transitions. Second operand  has 11 states, 6 states have (on average 1.8333333333333333) internal successors, (11), 8 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 5 states have call predecessors, (6), 6 states have call successors, (6)
[2025-04-28 21:21:43,038 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,038 INFO  L93              Difference]: Finished difference Result 197 states and 971 transitions.
[2025-04-28 21:21:43,038 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:43,039 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 6 states have (on average 1.8333333333333333) internal successors, (11), 8 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 5 states have call predecessors, (6), 6 states have call successors, (6) Word has length 25
[2025-04-28 21:21:43,039 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,044 INFO  L225             Difference]: With dead ends: 197
[2025-04-28 21:21:43,045 INFO  L226             Difference]: Without dead ends: 195
[2025-04-28 21:21:43,045 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 41 GetRequests, 18 SyntacticMatches, 0 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=73, Invalid=527, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:43,045 INFO  L437           NwaCegarLoop]: 264 mSDtfsCounter, 7 mSDsluCounter, 2038 mSDsCounter, 0 mSdLazyCounter, 2192 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 2302 SdHoareTripleChecker+Invalid, 2213 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 2192 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,046 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 2302 Invalid, 2213 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 2192 Invalid, 0 Unknown, 0 Unchecked, 1.7s Time]
[2025-04-28 21:21:43,047 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 195 states.
[2025-04-28 21:21:43,180 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 195 to 186.
[2025-04-28 21:21:43,181 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 186 states, 33 states have (on average 2.303030303030303) internal successors, (76), 76 states have internal predecessors, (76), 131 states have call successors, (131), 11 states have call predecessors, (131), 21 states have return successors, (639), 98 states have call predecessors, (639), 131 states have call successors, (639)
[2025-04-28 21:21:43,185 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 186 states to 186 states and 846 transitions.
[2025-04-28 21:21:43,186 INFO  L79                 Accepts]: Start accepts. Automaton has 186 states and 846 transitions. Word has length 25
[2025-04-28 21:21:43,186 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,186 INFO  L485      AbstractCegarLoop]: Abstraction has 186 states and 846 transitions.
[2025-04-28 21:21:43,186 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 6 states have (on average 1.8333333333333333) internal successors, (11), 8 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 5 states have call predecessors, (6), 6 states have call successors, (6)
[2025-04-28 21:21:43,186 INFO  L278                IsEmpty]: Start isEmpty. Operand 186 states and 846 transitions.
[2025-04-28 21:21:43,193 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:43,193 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,193 INFO  L218           NwaCegarLoop]: trace histogram [6, 3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,199 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:43,397 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:43,398 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,399 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,399 INFO  L85        PathProgramCache]: Analyzing trace with hash 652617341, now seen corresponding path program 7 times
[2025-04-28 21:21:43,399 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,399 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1711718961]
[2025-04-28 21:21:43,399 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:43,399 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,403 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:43,407 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:43,407 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,408 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,561 INFO  L134       CoverageAnalysis]: Checked inductivity of 47 backedges. 7 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:43,561 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,561 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1711718961]
[2025-04-28 21:21:43,561 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1711718961] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,561 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [452866370]
[2025-04-28 21:21:43,562 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:43,562 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,564 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,566 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,569 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,628 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:43,644 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:43,644 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,645 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,646 INFO  L256         TraceCheckSpWp]: Trace formula consists of 126 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,647 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,849 INFO  L134       CoverageAnalysis]: Checked inductivity of 47 backedges. 7 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:43,849 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,105 INFO  L134       CoverageAnalysis]: Checked inductivity of 47 backedges. 7 proven. 11 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:45,106 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [452866370] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,106 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,106 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 12] total 27
[2025-04-28 21:21:45,106 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1334782893]
[2025-04-28 21:21:45,106 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,107 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:21:45,107 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,107 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:21:45,107 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=80, Invalid=622, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:45,108 INFO  L87              Difference]: Start difference. First operand 186 states and 846 transitions. Second operand  has 27 states, 8 states have (on average 2.75) internal successors, (22), 17 states have internal predecessors, (22), 20 states have call successors, (20), 1 states have call predecessors, (20), 7 states have return successors, (22), 16 states have call predecessors, (22), 20 states have call successors, (22)
