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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:10,486 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:10,573 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11a0fe3c-52af-4ac9-a3b2-637e8d5ff204/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:10,578 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:10,578 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:10,600 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:10,601 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:10,601 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:10,601 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:10,601 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:10,602 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:10,602 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:10,602 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:10,602 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:10,602 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:10,602 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:10,603 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:10,603 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:10,603 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:10,603 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:10,603 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:10,603 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:10,603 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:10,604 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:10,604 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:10,604 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:10,605 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:10,932 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:10,942 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:10,945 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:10,948 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:10,948 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:10,949 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11a0fe3c-52af-4ac9-a3b2-637e8d5ff204/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-215.smt2
[2025-04-28 21:21:10,952 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:10,955 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:11,330 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11a0fe3c-52af-4ac9-a3b2-637e8d5ff204/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-215.smt2
[2025-04-28 21:21:11,334 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:11,335 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:11,336 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:11,336 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:11,337 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:11,339 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,369 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11 Unit
[2025-04-28 21:21:11,369 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:11,370 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:11,372 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:11,372 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:11,389 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,389 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,429 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,429 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,439 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,442 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,449 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,450 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,451 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,473 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:11,474 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:11,474 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:11,474 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:11,478 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,481 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:11,501 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:11,517 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:11,521 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:11,532 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:11,533 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:11,533 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:11,533 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main114 given in one single declaration
[2025-04-28 21:21:11,533 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main114
[2025-04-28 21:21:11,533 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main114
[2025-04-28 21:21:11,533 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main103 given in one single declaration
[2025-04-28 21:21:11,533 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main103
[2025-04-28 21:21:11,534 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main103
[2025-04-28 21:21:11,534 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main85 given in one single declaration
[2025-04-28 21:21:11,534 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main85
[2025-04-28 21:21:11,534 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main85
[2025-04-28 21:21:11,534 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main73 given in one single declaration
[2025-04-28 21:21:11,534 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main73
[2025-04-28 21:21:11,534 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main73
[2025-04-28 21:21:11,534 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main91 given in one single declaration
[2025-04-28 21:21:11,534 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main91
[2025-04-28 21:21:11,534 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main91
[2025-04-28 21:21:11,534 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main67 given in one single declaration
[2025-04-28 21:21:11,535 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main67
[2025-04-28 21:21:11,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main67
[2025-04-28 21:21:11,535 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main97 given in one single declaration
[2025-04-28 21:21:11,535 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main97
[2025-04-28 21:21:11,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main97
[2025-04-28 21:21:11,535 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main64 given in one single declaration
[2025-04-28 21:21:11,535 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main64
[2025-04-28 21:21:11,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main64
[2025-04-28 21:21:11,535 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main58 given in one single declaration
[2025-04-28 21:21:11,535 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main58
[2025-04-28 21:21:11,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main58
[2025-04-28 21:21:11,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main52 given in one single declaration
[2025-04-28 21:21:11,536 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main52
[2025-04-28 21:21:11,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main52
[2025-04-28 21:21:11,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main46 given in one single declaration
[2025-04-28 21:21:11,536 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main46
[2025-04-28 21:21:11,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main46
[2025-04-28 21:21:11,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main27 given in one single declaration
[2025-04-28 21:21:11,536 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main27
[2025-04-28 21:21:11,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main27
[2025-04-28 21:21:11,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main2 given in one single declaration
[2025-04-28 21:21:11,536 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main2
[2025-04-28 21:21:11,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main2
[2025-04-28 21:21:11,537 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main79 given in one single declaration
[2025-04-28 21:21:11,537 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main79
[2025-04-28 21:21:11,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main79
[2025-04-28 21:21:11,537 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:11,537 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:11,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:11,676 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:11,678 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:12,074 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:12,074 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:12,088 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:12,089 INFO  L312             CfgBuilder]: Removed 3 assume(true) statements.
[2025-04-28 21:21:12,089 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:12 BoogieIcfgContainer
[2025-04-28 21:21:12,090 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:12,093 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:12,093 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:12,097 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:12,097 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:11" (1/3) ...
[2025-04-28 21:21:12,098 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@68156e49 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:12, skipping insertion in model container
[2025-04-28 21:21:12,098 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (2/3) ...
[2025-04-28 21:21:12,098 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@68156e49 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:12, skipping insertion in model container
[2025-04-28 21:21:12,099 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:12" (3/3) ...
[2025-04-28 21:21:12,100 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:12,116 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:12,119 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 16 procedures, 89 locations, 187 edges, 16 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:12,177 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:12,193 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;@6091b032, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:12,194 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:12,205 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 89 states, 30 states have (on average 1.9333333333333333) internal successors, (58), 58 states have internal predecessors, (58), 43 states have call successors, (43), 15 states have call predecessors, (43), 15 states have return successors, (43), 15 states have call predecessors, (43), 43 states have call successors, (43)
[2025-04-28 21:21:12,224 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:12,226 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:12,227 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:12,228 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:12,235 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:12,236 INFO  L85        PathProgramCache]: Analyzing trace with hash -68717116, now seen corresponding path program 1 times
[2025-04-28 21:21:12,244 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:12,246 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1535028744]
[2025-04-28 21:21:12,246 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:12,247 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:12,295 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:12,342 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:12,342 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:12,342 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:12,720 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:12,721 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:12,721 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1535028744]
[2025-04-28 21:21:12,722 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1535028744] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:12,722 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:12,725 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:12,727 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1179588660]
[2025-04-28 21:21:12,728 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:12,732 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:12,732 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:12,767 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:12,767 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:12,770 INFO  L87              Difference]: Start difference. First operand  has 89 states, 30 states have (on average 1.9333333333333333) internal successors, (58), 58 states have internal predecessors, (58), 43 states have call successors, (43), 15 states have call predecessors, (43), 15 states have return successors, (43), 15 states have call predecessors, (43), 43 states have call successors, (43) Second operand  has 7 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 7 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:13,102 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:13,103 INFO  L93              Difference]: Finished difference Result 97 states and 162 transitions.
[2025-04-28 21:21:13,104 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:13,106 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 7 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:13,107 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:13,152 INFO  L225             Difference]: With dead ends: 97
[2025-04-28 21:21:13,153 INFO  L226             Difference]: Without dead ends: 97
[2025-04-28 21:21:13,155 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:13,160 INFO  L437           NwaCegarLoop]: 129 mSDtfsCounter, 1 mSDsluCounter, 632 mSDsCounter, 0 mSdLazyCounter, 96 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 761 SdHoareTripleChecker+Invalid, 106 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 96 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:13,161 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 761 Invalid, 106 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [10 Valid, 96 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:13,185 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 97 states.
[2025-04-28 21:21:13,258 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 97 to 95.
[2025-04-28 21:21:13,260 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 95 states, 33 states have (on average 1.8181818181818181) internal successors, (60), 60 states have internal predecessors, (60), 43 states have call successors, (43), 15 states have call predecessors, (43), 19 states have return successors, (57), 19 states have call predecessors, (57), 43 states have call successors, (57)
[2025-04-28 21:21:13,271 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 95 states to 95 states and 160 transitions.
[2025-04-28 21:21:13,276 INFO  L79                 Accepts]: Start accepts. Automaton has 95 states and 160 transitions. Word has length 30
[2025-04-28 21:21:13,278 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:13,278 INFO  L485      AbstractCegarLoop]: Abstraction has 95 states and 160 transitions.
[2025-04-28 21:21:13,278 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 7 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:13,278 INFO  L278                IsEmpty]: Start isEmpty. Operand 95 states and 160 transitions.
[2025-04-28 21:21:13,286 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:13,286 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:13,286 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:13,287 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:13,287 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:13,290 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:13,291 INFO  L85        PathProgramCache]: Analyzing trace with hash 1143482868, now seen corresponding path program 1 times
[2025-04-28 21:21:13,291 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:13,292 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [550833414]
[2025-04-28 21:21:13,293 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:13,293 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:13,319 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:13,337 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:13,337 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:13,337 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:13,533 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:13,534 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:13,534 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [550833414]
[2025-04-28 21:21:13,534 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [550833414] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:13,534 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:13,534 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:13,534 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1745447786]
[2025-04-28 21:21:13,534 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:13,535 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:13,536 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:13,536 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:13,536 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:13,537 INFO  L87              Difference]: Start difference. First operand 95 states and 160 transitions. Second operand  has 7 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 7 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:13,754 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:13,754 INFO  L93              Difference]: Finished difference Result 95 states and 159 transitions.
[2025-04-28 21:21:13,754 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:13,755 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 7 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:13,755 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:13,757 INFO  L225             Difference]: With dead ends: 95
[2025-04-28 21:21:13,757 INFO  L226             Difference]: Without dead ends: 94
[2025-04-28 21:21:13,758 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:13,762 INFO  L437           NwaCegarLoop]: 145 mSDtfsCounter, 0 mSDsluCounter, 698 mSDsCounter, 0 mSdLazyCounter, 90 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 843 SdHoareTripleChecker+Invalid, 100 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 90 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:13,762 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 843 Invalid, 100 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 90 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:13,763 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-04-28 21:21:13,778 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 86.
[2025-04-28 21:21:13,780 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 86 states, 29 states have (on average 1.896551724137931) internal successors, (55), 55 states have internal predecessors, (55), 42 states have call successors, (42), 15 states have call predecessors, (42), 15 states have return successors, (42), 15 states have call predecessors, (42), 42 states have call successors, (42)
[2025-04-28 21:21:13,783 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 139 transitions.
[2025-04-28 21:21:13,786 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 139 transitions. Word has length 30
[2025-04-28 21:21:13,786 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:13,786 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 139 transitions.
[2025-04-28 21:21:13,786 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 7 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:13,786 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 139 transitions.
[2025-04-28 21:21:13,788 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 35
[2025-04-28 21:21:13,791 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:13,791 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:13,791 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:13,791 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:13,792 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:13,792 INFO  L85        PathProgramCache]: Analyzing trace with hash 1839575069, now seen corresponding path program 1 times
[2025-04-28 21:21:13,792 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:13,792 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [780877585]
[2025-04-28 21:21:13,792 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:13,793 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:13,812 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 34 statements into 1 equivalence classes.
[2025-04-28 21:21:13,827 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 34 of 34 statements.
[2025-04-28 21:21:13,827 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:13,827 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:13,953 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:13,953 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:13,954 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [780877585]
[2025-04-28 21:21:13,954 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [780877585] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:13,954 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:13,954 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:13,954 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [695037430]
[2025-04-28 21:21:13,954 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:13,954 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:13,954 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:13,955 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:13,955 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:13,955 INFO  L87              Difference]: Start difference. First operand 86 states and 139 transitions. Second operand  has 7 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 7 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:14,182 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:14,183 INFO  L93              Difference]: Finished difference Result 96 states and 160 transitions.
[2025-04-28 21:21:14,184 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:14,184 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 7 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9) Word has length 34
[2025-04-28 21:21:14,185 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:14,186 INFO  L225             Difference]: With dead ends: 96
[2025-04-28 21:21:14,187 INFO  L226             Difference]: Without dead ends: 96
[2025-04-28 21:21:14,187 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:14,191 INFO  L437           NwaCegarLoop]: 125 mSDtfsCounter, 1 mSDsluCounter, 610 mSDsCounter, 0 mSdLazyCounter, 104 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 735 SdHoareTripleChecker+Invalid, 114 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 104 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:14,191 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 735 Invalid, 114 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 104 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:14,192 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 96 states.
[2025-04-28 21:21:14,209 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 96 to 94.
[2025-04-28 21:21:14,210 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 33 states have (on average 1.7878787878787878) internal successors, (59), 59 states have internal predecessors, (59), 42 states have call successors, (42), 15 states have call predecessors, (42), 19 states have return successors, (55), 19 states have call predecessors, (55), 42 states have call successors, (55)
[2025-04-28 21:21:14,213 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 156 transitions.
[2025-04-28 21:21:14,213 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 156 transitions. Word has length 34
[2025-04-28 21:21:14,213 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:14,214 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 156 transitions.
[2025-04-28 21:21:14,214 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 7 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:14,214 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 156 transitions.
[2025-04-28 21:21:14,215 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 35
[2025-04-28 21:21:14,216 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,216 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,216 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:14,218 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,220 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,220 INFO  L85        PathProgramCache]: Analyzing trace with hash 1152365730, now seen corresponding path program 1 times
[2025-04-28 21:21:14,220 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,220 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [643480767]
[2025-04-28 21:21:14,221 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,221 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,238 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 34 statements into 1 equivalence classes.
[2025-04-28 21:21:14,244 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 34 of 34 statements.
[2025-04-28 21:21:14,244 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,244 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,396 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:14,396 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,396 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [643480767]
[2025-04-28 21:21:14,397 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [643480767] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:14,397 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:14,397 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:14,397 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [507685069]
[2025-04-28 21:21:14,397 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:14,397 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:14,397 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:14,398 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:14,398 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:14,398 INFO  L87              Difference]: Start difference. First operand 94 states and 156 transitions. Second operand  has 8 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (9), 7 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:14,615 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:14,615 INFO  L93              Difference]: Finished difference Result 114 states and 196 transitions.
[2025-04-28 21:21:14,615 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:14,616 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (9), 7 states have call predecessors, (9), 3 states have call successors, (9) Word has length 34
[2025-04-28 21:21:14,616 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:14,618 INFO  L225             Difference]: With dead ends: 114
[2025-04-28 21:21:14,618 INFO  L226             Difference]: Without dead ends: 114
[2025-04-28 21:21:14,618 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:14,622 INFO  L437           NwaCegarLoop]: 143 mSDtfsCounter, 1 mSDsluCounter, 827 mSDsCounter, 0 mSdLazyCounter, 125 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 970 SdHoareTripleChecker+Invalid, 136 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 125 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:14,623 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 970 Invalid, 136 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 125 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:14,623 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 114 states.
[2025-04-28 21:21:14,642 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 114 to 112.
[2025-04-28 21:21:14,646 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 112 states, 42 states have (on average 1.619047619047619) internal successors, (68), 68 states have internal predecessors, (68), 42 states have call successors, (42), 15 states have call predecessors, (42), 28 states have return successors, (84), 28 states have call predecessors, (84), 42 states have call successors, (84)
[2025-04-28 21:21:14,647 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 112 states to 112 states and 194 transitions.
[2025-04-28 21:21:14,648 INFO  L79                 Accepts]: Start accepts. Automaton has 112 states and 194 transitions. Word has length 34
[2025-04-28 21:21:14,649 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:14,649 INFO  L485      AbstractCegarLoop]: Abstraction has 112 states and 194 transitions.
[2025-04-28 21:21:14,650 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (9), 7 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:14,650 INFO  L278                IsEmpty]: Start isEmpty. Operand 112 states and 194 transitions.
[2025-04-28 21:21:14,652 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 35
[2025-04-28 21:21:14,653 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,653 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,653 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:14,653 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,654 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,654 INFO  L85        PathProgramCache]: Analyzing trace with hash 418344480, now seen corresponding path program 1 times
[2025-04-28 21:21:14,655 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,655 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1763899696]
[2025-04-28 21:21:14,655 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,655 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,670 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 34 statements into 1 equivalence classes.
[2025-04-28 21:21:14,678 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 34 of 34 statements.
[2025-04-28 21:21:14,681 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,681 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,784 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:14,784 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,784 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1763899696]
[2025-04-28 21:21:14,784 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1763899696] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:14,784 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:14,784 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:14,784 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1866836539]
[2025-04-28 21:21:14,784 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:14,785 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:14,785 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:14,785 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:14,786 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:14,786 INFO  L87              Difference]: Start difference. First operand 112 states and 194 transitions. Second operand  has 7 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 7 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:14,964 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:14,964 INFO  L93              Difference]: Finished difference Result 116 states and 199 transitions.
[2025-04-28 21:21:14,965 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:14,965 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 7 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9) Word has length 34
[2025-04-28 21:21:14,965 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:14,967 INFO  L225             Difference]: With dead ends: 116
[2025-04-28 21:21:14,967 INFO  L226             Difference]: Without dead ends: 116
[2025-04-28 21:21:14,967 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:14,968 INFO  L437           NwaCegarLoop]: 141 mSDtfsCounter, 1 mSDsluCounter, 675 mSDsCounter, 0 mSdLazyCounter, 104 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 816 SdHoareTripleChecker+Invalid, 114 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 104 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:14,969 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 816 Invalid, 114 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 104 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:14,970 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 116 states.
[2025-04-28 21:21:14,981 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 116 to 112.
[2025-04-28 21:21:14,982 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 112 states, 42 states have (on average 1.619047619047619) internal successors, (68), 68 states have internal predecessors, (68), 42 states have call successors, (42), 15 states have call predecessors, (42), 28 states have return successors, (82), 28 states have call predecessors, (82), 42 states have call successors, (82)
[2025-04-28 21:21:14,983 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 112 states to 112 states and 192 transitions.
[2025-04-28 21:21:14,984 INFO  L79                 Accepts]: Start accepts. Automaton has 112 states and 192 transitions. Word has length 34
[2025-04-28 21:21:14,984 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:14,984 INFO  L485      AbstractCegarLoop]: Abstraction has 112 states and 192 transitions.
[2025-04-28 21:21:14,984 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 7 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:14,984 INFO  L278                IsEmpty]: Start isEmpty. Operand 112 states and 192 transitions.
[2025-04-28 21:21:14,986 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 35
[2025-04-28 21:21:14,986 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,986 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,986 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:14,987 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,987 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,987 INFO  L85        PathProgramCache]: Analyzing trace with hash -2004038610, now seen corresponding path program 1 times
[2025-04-28 21:21:14,987 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,987 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [473012022]
[2025-04-28 21:21:14,987 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,988 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,004 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 34 statements into 1 equivalence classes.
[2025-04-28 21:21:15,009 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 34 of 34 statements.
[2025-04-28 21:21:15,009 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,009 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,157 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,157 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,157 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [473012022]
[2025-04-28 21:21:15,157 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [473012022] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:15,157 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:15,157 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:15,157 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2062730515]
[2025-04-28 21:21:15,157 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:15,158 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:15,158 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:15,158 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:15,159 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:15,159 INFO  L87              Difference]: Start difference. First operand 112 states and 192 transitions. Second operand  has 8 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (9), 7 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:15,354 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:15,358 INFO  L93              Difference]: Finished difference Result 112 states and 191 transitions.
[2025-04-28 21:21:15,361 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:15,361 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (9), 7 states have call predecessors, (9), 3 states have call successors, (9) Word has length 34
[2025-04-28 21:21:15,362 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:15,363 INFO  L225             Difference]: With dead ends: 112
[2025-04-28 21:21:15,363 INFO  L226             Difference]: Without dead ends: 111
[2025-04-28 21:21:15,363 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:15,364 INFO  L437           NwaCegarLoop]: 123 mSDtfsCounter, 0 mSDsluCounter, 726 mSDsCounter, 0 mSdLazyCounter, 118 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 849 SdHoareTripleChecker+Invalid, 129 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 118 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:15,367 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 849 Invalid, 129 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 118 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:15,368 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 111 states.
[2025-04-28 21:21:15,377 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 111 to 93.
[2025-04-28 21:21:15,377 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 93 states, 33 states have (on average 1.7575757575757576) internal successors, (58), 58 states have internal predecessors, (58), 41 states have call successors, (41), 15 states have call predecessors, (41), 19 states have return successors, (53), 19 states have call predecessors, (53), 41 states have call successors, (53)
[2025-04-28 21:21:15,378 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 93 states to 93 states and 152 transitions.
[2025-04-28 21:21:15,379 INFO  L79                 Accepts]: Start accepts. Automaton has 93 states and 152 transitions. Word has length 34
[2025-04-28 21:21:15,379 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:15,379 INFO  L485      AbstractCegarLoop]: Abstraction has 93 states and 152 transitions.
[2025-04-28 21:21:15,379 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (9), 7 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:15,379 INFO  L278                IsEmpty]: Start isEmpty. Operand 93 states and 152 transitions.
[2025-04-28 21:21:15,381 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 39
[2025-04-28 21:21:15,381 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,381 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,381 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:15,381 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,382 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,382 INFO  L85        PathProgramCache]: Analyzing trace with hash 1087491519, now seen corresponding path program 1 times
[2025-04-28 21:21:15,382 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,382 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1664588573]
[2025-04-28 21:21:15,382 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,382 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,397 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 38 statements into 1 equivalence classes.
[2025-04-28 21:21:15,402 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 38 of 38 statements.
[2025-04-28 21:21:15,402 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,402 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,522 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,522 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,522 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1664588573]
[2025-04-28 21:21:15,522 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1664588573] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:15,523 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:15,523 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:15,523 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [912645933]
[2025-04-28 21:21:15,524 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:15,524 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:15,524 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:15,524 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:15,525 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:15,525 INFO  L87              Difference]: Start difference. First operand 93 states and 152 transitions. Second operand  has 8 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 8 states have internal predecessors, (18), 3 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:15,705 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:15,705 INFO  L93              Difference]: Finished difference Result 111 states and 184 transitions.
[2025-04-28 21:21:15,705 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:15,705 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 8 states have internal predecessors, (18), 3 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10) Word has length 38
[2025-04-28 21:21:15,706 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:15,707 INFO  L225             Difference]: With dead ends: 111
[2025-04-28 21:21:15,707 INFO  L226             Difference]: Without dead ends: 111
[2025-04-28 21:21:15,707 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:15,708 INFO  L437           NwaCegarLoop]: 123 mSDtfsCounter, 1 mSDsluCounter, 728 mSDsCounter, 0 mSdLazyCounter, 109 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 851 SdHoareTripleChecker+Invalid, 118 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 109 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:15,708 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 851 Invalid, 118 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 109 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:15,709 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 111 states.
[2025-04-28 21:21:15,726 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 111 to 109.
[2025-04-28 21:21:15,727 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 109 states, 41 states have (on average 1.6097560975609757) internal successors, (66), 66 states have internal predecessors, (66), 41 states have call successors, (41), 15 states have call predecessors, (41), 27 states have return successors, (75), 27 states have call predecessors, (75), 41 states have call successors, (75)
[2025-04-28 21:21:15,729 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 109 states to 109 states and 182 transitions.
[2025-04-28 21:21:15,730 INFO  L79                 Accepts]: Start accepts. Automaton has 109 states and 182 transitions. Word has length 38
[2025-04-28 21:21:15,730 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:15,731 INFO  L485      AbstractCegarLoop]: Abstraction has 109 states and 182 transitions.
[2025-04-28 21:21:15,731 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 8 states have internal predecessors, (18), 3 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:15,731 INFO  L278                IsEmpty]: Start isEmpty. Operand 109 states and 182 transitions.
[2025-04-28 21:21:15,733 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 39
[2025-04-28 21:21:15,734 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,734 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,735 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:15,735 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,735 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,735 INFO  L85        PathProgramCache]: Analyzing trace with hash -2093869761, now seen corresponding path program 1 times
[2025-04-28 21:21:15,735 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,735 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [353512261]
[2025-04-28 21:21:15,736 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,736 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,749 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 38 statements into 1 equivalence classes.
[2025-04-28 21:21:15,757 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 38 of 38 statements.
[2025-04-28 21:21:15,761 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,761 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,894 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,894 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,894 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [353512261]
[2025-04-28 21:21:15,894 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [353512261] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:15,894 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:15,894 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:15,895 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1291044629]
[2025-04-28 21:21:15,895 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:15,895 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:15,895 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:15,895 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:15,896 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:15,896 INFO  L87              Difference]: Start difference. First operand 109 states and 182 transitions. Second operand  has 8 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 8 states have internal predecessors, (18), 3 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:16,067 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,068 INFO  L93              Difference]: Finished difference Result 109 states and 181 transitions.
[2025-04-28 21:21:16,068 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:16,069 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 8 states have internal predecessors, (18), 3 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10) Word has length 38
[2025-04-28 21:21:16,069 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,070 INFO  L225             Difference]: With dead ends: 109
[2025-04-28 21:21:16,070 INFO  L226             Difference]: Without dead ends: 108
[2025-04-28 21:21:16,070 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:16,071 INFO  L437           NwaCegarLoop]: 123 mSDtfsCounter, 0 mSDsluCounter, 727 mSDsCounter, 0 mSdLazyCounter, 104 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 850 SdHoareTripleChecker+Invalid, 113 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 104 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,071 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 850 Invalid, 113 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 104 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:16,072 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 108 states.
[2025-04-28 21:21:16,087 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 108 to 92.
[2025-04-28 21:21:16,087 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 33 states have (on average 1.7272727272727273) internal successors, (57), 57 states have internal predecessors, (57), 40 states have call successors, (40), 15 states have call predecessors, (40), 19 states have return successors, (52), 19 states have call predecessors, (52), 40 states have call successors, (52)
[2025-04-28 21:21:16,088 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 149 transitions.
[2025-04-28 21:21:16,088 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 149 transitions. Word has length 38
[2025-04-28 21:21:16,089 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,089 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 149 transitions.
[2025-04-28 21:21:16,089 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 8 states have internal predecessors, (18), 3 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:16,089 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 149 transitions.
[2025-04-28 21:21:16,093 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 43
[2025-04-28 21:21:16,093 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,094 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,094 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:16,094 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,094 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,094 INFO  L85        PathProgramCache]: Analyzing trace with hash -1084435753, now seen corresponding path program 1 times
[2025-04-28 21:21:16,094 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,095 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [318019534]
[2025-04-28 21:21:16,095 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,095 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,112 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 42 statements into 1 equivalence classes.
[2025-04-28 21:21:16,115 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 42 of 42 statements.
[2025-04-28 21:21:16,116 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,116 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,242 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:16,242 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,242 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [318019534]
[2025-04-28 21:21:16,242 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [318019534] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,242 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,242 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:16,243 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [854050622]
[2025-04-28 21:21:16,243 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,243 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:16,243 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,244 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:16,244 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:16,244 INFO  L87              Difference]: Start difference. First operand 92 states and 149 transitions. Second operand  has 9 states, 8 states have (on average 2.5) internal successors, (20), 9 states have internal predecessors, (20), 3 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 8 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:16,442 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,442 INFO  L93              Difference]: Finished difference Result 112 states and 184 transitions.
[2025-04-28 21:21:16,442 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:16,443 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 2.5) internal successors, (20), 9 states have internal predecessors, (20), 3 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 8 states have call predecessors, (11), 3 states have call successors, (11) Word has length 42
[2025-04-28 21:21:16,443 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,444 INFO  L225             Difference]: With dead ends: 112
[2025-04-28 21:21:16,444 INFO  L226             Difference]: Without dead ends: 112
[2025-04-28 21:21:16,445 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:16,445 INFO  L437           NwaCegarLoop]: 118 mSDtfsCounter, 1 mSDsluCounter, 814 mSDsCounter, 0 mSdLazyCounter, 142 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 932 SdHoareTripleChecker+Invalid, 152 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 142 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,446 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 932 Invalid, 152 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 142 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:16,446 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-04-28 21:21:16,455 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 110.
[2025-04-28 21:21:16,456 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 110 states, 42 states have (on average 1.5714285714285714) internal successors, (66), 66 states have internal predecessors, (66), 40 states have call successors, (40), 15 states have call predecessors, (40), 28 states have return successors, (76), 28 states have call predecessors, (76), 40 states have call successors, (76)
[2025-04-28 21:21:16,457 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 110 states to 110 states and 182 transitions.
[2025-04-28 21:21:16,457 INFO  L79                 Accepts]: Start accepts. Automaton has 110 states and 182 transitions. Word has length 42
[2025-04-28 21:21:16,458 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,458 INFO  L485      AbstractCegarLoop]: Abstraction has 110 states and 182 transitions.
[2025-04-28 21:21:16,458 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 2.5) internal successors, (20), 9 states have internal predecessors, (20), 3 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 8 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:16,458 INFO  L278                IsEmpty]: Start isEmpty. Operand 110 states and 182 transitions.
[2025-04-28 21:21:16,460 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 43
[2025-04-28 21:21:16,460 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,460 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,460 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:16,460 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,461 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,461 INFO  L85        PathProgramCache]: Analyzing trace with hash 1340893321, now seen corresponding path program 1 times
[2025-04-28 21:21:16,461 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,461 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1621123121]
[2025-04-28 21:21:16,461 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,461 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,471 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 42 statements into 1 equivalence classes.
[2025-04-28 21:21:16,475 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 42 of 42 statements.
[2025-04-28 21:21:16,475 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,475 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,603 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:16,603 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,603 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1621123121]
[2025-04-28 21:21:16,603 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1621123121] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,603 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,603 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:16,603 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [87224692]
[2025-04-28 21:21:16,603 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,604 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:16,604 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,604 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:16,604 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:16,605 INFO  L87              Difference]: Start difference. First operand 110 states and 182 transitions. Second operand  has 9 states, 8 states have (on average 2.5) internal successors, (20), 9 states have internal predecessors, (20), 3 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 8 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:16,770 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,770 INFO  L93              Difference]: Finished difference Result 110 states and 181 transitions.
[2025-04-28 21:21:16,770 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:16,771 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 2.5) internal successors, (20), 9 states have internal predecessors, (20), 3 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 8 states have call predecessors, (11), 3 states have call successors, (11) Word has length 42
[2025-04-28 21:21:16,771 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,772 INFO  L225             Difference]: With dead ends: 110
[2025-04-28 21:21:16,772 INFO  L226             Difference]: Without dead ends: 109
[2025-04-28 21:21:16,772 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:16,773 INFO  L437           NwaCegarLoop]: 116 mSDtfsCounter, 0 mSDsluCounter, 803 mSDsCounter, 0 mSdLazyCounter, 132 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 919 SdHoareTripleChecker+Invalid, 142 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 132 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,773 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 919 Invalid, 142 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 132 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:16,774 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 109 states.
[2025-04-28 21:21:16,785 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 109 to 91.
[2025-04-28 21:21:16,786 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 33 states have (on average 1.696969696969697) internal successors, (56), 56 states have internal predecessors, (56), 39 states have call successors, (39), 15 states have call predecessors, (39), 19 states have return successors, (51), 19 states have call predecessors, (51), 39 states have call successors, (51)
[2025-04-28 21:21:16,789 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 146 transitions.
[2025-04-28 21:21:16,789 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 146 transitions. Word has length 42
[2025-04-28 21:21:16,789 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,789 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 146 transitions.
[2025-04-28 21:21:16,789 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 2.5) internal successors, (20), 9 states have internal predecessors, (20), 3 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 8 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:16,789 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 146 transitions.
[2025-04-28 21:21:16,792 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 47
[2025-04-28 21:21:16,792 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,792 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,793 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:16,793 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,793 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,793 INFO  L85        PathProgramCache]: Analyzing trace with hash -1019926522, now seen corresponding path program 1 times
[2025-04-28 21:21:16,793 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,793 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1469183542]
[2025-04-28 21:21:16,793 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,794 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,811 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 46 statements into 1 equivalence classes.
[2025-04-28 21:21:16,814 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 46 of 46 statements.
[2025-04-28 21:21:16,816 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,816 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,946 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:16,946 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,946 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1469183542]
[2025-04-28 21:21:16,946 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1469183542] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,946 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,946 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:16,946 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [153540083]
[2025-04-28 21:21:16,946 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,947 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:16,947 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,947 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:16,947 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:16,948 INFO  L87              Difference]: Start difference. First operand 91 states and 146 transitions. Second operand  has 9 states, 8 states have (on average 2.75) internal successors, (22), 9 states have internal predecessors, (22), 3 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 8 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:17,107 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,107 INFO  L93              Difference]: Finished difference Result 109 states and 174 transitions.
[2025-04-28 21:21:17,108 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:17,108 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 2.75) internal successors, (22), 9 states have internal predecessors, (22), 3 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 8 states have call predecessors, (12), 3 states have call successors, (12) Word has length 46
[2025-04-28 21:21:17,108 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,109 INFO  L225             Difference]: With dead ends: 109
[2025-04-28 21:21:17,109 INFO  L226             Difference]: Without dead ends: 109
[2025-04-28 21:21:17,109 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:17,113 INFO  L437           NwaCegarLoop]: 117 mSDtfsCounter, 1 mSDsluCounter, 807 mSDsCounter, 0 mSdLazyCounter, 126 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 924 SdHoareTripleChecker+Invalid, 134 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 126 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,114 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 924 Invalid, 134 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 126 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:17,117 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 109 states.
[2025-04-28 21:21:17,124 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 109 to 107.
[2025-04-28 21:21:17,128 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 107 states, 41 states have (on average 1.5609756097560976) internal successors, (64), 64 states have internal predecessors, (64), 39 states have call successors, (39), 15 states have call predecessors, (39), 27 states have return successors, (69), 27 states have call predecessors, (69), 39 states have call successors, (69)
[2025-04-28 21:21:17,129 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 107 states to 107 states and 172 transitions.
[2025-04-28 21:21:17,129 INFO  L79                 Accepts]: Start accepts. Automaton has 107 states and 172 transitions. Word has length 46
[2025-04-28 21:21:17,130 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,130 INFO  L485      AbstractCegarLoop]: Abstraction has 107 states and 172 transitions.
[2025-04-28 21:21:17,130 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 2.75) internal successors, (22), 9 states have internal predecessors, (22), 3 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 8 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:17,130 INFO  L278                IsEmpty]: Start isEmpty. Operand 107 states and 172 transitions.
[2025-04-28 21:21:17,132 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 47
[2025-04-28 21:21:17,132 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,132 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,133 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:17,133 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,133 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,133 INFO  L85        PathProgramCache]: Analyzing trace with hash -2142470374, now seen corresponding path program 1 times
[2025-04-28 21:21:17,133 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,133 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1981147007]
[2025-04-28 21:21:17,133 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,134 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,145 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 46 statements into 1 equivalence classes.
[2025-04-28 21:21:17,148 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 46 of 46 statements.
[2025-04-28 21:21:17,148 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,149 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,274 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:17,274 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,274 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1981147007]
[2025-04-28 21:21:17,274 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1981147007] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,274 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,274 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:17,274 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [270099483]
[2025-04-28 21:21:17,274 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,275 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:17,275 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,276 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:17,276 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:17,276 INFO  L87              Difference]: Start difference. First operand 107 states and 172 transitions. Second operand  has 9 states, 8 states have (on average 2.75) internal successors, (22), 9 states have internal predecessors, (22), 3 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 8 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:17,432 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,432 INFO  L93              Difference]: Finished difference Result 107 states and 171 transitions.
[2025-04-28 21:21:17,433 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:17,433 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 2.75) internal successors, (22), 9 states have internal predecessors, (22), 3 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 8 states have call predecessors, (12), 3 states have call successors, (12) Word has length 46
[2025-04-28 21:21:17,433 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,434 INFO  L225             Difference]: With dead ends: 107
[2025-04-28 21:21:17,434 INFO  L226             Difference]: Without dead ends: 106
[2025-04-28 21:21:17,435 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:17,435 INFO  L437           NwaCegarLoop]: 117 mSDtfsCounter, 0 mSDsluCounter, 810 mSDsCounter, 0 mSdLazyCounter, 116 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 927 SdHoareTripleChecker+Invalid, 124 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 116 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,435 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 927 Invalid, 124 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 116 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:17,437 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-04-28 21:21:17,446 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 90.
[2025-04-28 21:21:17,447 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 33 states have (on average 1.6666666666666667) internal successors, (55), 55 states have internal predecessors, (55), 38 states have call successors, (38), 15 states have call predecessors, (38), 19 states have return successors, (50), 19 states have call predecessors, (50), 38 states have call successors, (50)
[2025-04-28 21:21:17,448 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 143 transitions.
[2025-04-28 21:21:17,448 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 143 transitions. Word has length 46
[2025-04-28 21:21:17,448 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,448 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 143 transitions.
[2025-04-28 21:21:17,448 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 2.75) internal successors, (22), 9 states have internal predecessors, (22), 3 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 8 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:17,448 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 143 transitions.
[2025-04-28 21:21:17,450 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 51
[2025-04-28 21:21:17,450 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,450 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,450 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:17,450 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,452 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,453 INFO  L85        PathProgramCache]: Analyzing trace with hash -948239203, now seen corresponding path program 1 times
[2025-04-28 21:21:17,453 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,453 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [160152245]
[2025-04-28 21:21:17,453 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,453 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,476 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 50 statements into 1 equivalence classes.
[2025-04-28 21:21:17,481 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 50 of 50 statements.
[2025-04-28 21:21:17,481 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,482 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,620 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:17,621 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,621 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [160152245]
[2025-04-28 21:21:17,621 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [160152245] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,621 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,621 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:17,621 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2034602953]
[2025-04-28 21:21:17,621 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,621 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:17,622 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,622 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:17,622 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:17,622 INFO  L87              Difference]: Start difference. First operand 90 states and 143 transitions. Second operand  has 10 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 10 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (13), 9 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:17,822 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,822 INFO  L93              Difference]: Finished difference Result 110 states and 174 transitions.
[2025-04-28 21:21:17,823 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:17,823 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 10 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (13), 9 states have call predecessors, (13), 3 states have call successors, (13) Word has length 50
[2025-04-28 21:21:17,823 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,824 INFO  L225             Difference]: With dead ends: 110
[2025-04-28 21:21:17,824 INFO  L226             Difference]: Without dead ends: 110
[2025-04-28 21:21:17,824 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:17,825 INFO  L437           NwaCegarLoop]: 133 mSDtfsCounter, 1 mSDsluCounter, 1033 mSDsCounter, 0 mSdLazyCounter, 157 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1166 SdHoareTripleChecker+Invalid, 166 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 157 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,825 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1166 Invalid, 166 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 157 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:17,826 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-04-28 21:21:17,839 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 108.
[2025-04-28 21:21:17,840 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 108 states, 42 states have (on average 1.5238095238095237) internal successors, (64), 64 states have internal predecessors, (64), 38 states have call successors, (38), 15 states have call predecessors, (38), 28 states have return successors, (70), 28 states have call predecessors, (70), 38 states have call successors, (70)
[2025-04-28 21:21:17,841 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 108 states to 108 states and 172 transitions.
[2025-04-28 21:21:17,841 INFO  L79                 Accepts]: Start accepts. Automaton has 108 states and 172 transitions. Word has length 50
[2025-04-28 21:21:17,842 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,842 INFO  L485      AbstractCegarLoop]: Abstraction has 108 states and 172 transitions.
[2025-04-28 21:21:17,842 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 10 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (13), 9 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:17,842 INFO  L278                IsEmpty]: Start isEmpty. Operand 108 states and 172 transitions.
[2025-04-28 21:21:17,845 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 51
[2025-04-28 21:21:17,845 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,845 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,845 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:17,845 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,846 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,846 INFO  L85        PathProgramCache]: Analyzing trace with hash -760048037, now seen corresponding path program 1 times
[2025-04-28 21:21:17,846 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,846 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [923373055]
[2025-04-28 21:21:17,846 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,846 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,859 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 50 statements into 1 equivalence classes.
[2025-04-28 21:21:17,863 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 50 of 50 statements.
[2025-04-28 21:21:17,863 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,864 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,990 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:17,990 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,990 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [923373055]
[2025-04-28 21:21:17,990 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [923373055] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,990 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,990 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:17,990 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1278388709]
[2025-04-28 21:21:17,991 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,991 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:17,991 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,991 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:17,991 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:17,992 INFO  L87              Difference]: Start difference. First operand 108 states and 172 transitions. Second operand  has 9 states, 8 states have (on average 3.0) internal successors, (24), 9 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (13), 8 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:18,163 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,164 INFO  L93              Difference]: Finished difference Result 144 states and 229 transitions.
[2025-04-28 21:21:18,164 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:18,164 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 3.0) internal successors, (24), 9 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (13), 8 states have call predecessors, (13), 3 states have call successors, (13) Word has length 50
[2025-04-28 21:21:18,165 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,166 INFO  L225             Difference]: With dead ends: 144
[2025-04-28 21:21:18,166 INFO  L226             Difference]: Without dead ends: 144
[2025-04-28 21:21:18,166 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:18,167 INFO  L437           NwaCegarLoop]: 114 mSDtfsCounter, 1 mSDsluCounter, 783 mSDsCounter, 0 mSdLazyCounter, 136 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 897 SdHoareTripleChecker+Invalid, 144 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 136 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,167 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 897 Invalid, 144 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 136 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:18,167 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 144 states.
[2025-04-28 21:21:18,181 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 144 to 140.
[2025-04-28 21:21:18,183 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 140 states, 58 states have (on average 1.3793103448275863) internal successors, (80), 80 states have internal predecessors, (80), 38 states have call successors, (38), 15 states have call predecessors, (38), 44 states have return successors, (104), 44 states have call predecessors, (104), 38 states have call successors, (104)
[2025-04-28 21:21:18,185 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 140 states to 140 states and 222 transitions.
[2025-04-28 21:21:18,185 INFO  L79                 Accepts]: Start accepts. Automaton has 140 states and 222 transitions. Word has length 50
[2025-04-28 21:21:18,185 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,185 INFO  L485      AbstractCegarLoop]: Abstraction has 140 states and 222 transitions.
[2025-04-28 21:21:18,185 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 3.0) internal successors, (24), 9 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (13), 8 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:18,185 INFO  L278                IsEmpty]: Start isEmpty. Operand 140 states and 222 transitions.
[2025-04-28 21:21:18,187 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 51
[2025-04-28 21:21:18,187 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,187 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,187 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:18,187 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,188 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,188 INFO  L85        PathProgramCache]: Analyzing trace with hash -408143424, now seen corresponding path program 1 times
[2025-04-28 21:21:18,188 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,188 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [124640096]
[2025-04-28 21:21:18,188 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,188 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,201 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 50 statements into 1 equivalence classes.
[2025-04-28 21:21:18,206 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 50 of 50 statements.
[2025-04-28 21:21:18,206 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,206 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,317 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:18,317 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,317 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [124640096]
[2025-04-28 21:21:18,317 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [124640096] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,317 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,317 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:18,317 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [886106047]
[2025-04-28 21:21:18,317 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,318 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:18,318 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,318 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:18,318 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:18,318 INFO  L87              Difference]: Start difference. First operand 140 states and 222 transitions. Second operand  has 9 states, 8 states have (on average 3.0) internal successors, (24), 9 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (13), 8 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:18,479 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,479 INFO  L93              Difference]: Finished difference Result 144 states and 227 transitions.
[2025-04-28 21:21:18,479 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:18,480 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 3.0) internal successors, (24), 9 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (13), 8 states have call predecessors, (13), 3 states have call successors, (13) Word has length 50
[2025-04-28 21:21:18,480 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,493 INFO  L225             Difference]: With dead ends: 144
[2025-04-28 21:21:18,494 INFO  L226             Difference]: Without dead ends: 144
[2025-04-28 21:21:18,494 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:18,495 INFO  L437           NwaCegarLoop]: 129 mSDtfsCounter, 1 mSDsluCounter, 871 mSDsCounter, 0 mSdLazyCounter, 136 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1000 SdHoareTripleChecker+Invalid, 144 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 136 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,495 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1000 Invalid, 144 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 136 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:18,495 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 144 states.
[2025-04-28 21:21:18,510 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 144 to 140.
[2025-04-28 21:21:18,511 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 140 states, 58 states have (on average 1.3793103448275863) internal successors, (80), 80 states have internal predecessors, (80), 38 states have call successors, (38), 15 states have call predecessors, (38), 44 states have return successors, (102), 44 states have call predecessors, (102), 38 states have call successors, (102)
[2025-04-28 21:21:18,515 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 140 states to 140 states and 220 transitions.
[2025-04-28 21:21:18,515 INFO  L79                 Accepts]: Start accepts. Automaton has 140 states and 220 transitions. Word has length 50
[2025-04-28 21:21:18,516 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,516 INFO  L485      AbstractCegarLoop]: Abstraction has 140 states and 220 transitions.
[2025-04-28 21:21:18,516 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 3.0) internal successors, (24), 9 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (13), 8 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:18,516 INFO  L278                IsEmpty]: Start isEmpty. Operand 140 states and 220 transitions.
[2025-04-28 21:21:18,518 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 51
[2025-04-28 21:21:18,518 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,518 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,518 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:21:18,519 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,519 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,519 INFO  L85        PathProgramCache]: Analyzing trace with hash 948177307, now seen corresponding path program 1 times
[2025-04-28 21:21:18,519 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,520 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1699621781]
[2025-04-28 21:21:18,520 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[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,531 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 50 statements into 1 equivalence classes.
[2025-04-28 21:21:18,535 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 50 of 50 statements.
[2025-04-28 21:21:18,535 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,536 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,666 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:18,666 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,666 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1699621781]
[2025-04-28 21:21:18,666 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1699621781] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,666 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,666 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:18,666 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1671270992]
[2025-04-28 21:21:18,666 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,667 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:18,667 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,667 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:18,667 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:18,667 INFO  L87              Difference]: Start difference. First operand 140 states and 220 transitions. Second operand  has 10 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 10 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (13), 9 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:18,839 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,839 INFO  L93              Difference]: Finished difference Result 140 states and 219 transitions.
[2025-04-28 21:21:18,841 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:18,841 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 10 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (13), 9 states have call predecessors, (13), 3 states have call successors, (13) Word has length 50
[2025-04-28 21:21:18,841 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,843 INFO  L225             Difference]: With dead ends: 140
[2025-04-28 21:21:18,843 INFO  L226             Difference]: Without dead ends: 139
[2025-04-28 21:21:18,843 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:18,844 INFO  L437           NwaCegarLoop]: 130 mSDtfsCounter, 0 mSDsluCounter, 1009 mSDsCounter, 0 mSdLazyCounter, 150 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 1139 SdHoareTripleChecker+Invalid, 159 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 150 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,844 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 1139 Invalid, 159 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 150 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:18,847 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 139 states.
[2025-04-28 21:21:18,856 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 139 to 105.
[2025-04-28 21:21:18,857 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 41 states have (on average 1.5121951219512195) internal successors, (62), 62 states have internal predecessors, (62), 37 states have call successors, (37), 15 states have call predecessors, (37), 27 states have return successors, (65), 27 states have call predecessors, (65), 37 states have call successors, (65)
[2025-04-28 21:21:18,860 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 164 transitions.
[2025-04-28 21:21:18,860 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 164 transitions. Word has length 50
[2025-04-28 21:21:18,860 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,860 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 164 transitions.
[2025-04-28 21:21:18,861 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 10 states have internal predecessors, (24), 3 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (13), 9 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:18,861 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 164 transitions.
[2025-04-28 21:21:18,862 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 55
[2025-04-28 21:21:18,863 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,863 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,863 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:21:18,863 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,863 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,863 INFO  L85        PathProgramCache]: Analyzing trace with hash 1566169507, now seen corresponding path program 1 times
[2025-04-28 21:21:18,863 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,863 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1417583507]
[2025-04-28 21:21:18,863 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,864 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,876 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 54 statements into 1 equivalence classes.
[2025-04-28 21:21:18,880 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 54 of 54 statements.
[2025-04-28 21:21:18,881 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,881 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,021 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:19,021 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,021 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1417583507]
[2025-04-28 21:21:19,021 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1417583507] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:19,021 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:19,021 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:19,022 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [617408565]
[2025-04-28 21:21:19,022 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,022 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:19,022 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,023 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:19,023 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:19,023 INFO  L87              Difference]: Start difference. First operand 105 states and 164 transitions. Second operand  has 10 states, 9 states have (on average 2.888888888888889) internal successors, (26), 10 states have internal predecessors, (26), 3 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (14), 9 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:21:19,189 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,189 INFO  L93              Difference]: Finished difference Result 135 states and 202 transitions.
[2025-04-28 21:21:19,190 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:19,191 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 2.888888888888889) internal successors, (26), 10 states have internal predecessors, (26), 3 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (14), 9 states have call predecessors, (14), 3 states have call successors, (14) Word has length 54
[2025-04-28 21:21:19,191 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,192 INFO  L225             Difference]: With dead ends: 135
[2025-04-28 21:21:19,192 INFO  L226             Difference]: Without dead ends: 135
[2025-04-28 21:21:19,192 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:19,193 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 1 mSDsluCounter, 862 mSDsCounter, 0 mSdLazyCounter, 139 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 971 SdHoareTripleChecker+Invalid, 146 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 139 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,193 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 971 Invalid, 146 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 139 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:19,194 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 135 states.
[2025-04-28 21:21:19,206 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 135 to 133.
[2025-04-28 21:21:19,206 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 55 states have (on average 1.3818181818181818) internal successors, (76), 76 states have internal predecessors, (76), 37 states have call successors, (37), 15 states have call predecessors, (37), 41 states have return successors, (87), 41 states have call predecessors, (87), 37 states have call successors, (87)
[2025-04-28 21:21:19,208 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 200 transitions.
[2025-04-28 21:21:19,208 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 200 transitions. Word has length 54
[2025-04-28 21:21:19,208 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,208 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 200 transitions.
[2025-04-28 21:21:19,208 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 2.888888888888889) internal successors, (26), 10 states have internal predecessors, (26), 3 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (14), 9 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:21:19,208 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 200 transitions.
[2025-04-28 21:21:19,210 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 55
[2025-04-28 21:21:19,211 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,211 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,211 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:21:19,211 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,211 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,211 INFO  L85        PathProgramCache]: Analyzing trace with hash -2130863827, now seen corresponding path program 1 times
[2025-04-28 21:21:19,211 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,211 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [876467513]
[2025-04-28 21:21:19,212 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,212 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,224 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 54 statements into 1 equivalence classes.
[2025-04-28 21:21:19,229 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 54 of 54 statements.
[2025-04-28 21:21:19,229 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,229 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,367 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:19,368 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,368 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [876467513]
[2025-04-28 21:21:19,368 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [876467513] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:19,368 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:19,368 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:19,368 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [426609180]
[2025-04-28 21:21:19,368 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,368 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:19,369 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,369 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:19,369 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:19,369 INFO  L87              Difference]: Start difference. First operand 133 states and 200 transitions. Second operand  has 10 states, 9 states have (on average 2.888888888888889) internal successors, (26), 10 states have internal predecessors, (26), 3 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (14), 9 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:21:19,529 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,529 INFO  L93              Difference]: Finished difference Result 133 states and 199 transitions.
[2025-04-28 21:21:19,529 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:19,529 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 2.888888888888889) internal successors, (26), 10 states have internal predecessors, (26), 3 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (14), 9 states have call predecessors, (14), 3 states have call successors, (14) Word has length 54
[2025-04-28 21:21:19,530 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,531 INFO  L225             Difference]: With dead ends: 133
[2025-04-28 21:21:19,531 INFO  L226             Difference]: Without dead ends: 132
[2025-04-28 21:21:19,533 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:19,534 INFO  L437           NwaCegarLoop]: 111 mSDtfsCounter, 0 mSDsluCounter, 877 mSDsCounter, 0 mSdLazyCounter, 132 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 988 SdHoareTripleChecker+Invalid, 139 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 132 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,534 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 988 Invalid, 139 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 132 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:19,535 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-04-28 21:21:19,544 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 104.
[2025-04-28 21:21:19,545 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 104 states, 41 states have (on average 1.4878048780487805) internal successors, (61), 61 states have internal predecessors, (61), 36 states have call successors, (36), 15 states have call predecessors, (36), 27 states have return successors, (64), 27 states have call predecessors, (64), 36 states have call successors, (64)
[2025-04-28 21:21:19,546 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 104 states to 104 states and 161 transitions.
[2025-04-28 21:21:19,546 INFO  L79                 Accepts]: Start accepts. Automaton has 104 states and 161 transitions. Word has length 54
[2025-04-28 21:21:19,546 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,546 INFO  L485      AbstractCegarLoop]: Abstraction has 104 states and 161 transitions.
[2025-04-28 21:21:19,547 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 2.888888888888889) internal successors, (26), 10 states have internal predecessors, (26), 3 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (14), 9 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:21:19,547 INFO  L278                IsEmpty]: Start isEmpty. Operand 104 states and 161 transitions.
[2025-04-28 21:21:19,548 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-04-28 21:21:19,548 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,548 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,548 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-04-28 21:21:19,548 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,549 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,550 INFO  L85        PathProgramCache]: Analyzing trace with hash -1954096093, now seen corresponding path program 1 times
[2025-04-28 21:21:19,550 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,550 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [942989562]
[2025-04-28 21:21:19,550 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,550 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,564 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-04-28 21:21:19,568 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-04-28 21:21:19,569 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,569 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,723 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:19,723 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,724 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [942989562]
[2025-04-28 21:21:19,724 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [942989562] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:19,724 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:19,724 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:19,724 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [696644152]
[2025-04-28 21:21:19,724 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,724 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:19,724 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,725 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:19,725 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:19,725 INFO  L87              Difference]: Start difference. First operand 104 states and 161 transitions. Second operand  has 11 states, 10 states have (on average 2.8) internal successors, (28), 11 states have internal predecessors, (28), 3 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (15), 10 states have call predecessors, (15), 3 states have call successors, (15)
[2025-04-28 21:21:19,916 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,916 INFO  L93              Difference]: Finished difference Result 134 states and 200 transitions.
[2025-04-28 21:21:19,917 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:19,917 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 10 states have (on average 2.8) internal successors, (28), 11 states have internal predecessors, (28), 3 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (15), 10 states have call predecessors, (15), 3 states have call successors, (15) Word has length 58
[2025-04-28 21:21:19,917 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,918 INFO  L225             Difference]: With dead ends: 134
[2025-04-28 21:21:19,918 INFO  L226             Difference]: Without dead ends: 134
[2025-04-28 21:21:19,919 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:19,919 INFO  L437           NwaCegarLoop]: 106 mSDtfsCounter, 1 mSDsluCounter, 943 mSDsCounter, 0 mSdLazyCounter, 174 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1049 SdHoareTripleChecker+Invalid, 182 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 174 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,919 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1049 Invalid, 182 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 174 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:19,920 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-04-28 21:21:19,927 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 134.
[2025-04-28 21:21:19,927 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 134 states, 56 states have (on average 1.3571428571428572) internal successors, (76), 76 states have internal predecessors, (76), 36 states have call successors, (36), 15 states have call predecessors, (36), 42 states have return successors, (88), 42 states have call predecessors, (88), 36 states have call successors, (88)
[2025-04-28 21:21:19,928 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 134 states to 134 states and 200 transitions.
[2025-04-28 21:21:19,929 INFO  L79                 Accepts]: Start accepts. Automaton has 134 states and 200 transitions. Word has length 58
[2025-04-28 21:21:19,929 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,929 INFO  L485      AbstractCegarLoop]: Abstraction has 134 states and 200 transitions.
[2025-04-28 21:21:19,929 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 10 states have (on average 2.8) internal successors, (28), 11 states have internal predecessors, (28), 3 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (15), 10 states have call predecessors, (15), 3 states have call successors, (15)
[2025-04-28 21:21:19,929 INFO  L278                IsEmpty]: Start isEmpty. Operand 134 states and 200 transitions.
[2025-04-28 21:21:19,931 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-04-28 21:21:19,931 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,931 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,931 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-04-28 21:21:19,931 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,931 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,932 INFO  L85        PathProgramCache]: Analyzing trace with hash -1039607372, now seen corresponding path program 1 times
[2025-04-28 21:21:19,932 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,932 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2047260664]
[2025-04-28 21:21:19,932 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,932 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,943 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-04-28 21:21:19,948 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-04-28 21:21:19,948 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,948 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,091 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:20,091 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,091 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2047260664]
[2025-04-28 21:21:20,091 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2047260664] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,091 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,091 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:20,091 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [585351625]
[2025-04-28 21:21:20,091 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,092 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:20,092 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,092 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:20,092 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:20,093 INFO  L87              Difference]: Start difference. First operand 134 states and 200 transitions. Second operand  has 11 states, 10 states have (on average 2.8) internal successors, (28), 11 states have internal predecessors, (28), 3 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (15), 10 states have call predecessors, (15), 3 states have call successors, (15)
[2025-04-28 21:21:20,267 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,267 INFO  L93              Difference]: Finished difference Result 128 states and 194 transitions.
[2025-04-28 21:21:20,267 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:20,268 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 10 states have (on average 2.8) internal successors, (28), 11 states have internal predecessors, (28), 3 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (15), 10 states have call predecessors, (15), 3 states have call successors, (15) Word has length 58
[2025-04-28 21:21:20,268 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,268 INFO  L225             Difference]: With dead ends: 128
[2025-04-28 21:21:20,268 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:20,268 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:20,269 INFO  L437           NwaCegarLoop]: 99 mSDtfsCounter, 0 mSDsluCounter, 880 mSDsCounter, 0 mSdLazyCounter, 166 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 979 SdHoareTripleChecker+Invalid, 174 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 166 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,269 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 979 Invalid, 174 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 166 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:20,269 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:20,270 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:20,270 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:21:20,270 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:20,270 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 58
[2025-04-28 21:21:20,270 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,270 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:20,270 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 10 states have (on average 2.8) internal successors, (28), 11 states have internal predecessors, (28), 3 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (15), 10 states have call predecessors, (15), 3 states have call successors, (15)
[2025-04-28 21:21:20,270 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:20,271 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:20,273 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:20,273 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-04-28 21:21:20,276 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,279 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:20,282 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:20 BoogieIcfgContainer
[2025-04-28 21:21:20,282 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:20,283 INFO  L158              Benchmark]: Toolchain (without parser) took 8947.47ms. Allocated memory is still 234.9MB. Free memory was 153.8MB in the beginning and 86.7MB in the end (delta: 67.1MB). Peak memory consumption was 71.1MB. Max. memory is 33.6GB.
[2025-04-28 21:21:20,283 INFO  L158              Benchmark]: SmtParser took 0.36ms. Allocated memory is still 234.9MB. Free memory is still 170.3MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:20,283 INFO  L158              Benchmark]: ChcToBoogie took 33.56ms. Allocated memory is still 234.9MB. Free memory was 153.8MB in the beginning and 152.3MB in the end (delta: 1.5MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:20,283 INFO  L158              Benchmark]: Boogie Preprocessor took 102.61ms. Allocated memory is still 234.9MB. Free memory was 152.3MB in the beginning and 149.1MB in the end (delta: 3.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:20,284 INFO  L158              Benchmark]: RCFGBuilder took 615.97ms. Allocated memory is still 234.9MB. Free memory was 149.1MB in the beginning and 121.4MB in the end (delta: 27.7MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:20,284 INFO  L158              Benchmark]: TraceAbstraction took 8189.47ms. Allocated memory is still 234.9MB. Free memory was 120.6MB in the beginning and 86.7MB in the end (delta: 33.9MB). Peak memory consumption was 37.5MB. Max. memory is 33.6GB.
[2025-04-28 21:21:20,286 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.36ms. Allocated memory is still 234.9MB. Free memory is still 170.3MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 33.56ms. Allocated memory is still 234.9MB. Free memory was 153.8MB in the beginning and 152.3MB in the end (delta: 1.5MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 102.61ms. Allocated memory is still 234.9MB. Free memory was 152.3MB in the beginning and 149.1MB in the end (delta: 3.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 615.97ms. Allocated memory is still 234.9MB. Free memory was 149.1MB in the beginning and 121.4MB in the end (delta: 27.7MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 8189.47ms. Allocated memory is still 234.9MB. Free memory was 120.6MB in the beginning and 86.7MB in the end (delta: 33.9MB). Peak memory consumption was 37.5MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 16 procedures, 89 locations, 187 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 8.1s, OverallIterations: 20, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.1s, AutomataDifference: 4.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 44 SdHoareTripleChecker+Valid, 3.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 12 mSDsluCounter, 18566 SdHoareTripleChecker+Invalid, 2.8s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 16115 mSDsCounter, 180 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 2556 IncrementalHoareTripleChecker+Invalid, 2736 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 180 mSolverCounterUnsat, 2451 mSDtfsCounter, 2556 mSolverCounterSat, 0.2s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 176 GetRequests, 40 SyntacticMatches, 0 SemanticMatches, 136 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.9s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=140occurred in iteration=14, InterpolantAutomatonStates: 176, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.4s AutomataMinimizationTime, 20 MinimizatonAttempts, 166 StatesRemovedByMinimization, 18 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 2.9s InterpolantComputationTime, 872 NumberOfCodeBlocks, 872 NumberOfCodeBlocksAsserted, 20 NumberOfCheckSat, 852 ConstructedInterpolants, 0 QuantifiedInterpolants, 1436 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 20 InterpolantComputations, 20 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:21:20,299 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
sat
