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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:40,018 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:40,110 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5219b19d-dd59-4270-a3cf-1191869dd5a6/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:40,118 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:40,120 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:40,157 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:40,159 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:40,159 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:40,161 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:40,161 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:40,161 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:40,162 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:40,162 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:40,162 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:40,163 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:40,163 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:40,164 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:40,164 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:40,164 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,165 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:40,165 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:40,165 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:40,165 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:40,165 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:40,165 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:40,166 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:40,166 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:40,472 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:40,480 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:40,482 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:40,484 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:40,484 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:40,485 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5219b19d-dd59-4270-a3cf-1191869dd5a6/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-217.smt2
[2025-04-28 21:21:40,487 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:40,490 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:41,557 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5219b19d-dd59-4270-a3cf-1191869dd5a6/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-217.smt2
[2025-04-28 21:21:41,561 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:41,564 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:41,564 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:41,565 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:41,565 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:41,569 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,642 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41 Unit
[2025-04-28 21:21:41,642 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:41,643 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,644 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:41,644 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:41,660 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,661 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,698 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,698 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,723 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,727 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,731 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,738 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,742 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,768 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,769 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:41,769 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:41,769 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:41,770 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,777 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,794 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,811 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:41,816 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:41,827 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:41,827 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:41,827 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:41,827 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main507 given in one single declaration
[2025-04-28 21:21:41,827 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main507
[2025-04-28 21:21:41,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main507
[2025-04-28 21:21:41,828 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main411 given in one single declaration
[2025-04-28 21:21:41,828 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main411
[2025-04-28 21:21:41,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main411
[2025-04-28 21:21:41,828 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main117 given in one single declaration
[2025-04-28 21:21:41,828 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main117
[2025-04-28 21:21:41,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main117
[2025-04-28 21:21:41,828 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main198 given in one single declaration
[2025-04-28 21:21:41,828 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main198
[2025-04-28 21:21:41,828 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main198
[2025-04-28 21:21:41,829 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main414 given in one single declaration
[2025-04-28 21:21:41,830 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main414
[2025-04-28 21:21:41,830 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main414
[2025-04-28 21:21:41,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main271 given in one single declaration
[2025-04-28 21:21:41,831 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main271
[2025-04-28 21:21:41,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main271
[2025-04-28 21:21:41,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main457 given in one single declaration
[2025-04-28 21:21:41,831 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main457
[2025-04-28 21:21:41,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main457
[2025-04-28 21:21:41,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main454 given in one single declaration
[2025-04-28 21:21:41,831 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main454
[2025-04-28 21:21:41,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main454
[2025-04-28 21:21:41,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main254 given in one single declaration
[2025-04-28 21:21:41,831 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main254
[2025-04-28 21:21:41,831 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main254
[2025-04-28 21:21:41,831 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main327 given in one single declaration
[2025-04-28 21:21:41,831 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main327
[2025-04-28 21:21:41,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main327
[2025-04-28 21:21:41,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main333 given in one single declaration
[2025-04-28 21:21:41,832 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main333
[2025-04-28 21:21:41,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main333
[2025-04-28 21:21:41,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main429 given in one single declaration
[2025-04-28 21:21:41,832 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main429
[2025-04-28 21:21:41,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main429
[2025-04-28 21:21:41,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main297 given in one single declaration
[2025-04-28 21:21:41,832 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main297
[2025-04-28 21:21:41,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main297
[2025-04-28 21:21:41,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main490 given in one single declaration
[2025-04-28 21:21:41,832 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main490
[2025-04-28 21:21:41,832 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main490
[2025-04-28 21:21:41,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main106 given in one single declaration
[2025-04-28 21:21:41,832 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main106
[2025-04-28 21:21:41,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main106
[2025-04-28 21:21:41,833 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main4 given in one single declaration
[2025-04-28 21:21:41,833 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main4
[2025-04-28 21:21:41,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main4
[2025-04-28 21:21:41,833 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:41,833 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:41,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:42,178 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:42,181 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:43,408 INFO  L?                        ?]: Removed 147 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:43,409 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:43,431 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:43,433 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:43,434 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:43 BoogieIcfgContainer
[2025-04-28 21:21:43,434 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:43,436 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:43,437 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:43,441 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:43,441 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/3) ...
[2025-04-28 21:21:43,442 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@17b3e530 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:43, skipping insertion in model container
[2025-04-28 21:21:43,442 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (2/3) ...
[2025-04-28 21:21:43,442 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@17b3e530 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:43, skipping insertion in model container
[2025-04-28 21:21:43,442 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:43" (3/3) ...
[2025-04-28 21:21:43,445 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:43,463 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:43,467 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 18 procedures, 143 locations, 375 edges, 18 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:43,528 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:43,552 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;@eabd61a, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:43,553 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:43,557 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 143 states, 35 states have (on average 3.085714285714286) internal successors, (108), 108 states have internal predecessors, (108), 89 states have call successors, (89), 17 states have call predecessors, (89), 17 states have return successors, (89), 17 states have call predecessors, (89), 89 states have call successors, (89)
[2025-04-28 21:21:43,582 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:43,582 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,583 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]
[2025-04-28 21:21:43,583 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,590 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,591 INFO  L85        PathProgramCache]: Analyzing trace with hash 197532598, now seen corresponding path program 1 times
[2025-04-28 21:21:43,600 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,601 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1019192958]
[2025-04-28 21:21:43,601 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,602 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,660 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:43,771 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:43,772 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,772 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,299 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:44,301 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,301 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1019192958]
[2025-04-28 21:21:44,302 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1019192958] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,303 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,307 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:44,310 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1201689028]
[2025-04-28 21:21:44,311 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,317 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:44,319 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,356 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:44,356 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:44,359 INFO  L87              Difference]: Start difference. First operand  has 143 states, 35 states have (on average 3.085714285714286) internal successors, (108), 108 states have internal predecessors, (108), 89 states have call successors, (89), 17 states have call predecessors, (89), 17 states have return successors, (89), 17 states have call predecessors, (89), 89 states have call successors, (89) Second operand  has 6 states, 5 states have (on average 2.4) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:45,290 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,291 INFO  L93              Difference]: Finished difference Result 138 states and 306 transitions.
[2025-04-28 21:21:45,293 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:45,295 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 2.4) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:45,295 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,310 INFO  L225             Difference]: With dead ends: 138
[2025-04-28 21:21:45,310 INFO  L226             Difference]: Without dead ends: 138
[2025-04-28 21:21:45,313 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:45,317 INFO  L437           NwaCegarLoop]: 218 mSDtfsCounter, 1 mSDsluCounter, 818 mSDsCounter, 0 mSdLazyCounter, 266 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1036 SdHoareTripleChecker+Invalid, 271 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 266 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,318 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1036 Invalid, 271 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 266 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:45,341 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 138 states.
[2025-04-28 21:21:45,417 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 138 to 138.
[2025-04-28 21:21:45,419 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 138 states, 36 states have (on average 2.8055555555555554) internal successors, (101), 101 states have internal predecessors, (101), 82 states have call successors, (82), 17 states have call predecessors, (82), 19 states have return successors, (123), 19 states have call predecessors, (123), 82 states have call successors, (123)
[2025-04-28 21:21:45,425 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 138 states to 138 states and 306 transitions.
[2025-04-28 21:21:45,427 INFO  L79                 Accepts]: Start accepts. Automaton has 138 states and 306 transitions. Word has length 24
[2025-04-28 21:21:45,428 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,428 INFO  L485      AbstractCegarLoop]: Abstraction has 138 states and 306 transitions.
[2025-04-28 21:21:45,428 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 2.4) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:45,429 INFO  L278                IsEmpty]: Start isEmpty. Operand 138 states and 306 transitions.
[2025-04-28 21:21:45,436 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:45,436 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,436 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,437 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:45,437 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,437 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,438 INFO  L85        PathProgramCache]: Analyzing trace with hash -2136107550, now seen corresponding path program 1 times
[2025-04-28 21:21:45,438 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,438 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [308053925]
[2025-04-28 21:21:45,438 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,438 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,474 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:45,523 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:45,523 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,523 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,727 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:45,727 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,727 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [308053925]
[2025-04-28 21:21:45,727 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [308053925] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,727 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,728 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:45,728 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [657558373]
[2025-04-28 21:21:45,728 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,729 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:45,729 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,730 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:45,730 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:45,730 INFO  L87              Difference]: Start difference. First operand 138 states and 306 transitions. Second operand  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:46,542 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,543 INFO  L93              Difference]: Finished difference Result 142 states and 348 transitions.
[2025-04-28 21:21:46,543 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:46,544 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:21:46,544 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,547 INFO  L225             Difference]: With dead ends: 142
[2025-04-28 21:21:46,550 INFO  L226             Difference]: Without dead ends: 142
[2025-04-28 21:21:46,550 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:46,551 INFO  L437           NwaCegarLoop]: 261 mSDtfsCounter, 1 mSDsluCounter, 688 mSDsCounter, 0 mSdLazyCounter, 256 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 949 SdHoareTripleChecker+Invalid, 260 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 256 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,552 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 949 Invalid, 260 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 256 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:46,555 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-04-28 21:21:46,598 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 142.
[2025-04-28 21:21:46,599 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 38 states have (on average 2.710526315789474) internal successors, (103), 103 states have internal predecessors, (103), 82 states have call successors, (82), 17 states have call predecessors, (82), 21 states have return successors, (163), 21 states have call predecessors, (163), 82 states have call successors, (163)
[2025-04-28 21:21:46,603 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 348 transitions.
[2025-04-28 21:21:46,603 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 348 transitions. Word has length 32
[2025-04-28 21:21:46,603 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,603 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 348 transitions.
[2025-04-28 21:21:46,603 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:46,604 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 348 transitions.
[2025-04-28 21:21:46,607 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:46,608 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,608 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,608 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:46,608 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,609 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,609 INFO  L85        PathProgramCache]: Analyzing trace with hash 1202814615, now seen corresponding path program 1 times
[2025-04-28 21:21:46,609 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,609 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [862483954]
[2025-04-28 21:21:46,609 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,609 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,635 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:46,655 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:46,655 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,656 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,800 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:46,800 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,800 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [862483954]
[2025-04-28 21:21:46,801 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [862483954] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,801 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,801 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:46,802 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [926135045]
[2025-04-28 21:21:46,802 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,803 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:46,803 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,804 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:46,804 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:46,805 INFO  L87              Difference]: Start difference. First operand 142 states and 348 transitions. Second operand  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:47,533 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,533 INFO  L93              Difference]: Finished difference Result 146 states and 390 transitions.
[2025-04-28 21:21:47,534 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:47,534 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:21:47,534 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,539 INFO  L225             Difference]: With dead ends: 146
[2025-04-28 21:21:47,540 INFO  L226             Difference]: Without dead ends: 146
[2025-04-28 21:21:47,540 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:47,541 INFO  L437           NwaCegarLoop]: 261 mSDtfsCounter, 1 mSDsluCounter, 682 mSDsCounter, 0 mSdLazyCounter, 248 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 943 SdHoareTripleChecker+Invalid, 258 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 248 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,541 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 943 Invalid, 258 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 248 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:47,542 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 146 states.
[2025-04-28 21:21:47,574 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 146 to 142.
[2025-04-28 21:21:47,575 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 38 states have (on average 2.710526315789474) internal successors, (103), 103 states have internal predecessors, (103), 82 states have call successors, (82), 17 states have call predecessors, (82), 21 states have return successors, (163), 21 states have call predecessors, (163), 82 states have call successors, (163)
[2025-04-28 21:21:47,578 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 348 transitions.
[2025-04-28 21:21:47,578 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 348 transitions. Word has length 32
[2025-04-28 21:21:47,578 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,578 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 348 transitions.
[2025-04-28 21:21:47,578 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:47,579 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 348 transitions.
[2025-04-28 21:21:47,582 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:47,583 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,583 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,583 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:47,583 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,583 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,584 INFO  L85        PathProgramCache]: Analyzing trace with hash 1380855520, now seen corresponding path program 1 times
[2025-04-28 21:21:47,584 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,584 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [405883466]
[2025-04-28 21:21:47,584 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,584 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,611 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:47,628 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:47,629 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,629 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,795 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:47,795 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,796 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [405883466]
[2025-04-28 21:21:47,796 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [405883466] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,796 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,796 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:47,796 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [141100468]
[2025-04-28 21:21:47,796 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,796 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:47,796 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,797 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:47,797 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:47,798 INFO  L87              Difference]: Start difference. First operand 142 states and 348 transitions. Second operand  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:48,474 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,475 INFO  L93              Difference]: Finished difference Result 150 states and 400 transitions.
[2025-04-28 21:21:48,475 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:48,475 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:21:48,476 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,478 INFO  L225             Difference]: With dead ends: 150
[2025-04-28 21:21:48,478 INFO  L226             Difference]: Without dead ends: 150
[2025-04-28 21:21:48,479 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:48,479 INFO  L437           NwaCegarLoop]: 266 mSDtfsCounter, 1 mSDsluCounter, 704 mSDsCounter, 0 mSdLazyCounter, 261 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 970 SdHoareTripleChecker+Invalid, 263 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 261 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,480 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 970 Invalid, 263 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 261 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:48,481 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 150 states.
[2025-04-28 21:21:48,507 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 150 to 146.
[2025-04-28 21:21:48,508 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 146 states, 40 states have (on average 2.625) internal successors, (105), 105 states have internal predecessors, (105), 82 states have call successors, (82), 17 states have call predecessors, (82), 23 states have return successors, (204), 23 states have call predecessors, (204), 82 states have call successors, (204)
[2025-04-28 21:21:48,510 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 146 states to 146 states and 391 transitions.
[2025-04-28 21:21:48,511 INFO  L79                 Accepts]: Start accepts. Automaton has 146 states and 391 transitions. Word has length 32
[2025-04-28 21:21:48,511 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,511 INFO  L485      AbstractCegarLoop]: Abstraction has 146 states and 391 transitions.
[2025-04-28 21:21:48,511 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.0) internal successors, (16), 5 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:48,511 INFO  L278                IsEmpty]: Start isEmpty. Operand 146 states and 391 transitions.
[2025-04-28 21:21:48,515 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:48,515 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,515 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,515 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:48,516 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,516 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,516 INFO  L85        PathProgramCache]: Analyzing trace with hash -1958066645, now seen corresponding path program 1 times
[2025-04-28 21:21:48,516 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,516 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1935114675]
[2025-04-28 21:21:48,516 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,517 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,540 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:48,557 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:48,557 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,557 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,758 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:48,759 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,759 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1935114675]
[2025-04-28 21:21:48,759 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1935114675] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,759 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,759 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:48,759 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1613369722]
[2025-04-28 21:21:48,759 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,760 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:48,760 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,760 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:48,760 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:48,760 INFO  L87              Difference]: Start difference. First operand 146 states and 391 transitions. Second operand  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:49,461 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,461 INFO  L93              Difference]: Finished difference Result 160 states and 524 transitions.
[2025-04-28 21:21:49,462 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:49,462 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:21:49,462 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,466 INFO  L225             Difference]: With dead ends: 160
[2025-04-28 21:21:49,466 INFO  L226             Difference]: Without dead ends: 160
[2025-04-28 21:21:49,466 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 3 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:49,467 INFO  L437           NwaCegarLoop]: 214 mSDtfsCounter, 1 mSDsluCounter, 1027 mSDsCounter, 0 mSdLazyCounter, 324 mSolverCounterSat, 24 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1241 SdHoareTripleChecker+Invalid, 348 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 24 IncrementalHoareTripleChecker+Valid, 324 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,469 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1241 Invalid, 348 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [24 Valid, 324 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:49,471 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 160 states.
[2025-04-28 21:21:49,529 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 160 to 156.
[2025-04-28 21:21:49,529 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 156 states, 45 states have (on average 2.4444444444444446) internal successors, (110), 110 states have internal predecessors, (110), 82 states have call successors, (82), 17 states have call predecessors, (82), 28 states have return successors, (289), 28 states have call predecessors, (289), 82 states have call successors, (289)
[2025-04-28 21:21:49,533 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 156 states to 156 states and 481 transitions.
[2025-04-28 21:21:49,534 INFO  L79                 Accepts]: Start accepts. Automaton has 156 states and 481 transitions. Word has length 32
[2025-04-28 21:21:49,534 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,534 INFO  L485      AbstractCegarLoop]: Abstraction has 156 states and 481 transitions.
[2025-04-28 21:21:49,534 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:49,534 INFO  L278                IsEmpty]: Start isEmpty. Operand 156 states and 481 transitions.
[2025-04-28 21:21:49,540 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:49,540 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,540 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,541 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:49,541 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,541 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,541 INFO  L85        PathProgramCache]: Analyzing trace with hash 441622433, now seen corresponding path program 1 times
[2025-04-28 21:21:49,542 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,542 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1212983468]
[2025-04-28 21:21:49,542 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,542 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,574 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:49,598 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:49,599 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,599 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,767 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:49,768 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,768 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1212983468]
[2025-04-28 21:21:49,768 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1212983468] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,768 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,768 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:49,768 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [272542744]
[2025-04-28 21:21:49,769 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,769 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:49,769 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,770 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:49,770 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:49,770 INFO  L87              Difference]: Start difference. First operand 156 states and 481 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:50,526 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,526 INFO  L93              Difference]: Finished difference Result 164 states and 533 transitions.
[2025-04-28 21:21:50,527 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:50,527 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:50,527 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,532 INFO  L225             Difference]: With dead ends: 164
[2025-04-28 21:21:50,532 INFO  L226             Difference]: Without dead ends: 164
[2025-04-28 21:21:50,532 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:50,534 INFO  L437           NwaCegarLoop]: 265 mSDtfsCounter, 1 mSDsluCounter, 702 mSDsCounter, 0 mSdLazyCounter, 263 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 967 SdHoareTripleChecker+Invalid, 265 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 263 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,535 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 967 Invalid, 265 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 263 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:50,537 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 164 states.
[2025-04-28 21:21:50,579 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 164 to 156.
[2025-04-28 21:21:50,580 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 156 states, 45 states have (on average 2.4444444444444446) internal successors, (110), 110 states have internal predecessors, (110), 82 states have call successors, (82), 17 states have call predecessors, (82), 28 states have return successors, (289), 28 states have call predecessors, (289), 82 states have call successors, (289)
[2025-04-28 21:21:50,585 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 156 states to 156 states and 481 transitions.
[2025-04-28 21:21:50,586 INFO  L79                 Accepts]: Start accepts. Automaton has 156 states and 481 transitions. Word has length 36
[2025-04-28 21:21:50,587 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,587 INFO  L485      AbstractCegarLoop]: Abstraction has 156 states and 481 transitions.
[2025-04-28 21:21:50,587 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:50,588 INFO  L278                IsEmpty]: Start isEmpty. Operand 156 states and 481 transitions.
[2025-04-28 21:21:50,592 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:50,592 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,592 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,592 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:50,592 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,593 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,593 INFO  L85        PathProgramCache]: Analyzing trace with hash -1476209611, now seen corresponding path program 1 times
[2025-04-28 21:21:50,593 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,593 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1658198027]
[2025-04-28 21:21:50,593 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,593 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,616 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:50,657 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:50,657 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,657 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,828 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:50,828 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,828 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1658198027]
[2025-04-28 21:21:50,829 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1658198027] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,829 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,829 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:50,829 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2008603634]
[2025-04-28 21:21:50,829 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,829 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:50,829 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,830 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:50,830 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:50,830 INFO  L87              Difference]: Start difference. First operand 156 states and 481 transitions. Second operand  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:52,211 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,212 INFO  L93              Difference]: Finished difference Result 224 states and 721 transitions.
[2025-04-28 21:21:52,212 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:52,213 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9) Word has length 36
[2025-04-28 21:21:52,213 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,217 INFO  L225             Difference]: With dead ends: 224
[2025-04-28 21:21:52,218 INFO  L226             Difference]: Without dead ends: 224
[2025-04-28 21:21:52,218 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:52,219 INFO  L437           NwaCegarLoop]: 335 mSDtfsCounter, 31 mSDsluCounter, 1494 mSDsCounter, 0 mSdLazyCounter, 631 mSolverCounterSat, 47 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 62 SdHoareTripleChecker+Valid, 1829 SdHoareTripleChecker+Invalid, 678 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 47 IncrementalHoareTripleChecker+Valid, 631 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,219 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [62 Valid, 1829 Invalid, 678 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [47 Valid, 631 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:52,220 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 224 states.
[2025-04-28 21:21:52,275 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 224 to 206.
[2025-04-28 21:21:52,276 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 206 states, 57 states have (on average 2.6315789473684212) internal successors, (150), 148 states have internal predecessors, (150), 111 states have call successors, (111), 20 states have call predecessors, (111), 37 states have return successors, (399), 37 states have call predecessors, (399), 111 states have call successors, (399)
[2025-04-28 21:21:52,281 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 206 states to 206 states and 660 transitions.
[2025-04-28 21:21:52,281 INFO  L79                 Accepts]: Start accepts. Automaton has 206 states and 660 transitions. Word has length 36
[2025-04-28 21:21:52,281 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,281 INFO  L485      AbstractCegarLoop]: Abstraction has 206 states and 660 transitions.
[2025-04-28 21:21:52,281 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:52,282 INFO  L278                IsEmpty]: Start isEmpty. Operand 206 states and 660 transitions.
[2025-04-28 21:21:52,288 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:52,289 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,289 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,289 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:52,289 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,290 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,290 INFO  L85        PathProgramCache]: Analyzing trace with hash 1162119983, now seen corresponding path program 1 times
[2025-04-28 21:21:52,290 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,290 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1463274783]
[2025-04-28 21:21:52,290 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,290 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,315 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:52,333 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:52,333 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,333 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,479 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:52,480 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,480 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1463274783]
[2025-04-28 21:21:52,480 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1463274783] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,480 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,480 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:52,480 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [794419405]
[2025-04-28 21:21:52,480 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,480 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:52,481 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,481 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:52,481 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:52,481 INFO  L87              Difference]: Start difference. First operand 206 states and 660 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:53,177 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,177 INFO  L93              Difference]: Finished difference Result 226 states and 806 transitions.
[2025-04-28 21:21:53,178 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:53,178 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:53,178 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,186 INFO  L225             Difference]: With dead ends: 226
[2025-04-28 21:21:53,186 INFO  L226             Difference]: Without dead ends: 226
[2025-04-28 21:21:53,187 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:53,187 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 1 mSDsluCounter, 949 mSDsCounter, 0 mSdLazyCounter, 313 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1211 SdHoareTripleChecker+Invalid, 321 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 313 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,188 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1211 Invalid, 321 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 313 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:53,188 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 226 states.
[2025-04-28 21:21:53,245 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 226 to 216.
[2025-04-28 21:21:53,247 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 216 states, 62 states have (on average 2.5) internal successors, (155), 153 states have internal predecessors, (155), 111 states have call successors, (111), 20 states have call predecessors, (111), 42 states have return successors, (427), 42 states have call predecessors, (427), 111 states have call successors, (427)
[2025-04-28 21:21:53,253 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 216 states to 216 states and 693 transitions.
[2025-04-28 21:21:53,256 INFO  L79                 Accepts]: Start accepts. Automaton has 216 states and 693 transitions. Word has length 36
[2025-04-28 21:21:53,256 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,257 INFO  L485      AbstractCegarLoop]: Abstraction has 216 states and 693 transitions.
[2025-04-28 21:21:53,257 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:53,257 INFO  L278                IsEmpty]: Start isEmpty. Operand 216 states and 693 transitions.
[2025-04-28 21:21:53,266 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:53,266 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,266 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,266 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:53,267 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,267 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,267 INFO  L85        PathProgramCache]: Analyzing trace with hash -364054560, now seen corresponding path program 1 times
[2025-04-28 21:21:53,267 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,267 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1713753641]
[2025-04-28 21:21:53,267 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,267 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,291 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:53,306 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:53,306 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,306 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,422 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:53,422 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,423 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1713753641]
[2025-04-28 21:21:53,423 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1713753641] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,423 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,423 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:53,423 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1959506182]
[2025-04-28 21:21:53,423 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,423 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:53,423 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,424 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:53,424 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:53,424 INFO  L87              Difference]: Start difference. First operand 216 states and 693 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:54,059 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,060 INFO  L93              Difference]: Finished difference Result 224 states and 741 transitions.
[2025-04-28 21:21:54,060 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:54,061 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:54,061 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,066 INFO  L225             Difference]: With dead ends: 224
[2025-04-28 21:21:54,066 INFO  L226             Difference]: Without dead ends: 224
[2025-04-28 21:21:54,066 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:54,067 INFO  L437           NwaCegarLoop]: 261 mSDtfsCounter, 1 mSDsluCounter, 687 mSDsCounter, 0 mSdLazyCounter, 257 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 948 SdHoareTripleChecker+Invalid, 262 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 257 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,067 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 948 Invalid, 262 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 257 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:54,068 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 224 states.
[2025-04-28 21:21:54,127 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 224 to 218.
[2025-04-28 21:21:54,128 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 218 states, 63 states have (on average 2.4761904761904763) internal successors, (156), 154 states have internal predecessors, (156), 111 states have call successors, (111), 20 states have call predecessors, (111), 43 states have return successors, (429), 43 states have call predecessors, (429), 111 states have call successors, (429)
[2025-04-28 21:21:54,131 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 218 states to 218 states and 696 transitions.
[2025-04-28 21:21:54,132 INFO  L79                 Accepts]: Start accepts. Automaton has 218 states and 696 transitions. Word has length 36
[2025-04-28 21:21:54,132 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,132 INFO  L485      AbstractCegarLoop]: Abstraction has 218 states and 696 transitions.
[2025-04-28 21:21:54,132 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:54,132 INFO  L278                IsEmpty]: Start isEmpty. Operand 218 states and 696 transitions.
[2025-04-28 21:21:54,138 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:54,138 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,139 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,139 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:54,139 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,140 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,140 INFO  L85        PathProgramCache]: Analyzing trace with hash 1549917318, now seen corresponding path program 1 times
[2025-04-28 21:21:54,140 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,141 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [365142161]
[2025-04-28 21:21:54,141 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,141 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,162 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:54,173 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:54,174 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,174 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,276 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:54,276 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,276 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [365142161]
[2025-04-28 21:21:54,277 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [365142161] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,277 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,277 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:54,277 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [818718929]
[2025-04-28 21:21:54,277 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,277 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:54,277 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,278 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:54,278 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:54,278 INFO  L87              Difference]: Start difference. First operand 218 states and 696 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:54,985 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,985 INFO  L93              Difference]: Finished difference Result 238 states and 842 transitions.
[2025-04-28 21:21:54,986 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:54,986 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:54,987 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,993 INFO  L225             Difference]: With dead ends: 238
[2025-04-28 21:21:54,994 INFO  L226             Difference]: Without dead ends: 238
[2025-04-28 21:21:54,994 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:54,994 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 1 mSDsluCounter, 947 mSDsCounter, 0 mSdLazyCounter, 309 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1209 SdHoareTripleChecker+Invalid, 319 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 309 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,996 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1209 Invalid, 319 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 309 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:54,996 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 238 states.
[2025-04-28 21:21:55,046 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 238 to 218.
[2025-04-28 21:21:55,047 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 218 states, 63 states have (on average 2.4761904761904763) internal successors, (156), 154 states have internal predecessors, (156), 111 states have call successors, (111), 20 states have call predecessors, (111), 43 states have return successors, (429), 43 states have call predecessors, (429), 111 states have call successors, (429)
[2025-04-28 21:21:55,050 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 218 states to 218 states and 696 transitions.
[2025-04-28 21:21:55,050 INFO  L79                 Accepts]: Start accepts. Automaton has 218 states and 696 transitions. Word has length 36
[2025-04-28 21:21:55,050 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,052 INFO  L485      AbstractCegarLoop]: Abstraction has 218 states and 696 transitions.
[2025-04-28 21:21:55,052 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:55,052 INFO  L278                IsEmpty]: Start isEmpty. Operand 218 states and 696 transitions.
[2025-04-28 21:21:55,058 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:55,058 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,058 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,058 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:55,058 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,059 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,059 INFO  L85        PathProgramCache]: Analyzing trace with hash -2014001923, now seen corresponding path program 1 times
[2025-04-28 21:21:55,059 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,059 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1538436254]
[2025-04-28 21:21:55,059 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,059 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,082 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:55,097 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:55,097 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,097 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,185 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:55,185 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,185 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1538436254]
[2025-04-28 21:21:55,185 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1538436254] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,185 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,185 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:55,185 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [728427256]
[2025-04-28 21:21:55,185 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,186 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:55,187 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,187 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:55,187 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:55,187 INFO  L87              Difference]: Start difference. First operand 218 states and 696 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:55,847 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,847 INFO  L93              Difference]: Finished difference Result 226 states and 744 transitions.
[2025-04-28 21:21:55,851 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:55,852 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:55,852 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,858 INFO  L225             Difference]: With dead ends: 226
[2025-04-28 21:21:55,858 INFO  L226             Difference]: Without dead ends: 226
[2025-04-28 21:21:55,858 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:55,860 INFO  L437           NwaCegarLoop]: 261 mSDtfsCounter, 1 mSDsluCounter, 688 mSDsCounter, 0 mSdLazyCounter, 258 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 949 SdHoareTripleChecker+Invalid, 262 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 258 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,860 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 949 Invalid, 262 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 258 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:55,861 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 226 states.
[2025-04-28 21:21:55,903 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 226 to 218.
[2025-04-28 21:21:55,904 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 218 states, 63 states have (on average 2.4761904761904763) internal successors, (156), 154 states have internal predecessors, (156), 111 states have call successors, (111), 20 states have call predecessors, (111), 43 states have return successors, (429), 43 states have call predecessors, (429), 111 states have call successors, (429)
[2025-04-28 21:21:55,908 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 218 states to 218 states and 696 transitions.
[2025-04-28 21:21:55,908 INFO  L79                 Accepts]: Start accepts. Automaton has 218 states and 696 transitions. Word has length 36
[2025-04-28 21:21:55,909 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,909 INFO  L485      AbstractCegarLoop]: Abstraction has 218 states and 696 transitions.
[2025-04-28 21:21:55,909 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:55,910 INFO  L278                IsEmpty]: Start isEmpty. Operand 218 states and 696 transitions.
[2025-04-28 21:21:55,915 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:55,916 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,916 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,916 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:55,916 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,916 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,916 INFO  L85        PathProgramCache]: Analyzing trace with hash 175936994, now seen corresponding path program 1 times
[2025-04-28 21:21:55,916 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,917 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2091950249]
[2025-04-28 21:21:55,917 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,917 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,940 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:55,950 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:55,951 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,951 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,042 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:56,042 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,042 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2091950249]
[2025-04-28 21:21:56,042 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2091950249] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:56,042 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:56,043 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:56,043 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [882623347]
[2025-04-28 21:21:56,043 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,043 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:56,043 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,043 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:56,044 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:56,044 INFO  L87              Difference]: Start difference. First operand 218 states and 696 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:56,638 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,639 INFO  L93              Difference]: Finished difference Result 230 states and 751 transitions.
[2025-04-28 21:21:56,639 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:56,639 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:56,639 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,643 INFO  L225             Difference]: With dead ends: 230
[2025-04-28 21:21:56,643 INFO  L226             Difference]: Without dead ends: 230
[2025-04-28 21:21:56,644 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:56,644 INFO  L437           NwaCegarLoop]: 266 mSDtfsCounter, 1 mSDsluCounter, 704 mSDsCounter, 0 mSdLazyCounter, 259 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 970 SdHoareTripleChecker+Invalid, 261 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 259 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,644 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 970 Invalid, 261 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 259 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:56,645 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 230 states.
[2025-04-28 21:21:56,686 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 230 to 218.
[2025-04-28 21:21:56,690 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 218 states, 63 states have (on average 2.4761904761904763) internal successors, (156), 154 states have internal predecessors, (156), 111 states have call successors, (111), 20 states have call predecessors, (111), 43 states have return successors, (427), 43 states have call predecessors, (427), 111 states have call successors, (427)
[2025-04-28 21:21:56,693 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 218 states to 218 states and 694 transitions.
[2025-04-28 21:21:56,694 INFO  L79                 Accepts]: Start accepts. Automaton has 218 states and 694 transitions. Word has length 36
[2025-04-28 21:21:56,694 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,694 INFO  L485      AbstractCegarLoop]: Abstraction has 218 states and 694 transitions.
[2025-04-28 21:21:56,694 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:56,695 INFO  L278                IsEmpty]: Start isEmpty. Operand 218 states and 694 transitions.
[2025-04-28 21:21:56,700 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:56,700 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,700 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,701 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:56,701 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,701 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,701 INFO  L85        PathProgramCache]: Analyzing trace with hash 1998112828, now seen corresponding path program 1 times
[2025-04-28 21:21:56,701 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,701 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1985975460]
[2025-04-28 21:21:56,701 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,701 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,747 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:56,757 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:56,757 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,757 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,846 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:56,847 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,847 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1985975460]
[2025-04-28 21:21:56,847 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1985975460] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:56,847 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:56,847 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:56,847 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1194523438]
[2025-04-28 21:21:56,848 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,848 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:56,848 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,848 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:56,849 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:56,849 INFO  L87              Difference]: Start difference. First operand 218 states and 694 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:57,556 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,556 INFO  L93              Difference]: Finished difference Result 240 states and 878 transitions.
[2025-04-28 21:21:57,557 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:57,557 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:57,559 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,565 INFO  L225             Difference]: With dead ends: 240
[2025-04-28 21:21:57,565 INFO  L226             Difference]: Without dead ends: 240
[2025-04-28 21:21:57,566 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:57,567 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 1 mSDsluCounter, 943 mSDsCounter, 0 mSdLazyCounter, 305 mSolverCounterSat, 14 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 1205 SdHoareTripleChecker+Invalid, 319 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 14 IncrementalHoareTripleChecker+Valid, 305 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,567 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 1205 Invalid, 319 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [14 Valid, 305 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:57,568 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 240 states.
[2025-04-28 21:21:57,639 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 240 to 222.
[2025-04-28 21:21:57,640 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 222 states, 65 states have (on average 2.4307692307692306) internal successors, (158), 156 states have internal predecessors, (158), 111 states have call successors, (111), 20 states have call predecessors, (111), 45 states have return successors, (441), 45 states have call predecessors, (441), 111 states have call successors, (441)
[2025-04-28 21:21:57,643 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 222 states to 222 states and 710 transitions.
[2025-04-28 21:21:57,644 INFO  L79                 Accepts]: Start accepts. Automaton has 222 states and 710 transitions. Word has length 36
[2025-04-28 21:21:57,644 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,644 INFO  L485      AbstractCegarLoop]: Abstraction has 222 states and 710 transitions.
[2025-04-28 21:21:57,645 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:57,645 INFO  L278                IsEmpty]: Start isEmpty. Operand 222 states and 710 transitions.
[2025-04-28 21:21:57,649 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:57,650 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,650 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,650 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:57,650 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,650 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,650 INFO  L85        PathProgramCache]: Analyzing trace with hash -1555259643, now seen corresponding path program 1 times
[2025-04-28 21:21:57,651 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,651 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1785912233]
[2025-04-28 21:21:57,651 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,651 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,670 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:57,679 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:57,679 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,679 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,798 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:57,798 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,798 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1785912233]
[2025-04-28 21:21:57,798 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1785912233] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:57,798 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:57,798 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:57,798 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [373359153]
[2025-04-28 21:21:57,798 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,799 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:57,799 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,799 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:57,799 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:57,799 INFO  L87              Difference]: Start difference. First operand 222 states and 710 transitions. Second operand  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:59,000 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,000 INFO  L93              Difference]: Finished difference Result 294 states and 1054 transitions.
[2025-04-28 21:21:59,001 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:59,001 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9) Word has length 36
[2025-04-28 21:21:59,001 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,006 INFO  L225             Difference]: With dead ends: 294
[2025-04-28 21:21:59,006 INFO  L226             Difference]: Without dead ends: 294
[2025-04-28 21:21:59,006 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:59,007 INFO  L437           NwaCegarLoop]: 335 mSDtfsCounter, 31 mSDsluCounter, 1494 mSDsCounter, 0 mSdLazyCounter, 613 mSolverCounterSat, 45 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 62 SdHoareTripleChecker+Valid, 1829 SdHoareTripleChecker+Invalid, 658 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 45 IncrementalHoareTripleChecker+Valid, 613 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,007 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [62 Valid, 1829 Invalid, 658 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [45 Valid, 613 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-04-28 21:21:59,008 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 294 states.
[2025-04-28 21:21:59,062 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 294 to 274.
[2025-04-28 21:21:59,063 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 274 states, 78 states have (on average 2.551282051282051) internal successors, (199), 195 states have internal predecessors, (199), 140 states have call successors, (140), 23 states have call predecessors, (140), 55 states have return successors, (591), 55 states have call predecessors, (591), 140 states have call successors, (591)
[2025-04-28 21:21:59,067 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 274 states to 274 states and 930 transitions.
[2025-04-28 21:21:59,068 INFO  L79                 Accepts]: Start accepts. Automaton has 274 states and 930 transitions. Word has length 36
[2025-04-28 21:21:59,068 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,068 INFO  L485      AbstractCegarLoop]: Abstraction has 274 states and 930 transitions.
[2025-04-28 21:21:59,068 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:59,068 INFO  L278                IsEmpty]: Start isEmpty. Operand 274 states and 930 transitions.
[2025-04-28 21:21:59,075 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:59,075 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,075 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,075 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:59,075 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,076 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,076 INFO  L85        PathProgramCache]: Analyzing trace with hash 266052864, now seen corresponding path program 1 times
[2025-04-28 21:21:59,076 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,076 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1956577248]
[2025-04-28 21:21:59,076 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,076 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,097 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:59,108 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:59,108 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,108 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,230 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:59,230 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,230 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1956577248]
[2025-04-28 21:21:59,230 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1956577248] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,230 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:59,231 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:59,231 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [40835513]
[2025-04-28 21:21:59,231 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,231 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:59,231 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,232 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:59,232 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:59,232 INFO  L87              Difference]: Start difference. First operand 274 states and 930 transitions. Second operand  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:22:00,427 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,427 INFO  L93              Difference]: Finished difference Result 346 states and 1295 transitions.
[2025-04-28 21:22:00,428 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:00,428 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9) Word has length 36
[2025-04-28 21:22:00,428 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,435 INFO  L225             Difference]: With dead ends: 346
[2025-04-28 21:22:00,435 INFO  L226             Difference]: Without dead ends: 346
[2025-04-28 21:22:00,435 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:00,436 INFO  L437           NwaCegarLoop]: 339 mSDtfsCounter, 31 mSDsluCounter, 1511 mSDsCounter, 0 mSdLazyCounter, 609 mSolverCounterSat, 43 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 61 SdHoareTripleChecker+Valid, 1850 SdHoareTripleChecker+Invalid, 652 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 43 IncrementalHoareTripleChecker+Valid, 609 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,436 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [61 Valid, 1850 Invalid, 652 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [43 Valid, 609 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:22:00,437 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 346 states.
[2025-04-28 21:22:00,520 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 346 to 326.
[2025-04-28 21:22:00,522 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 326 states, 91 states have (on average 2.6263736263736264) internal successors, (239), 234 states have internal predecessors, (239), 169 states have call successors, (169), 26 states have call predecessors, (169), 65 states have return successors, (773), 65 states have call predecessors, (773), 169 states have call successors, (773)
[2025-04-28 21:22:00,527 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 326 states to 326 states and 1181 transitions.
[2025-04-28 21:22:00,527 INFO  L79                 Accepts]: Start accepts. Automaton has 326 states and 1181 transitions. Word has length 36
[2025-04-28 21:22:00,527 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,527 INFO  L485      AbstractCegarLoop]: Abstraction has 326 states and 1181 transitions.
[2025-04-28 21:22:00,527 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:22:00,528 INFO  L278                IsEmpty]: Start isEmpty. Operand 326 states and 1181 transitions.
[2025-04-28 21:22:00,535 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:00,536 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,536 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,536 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:22:00,536 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,538 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,538 INFO  L85        PathProgramCache]: Analyzing trace with hash -1166354232, now seen corresponding path program 1 times
[2025-04-28 21:22:00,538 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,538 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [596789974]
[2025-04-28 21:22:00,538 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,539 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,560 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:00,571 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:00,571 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,571 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,645 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:00,645 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,645 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [596789974]
[2025-04-28 21:22:00,645 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [596789974] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:00,645 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:00,645 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:00,645 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1582665702]
[2025-04-28 21:22:00,645 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,646 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:00,646 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,646 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:00,646 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:00,646 INFO  L87              Difference]: Start difference. First operand 326 states and 1181 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:01,289 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,290 INFO  L93              Difference]: Finished difference Result 342 states and 1241 transitions.
[2025-04-28 21:22:01,290 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:01,291 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:22:01,291 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,297 INFO  L225             Difference]: With dead ends: 342
[2025-04-28 21:22:01,297 INFO  L226             Difference]: Without dead ends: 342
[2025-04-28 21:22:01,298 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:01,298 INFO  L437           NwaCegarLoop]: 261 mSDtfsCounter, 1 mSDsluCounter, 689 mSDsCounter, 0 mSdLazyCounter, 259 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 950 SdHoareTripleChecker+Invalid, 262 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 259 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,299 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 950 Invalid, 262 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 259 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:01,300 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 342 states.
[2025-04-28 21:22:01,358 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 342 to 330.
[2025-04-28 21:22:01,360 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 330 states, 93 states have (on average 2.5913978494623655) internal successors, (241), 236 states have internal predecessors, (241), 169 states have call successors, (169), 26 states have call predecessors, (169), 67 states have return successors, (777), 67 states have call predecessors, (777), 169 states have call successors, (777)
[2025-04-28 21:22:01,365 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 330 states to 330 states and 1187 transitions.
[2025-04-28 21:22:01,365 INFO  L79                 Accepts]: Start accepts. Automaton has 330 states and 1187 transitions. Word has length 36
[2025-04-28 21:22:01,366 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,366 INFO  L485      AbstractCegarLoop]: Abstraction has 330 states and 1187 transitions.
[2025-04-28 21:22:01,366 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:01,366 INFO  L278                IsEmpty]: Start isEmpty. Operand 330 states and 1187 transitions.
[2025-04-28 21:22:01,374 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:01,374 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,374 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,375 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:22:01,375 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,375 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,375 INFO  L85        PathProgramCache]: Analyzing trace with hash -1588113721, now seen corresponding path program 1 times
[2025-04-28 21:22:01,376 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,376 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [376496657]
[2025-04-28 21:22:01,376 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,376 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,402 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:01,414 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:01,415 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,415 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,529 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:01,529 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,529 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [376496657]
[2025-04-28 21:22:01,529 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [376496657] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:01,529 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:01,530 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:01,530 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1752080184]
[2025-04-28 21:22:01,530 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,530 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:01,531 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,531 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:01,531 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:01,531 INFO  L87              Difference]: Start difference. First operand 330 states and 1187 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:02,126 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,126 INFO  L93              Difference]: Finished difference Result 362 states and 1397 transitions.
[2025-04-28 21:22:02,127 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:02,127 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:22:02,127 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,133 INFO  L225             Difference]: With dead ends: 362
[2025-04-28 21:22:02,133 INFO  L226             Difference]: Without dead ends: 362
[2025-04-28 21:22:02,134 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:02,134 INFO  L437           NwaCegarLoop]: 265 mSDtfsCounter, 1 mSDsluCounter, 1000 mSDsCounter, 0 mSdLazyCounter, 259 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1265 SdHoareTripleChecker+Invalid, 280 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 259 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,134 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1265 Invalid, 280 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 259 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:02,135 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 362 states.
[2025-04-28 21:22:02,200 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 362 to 330.
[2025-04-28 21:22:02,202 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 330 states, 93 states have (on average 2.5913978494623655) internal successors, (241), 236 states have internal predecessors, (241), 169 states have call successors, (169), 26 states have call predecessors, (169), 67 states have return successors, (777), 67 states have call predecessors, (777), 169 states have call successors, (777)
[2025-04-28 21:22:02,207 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 330 states to 330 states and 1187 transitions.
[2025-04-28 21:22:02,207 INFO  L79                 Accepts]: Start accepts. Automaton has 330 states and 1187 transitions. Word has length 36
[2025-04-28 21:22:02,207 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:02,207 INFO  L485      AbstractCegarLoop]: Abstraction has 330 states and 1187 transitions.
[2025-04-28 21:22:02,207 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:02,208 INFO  L278                IsEmpty]: Start isEmpty. Operand 330 states and 1187 transitions.
[2025-04-28 21:22:02,214 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:02,214 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:02,214 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:02,215 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:22:02,215 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,215 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,215 INFO  L85        PathProgramCache]: Analyzing trace with hash -931727702, now seen corresponding path program 1 times
[2025-04-28 21:22:02,216 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,216 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [477725052]
[2025-04-28 21:22:02,216 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:02,216 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,237 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:02,247 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:02,248 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,248 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,359 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:02,359 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,359 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [477725052]
[2025-04-28 21:22:02,359 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [477725052] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:02,359 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:02,359 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:02,359 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [396865437]
[2025-04-28 21:22:02,359 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:02,360 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:02,361 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:02,361 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:02,361 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:02,361 INFO  L87              Difference]: Start difference. First operand 330 states and 1187 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:02,921 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,922 INFO  L93              Difference]: Finished difference Result 362 states and 1397 transitions.
[2025-04-28 21:22:02,922 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:02,922 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:22:02,923 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,929 INFO  L225             Difference]: With dead ends: 362
[2025-04-28 21:22:02,929 INFO  L226             Difference]: Without dead ends: 362
[2025-04-28 21:22:02,930 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:02,930 INFO  L437           NwaCegarLoop]: 265 mSDtfsCounter, 1 mSDsluCounter, 1000 mSDsCounter, 0 mSdLazyCounter, 259 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1265 SdHoareTripleChecker+Invalid, 280 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 259 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,930 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1265 Invalid, 280 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 259 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:22:02,931 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 362 states.
[2025-04-28 21:22:02,997 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 362 to 330.
[2025-04-28 21:22:02,998 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 330 states, 93 states have (on average 2.5913978494623655) internal successors, (241), 236 states have internal predecessors, (241), 169 states have call successors, (169), 26 states have call predecessors, (169), 67 states have return successors, (777), 67 states have call predecessors, (777), 169 states have call successors, (777)
[2025-04-28 21:22:03,003 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 330 states to 330 states and 1187 transitions.
[2025-04-28 21:22:03,003 INFO  L79                 Accepts]: Start accepts. Automaton has 330 states and 1187 transitions. Word has length 36
[2025-04-28 21:22:03,003 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,003 INFO  L485      AbstractCegarLoop]: Abstraction has 330 states and 1187 transitions.
[2025-04-28 21:22:03,003 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:03,003 INFO  L278                IsEmpty]: Start isEmpty. Operand 330 states and 1187 transitions.
[2025-04-28 21:22:03,009 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:03,009 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,010 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,010 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-04-28 21:22:03,010 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,010 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,010 INFO  L85        PathProgramCache]: Analyzing trace with hash -945973266, now seen corresponding path program 1 times
[2025-04-28 21:22:03,010 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,010 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1536518578]
[2025-04-28 21:22:03,011 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:03,011 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,032 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:03,041 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:03,041 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,041 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,136 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:03,136 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,137 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1536518578]
[2025-04-28 21:22:03,137 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1536518578] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:03,137 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:03,137 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:03,137 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [111072639]
[2025-04-28 21:22:03,137 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,137 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:03,137 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,138 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:03,138 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:03,138 INFO  L87              Difference]: Start difference. First operand 330 states and 1187 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:03,729 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,730 INFO  L93              Difference]: Finished difference Result 366 states and 1318 transitions.
[2025-04-28 21:22:03,730 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:03,731 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:22:03,731 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,737 INFO  L225             Difference]: With dead ends: 366
[2025-04-28 21:22:03,738 INFO  L226             Difference]: Without dead ends: 366
[2025-04-28 21:22:03,738 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:03,738 INFO  L437           NwaCegarLoop]: 266 mSDtfsCounter, 1 mSDsluCounter, 702 mSDsCounter, 0 mSdLazyCounter, 261 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 968 SdHoareTripleChecker+Invalid, 265 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 261 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,739 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 968 Invalid, 265 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 261 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:03,740 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 366 states.
[2025-04-28 21:22:03,800 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 366 to 338.
[2025-04-28 21:22:03,802 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 338 states, 97 states have (on average 2.5257731958762886) internal successors, (245), 240 states have internal predecessors, (245), 169 states have call successors, (169), 26 states have call predecessors, (169), 71 states have return successors, (861), 71 states have call predecessors, (861), 169 states have call successors, (861)
[2025-04-28 21:22:03,808 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 338 states to 338 states and 1275 transitions.
[2025-04-28 21:22:03,808 INFO  L79                 Accepts]: Start accepts. Automaton has 338 states and 1275 transitions. Word has length 36
[2025-04-28 21:22:03,809 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,809 INFO  L485      AbstractCegarLoop]: Abstraction has 338 states and 1275 transitions.
[2025-04-28 21:22:03,809 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:03,809 INFO  L278                IsEmpty]: Start isEmpty. Operand 338 states and 1275 transitions.
[2025-04-28 21:22:03,816 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:03,816 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,816 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,816 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-04-28 21:22:03,817 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,817 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,817 INFO  L85        PathProgramCache]: Analyzing trace with hash -243629131, now seen corresponding path program 1 times
[2025-04-28 21:22:03,818 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,818 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1042688257]
[2025-04-28 21:22:03,818 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:03,818 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,844 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:03,854 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:03,854 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,854 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,949 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:03,950 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,950 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1042688257]
[2025-04-28 21:22:03,950 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1042688257] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:03,950 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:03,950 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:03,950 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [655202345]
[2025-04-28 21:22:03,950 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,951 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:03,951 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,952 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:03,952 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:03,952 INFO  L87              Difference]: Start difference. First operand 338 states and 1275 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:04,665 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,665 INFO  L93              Difference]: Finished difference Result 378 states and 1552 transitions.
[2025-04-28 21:22:04,666 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:04,666 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:22:04,666 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,674 INFO  L225             Difference]: With dead ends: 378
[2025-04-28 21:22:04,674 INFO  L226             Difference]: Without dead ends: 378
[2025-04-28 21:22:04,674 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:04,675 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 1 mSDsluCounter, 903 mSDsCounter, 0 mSdLazyCounter, 313 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1151 SdHoareTripleChecker+Invalid, 321 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 313 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,675 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1151 Invalid, 321 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 313 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:04,676 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 378 states.
[2025-04-28 21:22:04,770 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 378 to 348.
[2025-04-28 21:22:04,772 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 348 states, 102 states have (on average 2.450980392156863) internal successors, (250), 245 states have internal predecessors, (250), 169 states have call successors, (169), 26 states have call predecessors, (169), 76 states have return successors, (930), 76 states have call predecessors, (930), 169 states have call successors, (930)
[2025-04-28 21:22:04,776 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 348 states to 348 states and 1349 transitions.
[2025-04-28 21:22:04,777 INFO  L79                 Accepts]: Start accepts. Automaton has 348 states and 1349 transitions. Word has length 36
[2025-04-28 21:22:04,777 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,777 INFO  L485      AbstractCegarLoop]: Abstraction has 348 states and 1349 transitions.
[2025-04-28 21:22:04,777 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:04,777 INFO  L278                IsEmpty]: Start isEmpty. Operand 348 states and 1349 transitions.
[2025-04-28 21:22:04,784 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:04,784 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,784 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:04,785 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-04-28 21:22:04,785 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,786 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,786 INFO  L85        PathProgramCache]: Analyzing trace with hash -972539623, now seen corresponding path program 1 times
[2025-04-28 21:22:04,786 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,786 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [533706734]
[2025-04-28 21:22:04,786 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:04,787 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,805 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:04,814 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:04,814 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,815 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,913 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:04,914 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,914 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [533706734]
[2025-04-28 21:22:04,915 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [533706734] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:04,915 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:04,915 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:04,915 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [782496283]
[2025-04-28 21:22:04,915 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:04,915 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:04,915 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:04,916 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:04,916 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:04,916 INFO  L87              Difference]: Start difference. First operand 348 states and 1349 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:05,522 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:05,523 INFO  L93              Difference]: Finished difference Result 382 states and 1562 transitions.
[2025-04-28 21:22:05,524 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:05,524 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:22:05,524 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:05,532 INFO  L225             Difference]: With dead ends: 382
[2025-04-28 21:22:05,532 INFO  L226             Difference]: Without dead ends: 382
[2025-04-28 21:22:05,532 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:05,533 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 1 mSDsluCounter, 988 mSDsCounter, 0 mSdLazyCounter, 259 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1250 SdHoareTripleChecker+Invalid, 280 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 259 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:05,533 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1250 Invalid, 280 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 259 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:05,534 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 382 states.
[2025-04-28 21:22:05,609 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 382 to 348.
[2025-04-28 21:22:05,610 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 348 states, 102 states have (on average 2.450980392156863) internal successors, (250), 245 states have internal predecessors, (250), 169 states have call successors, (169), 26 states have call predecessors, (169), 76 states have return successors, (930), 76 states have call predecessors, (930), 169 states have call successors, (930)
[2025-04-28 21:22:05,615 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 348 states to 348 states and 1349 transitions.
[2025-04-28 21:22:05,615 INFO  L79                 Accepts]: Start accepts. Automaton has 348 states and 1349 transitions. Word has length 36
[2025-04-28 21:22:05,615 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:05,615 INFO  L485      AbstractCegarLoop]: Abstraction has 348 states and 1349 transitions.
[2025-04-28 21:22:05,616 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:05,617 INFO  L278                IsEmpty]: Start isEmpty. Operand 348 states and 1349 transitions.
[2025-04-28 21:22:05,624 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:05,624 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:05,624 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:05,624 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-04-28 21:22:05,624 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:05,625 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:05,625 INFO  L85        PathProgramCache]: Analyzing trace with hash 1485954431, now seen corresponding path program 1 times
[2025-04-28 21:22:05,625 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:05,625 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [401787078]
[2025-04-28 21:22:05,625 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:05,625 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:05,647 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:05,657 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:05,658 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:05,658 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:05,745 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:05,746 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:05,746 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [401787078]
[2025-04-28 21:22:05,746 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [401787078] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:05,746 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:05,746 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:05,746 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [78155985]
[2025-04-28 21:22:05,746 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,747 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:05,747 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,747 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:05,747 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:05,748 INFO  L87              Difference]: Start difference. First operand 348 states and 1349 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:06,389 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,389 INFO  L93              Difference]: Finished difference Result 386 states and 1614 transitions.
[2025-04-28 21:22:06,390 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:06,390 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:22:06,390 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,397 INFO  L225             Difference]: With dead ends: 386
[2025-04-28 21:22:06,397 INFO  L226             Difference]: Without dead ends: 386
[2025-04-28 21:22:06,398 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:06,399 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 1 mSDsluCounter, 949 mSDsCounter, 0 mSdLazyCounter, 313 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1211 SdHoareTripleChecker+Invalid, 321 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 313 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,399 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1211 Invalid, 321 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 313 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:06,400 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 386 states.
[2025-04-28 21:22:06,475 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 386 to 338.
[2025-04-28 21:22:06,476 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 338 states, 97 states have (on average 2.5257731958762886) internal successors, (245), 240 states have internal predecessors, (245), 169 states have call successors, (169), 26 states have call predecessors, (169), 71 states have return successors, (872), 71 states have call predecessors, (872), 169 states have call successors, (872)
[2025-04-28 21:22:06,480 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 338 states to 338 states and 1286 transitions.
[2025-04-28 21:22:06,480 INFO  L79                 Accepts]: Start accepts. Automaton has 338 states and 1286 transitions. Word has length 36
[2025-04-28 21:22:06,481 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,481 INFO  L485      AbstractCegarLoop]: Abstraction has 338 states and 1286 transitions.
[2025-04-28 21:22:06,481 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:06,481 INFO  L278                IsEmpty]: Start isEmpty. Operand 338 states and 1286 transitions.
[2025-04-28 21:22:06,487 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:06,488 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,488 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:06,488 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-04-28 21:22:06,488 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,488 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,489 INFO  L85        PathProgramCache]: Analyzing trace with hash 1163617252, now seen corresponding path program 1 times
[2025-04-28 21:22:06,489 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,489 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2144464682]
[2025-04-28 21:22:06,489 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,489 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,506 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:06,515 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:06,515 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,515 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,581 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:06,582 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,582 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2144464682]
[2025-04-28 21:22:06,582 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2144464682] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:06,582 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:06,582 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:06,582 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [156712277]
[2025-04-28 21:22:06,582 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:06,583 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:06,583 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:06,583 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:06,583 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:06,583 INFO  L87              Difference]: Start difference. First operand 338 states and 1286 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:07,370 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,370 INFO  L93              Difference]: Finished difference Result 370 states and 1406 transitions.
[2025-04-28 21:22:07,371 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:07,371 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:22:07,371 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,377 INFO  L225             Difference]: With dead ends: 370
[2025-04-28 21:22:07,377 INFO  L226             Difference]: Without dead ends: 370
[2025-04-28 21:22:07,377 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:07,378 INFO  L437           NwaCegarLoop]: 261 mSDtfsCounter, 1 mSDsluCounter, 688 mSDsCounter, 0 mSdLazyCounter, 258 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 949 SdHoareTripleChecker+Invalid, 262 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 258 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,378 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 949 Invalid, 262 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 258 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:07,379 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 370 states.
[2025-04-28 21:22:07,458 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 370 to 340.
[2025-04-28 21:22:07,460 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 340 states, 98 states have (on average 2.510204081632653) internal successors, (246), 241 states have internal predecessors, (246), 169 states have call successors, (169), 26 states have call predecessors, (169), 72 states have return successors, (882), 72 states have call predecessors, (882), 169 states have call successors, (882)
[2025-04-28 21:22:07,464 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 340 states to 340 states and 1297 transitions.
[2025-04-28 21:22:07,464 INFO  L79                 Accepts]: Start accepts. Automaton has 340 states and 1297 transitions. Word has length 36
[2025-04-28 21:22:07,465 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,465 INFO  L485      AbstractCegarLoop]: Abstraction has 340 states and 1297 transitions.
[2025-04-28 21:22:07,465 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:22:07,465 INFO  L278                IsEmpty]: Start isEmpty. Operand 340 states and 1297 transitions.
[2025-04-28 21:22:07,472 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:07,472 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,472 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:07,472 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-04-28 21:22:07,472 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,474 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,474 INFO  L85        PathProgramCache]: Analyzing trace with hash 2009083059, now seen corresponding path program 1 times
[2025-04-28 21:22:07,474 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,474 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1936328414]
[2025-04-28 21:22:07,474 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,474 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,492 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:07,500 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:07,501 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,501 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,608 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:07,608 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,608 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1936328414]
[2025-04-28 21:22:07,608 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1936328414] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:07,609 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:07,609 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:07,609 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [537423678]
[2025-04-28 21:22:07,609 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,609 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:07,609 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,610 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:07,610 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:07,610 INFO  L87              Difference]: Start difference. First operand 340 states and 1297 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
