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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:50,094 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:50,197 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_28bcb8a3-4bb6-4715-a1e1-f78ff86905cd/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:50,208 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:50,208 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:50,250 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:50,251 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:50,252 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:50,253 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:50,253 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:50,254 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:50,254 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:50,254 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:50,255 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:50,255 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:50,256 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:50,257 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:50,257 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:50,257 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:50,257 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:50,257 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:50,257 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:50,257 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:50,257 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:50,258 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:50,259 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:50,259 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:50,609 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:50,623 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:50,626 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:50,627 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:50,628 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:50,629 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_28bcb8a3-4bb6-4715-a1e1-f78ff86905cd/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-220.smt2
[2025-04-28 21:21:50,633 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:50,637 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:51,607 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_28bcb8a3-4bb6-4715-a1e1-f78ff86905cd/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-220.smt2
[2025-04-28 21:21:51,611 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:51,612 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:51,613 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:51,613 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:51,613 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:51,616 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,685 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51 Unit
[2025-04-28 21:21:51,685 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:51,686 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:51,686 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:51,686 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:51,702 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,703 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,753 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,753 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,792 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,796 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,803 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,812 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,819 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,853 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:51,853 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:51,854 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:51,854 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:51,855 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,861 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:51,882 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:51,899 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:51,906 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:51,922 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:51,922 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:51,922 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:51,922 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main466 given in one single declaration
[2025-04-28 21:21:51,923 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main466
[2025-04-28 21:21:51,923 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main466
[2025-04-28 21:21:51,923 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main114 given in one single declaration
[2025-04-28 21:21:51,923 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main114
[2025-04-28 21:21:51,923 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main114
[2025-04-28 21:21:51,923 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main108 given in one single declaration
[2025-04-28 21:21:51,923 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main108
[2025-04-28 21:21:51,923 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main108
[2025-04-28 21:21:51,923 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main3 given in one single declaration
[2025-04-28 21:21:51,923 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main3
[2025-04-28 21:21:51,924 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main3
[2025-04-28 21:21:51,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main193 given in one single declaration
[2025-04-28 21:21:51,925 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main193
[2025-04-28 21:21:51,925 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main193
[2025-04-28 21:21:51,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main199 given in one single declaration
[2025-04-28 21:21:51,926 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main199
[2025-04-28 21:21:51,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main199
[2025-04-28 21:21:51,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main239 given in one single declaration
[2025-04-28 21:21:51,926 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main239
[2025-04-28 21:21:51,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main239
[2025-04-28 21:21:51,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main235 given in one single declaration
[2025-04-28 21:21:51,926 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main235
[2025-04-28 21:21:51,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main235
[2025-04-28 21:21:51,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main377 given in one single declaration
[2025-04-28 21:21:51,926 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main377
[2025-04-28 21:21:51,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main377
[2025-04-28 21:21:51,927 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main267 given in one single declaration
[2025-04-28 21:21:51,927 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main267
[2025-04-28 21:21:51,927 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main267
[2025-04-28 21:21:51,927 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main256 given in one single declaration
[2025-04-28 21:21:51,928 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main256
[2025-04-28 21:21:51,928 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main256
[2025-04-28 21:21:51,928 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main449 given in one single declaration
[2025-04-28 21:21:51,928 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main449
[2025-04-28 21:21:51,928 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main449
[2025-04-28 21:21:51,928 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:51,928 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:51,928 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:52,232 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:52,235 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:53,389 INFO  L?                        ?]: Removed 167 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:53,389 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:53,410 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:53,410 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:53,410 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:53 BoogieIcfgContainer
[2025-04-28 21:21:53,410 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:53,417 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:53,417 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:53,421 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:53,422 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:51" (1/3) ...
[2025-04-28 21:21:53,422 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@9939fc and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:53, skipping insertion in model container
[2025-04-28 21:21:53,422 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (2/3) ...
[2025-04-28 21:21:53,422 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@9939fc and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:53, skipping insertion in model container
[2025-04-28 21:21:53,423 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:53" (3/3) ...
[2025-04-28 21:21:53,424 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:53,439 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:53,441 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 14 procedures, 121 locations, 331 edges, 14 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:53,498 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:53,521 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;@4a33cc95, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:53,521 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:53,528 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 121 states, 27 states have (on average 3.4814814814814814) internal successors, (94), 94 states have internal predecessors, (94), 79 states have call successors, (79), 13 states have call predecessors, (79), 13 states have return successors, (79), 13 states have call predecessors, (79), 79 states have call successors, (79)
[2025-04-28 21:21:53,556 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:53,556 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,557 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]
[2025-04-28 21:21:53,557 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,562 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,563 INFO  L85        PathProgramCache]: Analyzing trace with hash 1244959581, now seen corresponding path program 1 times
[2025-04-28 21:21:53,569 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,570 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [815198992]
[2025-04-28 21:21:53,570 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,570 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,624 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:53,706 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:53,707 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,707 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,029 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:54,030 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,030 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [815198992]
[2025-04-28 21:21:54,031 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [815198992] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,031 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,034 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:54,035 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [944420836]
[2025-04-28 21:21:54,036 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,040 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:54,040 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,068 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:54,069 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:54,073 INFO  L87              Difference]: Start difference. First operand  has 121 states, 27 states have (on average 3.4814814814814814) internal successors, (94), 94 states have internal predecessors, (94), 79 states have call successors, (79), 13 states have call predecessors, (79), 13 states have return successors, (79), 13 states have call predecessors, (79), 79 states have call successors, (79) Second operand  has 5 states, 4 states have (on average 2.5) internal successors, (10), 5 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:55,037 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,037 INFO  L93              Difference]: Finished difference Result 121 states and 296 transitions.
[2025-04-28 21:21:55,039 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:55,040 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 2.5) internal successors, (10), 5 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:55,041 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,052 INFO  L225             Difference]: With dead ends: 121
[2025-04-28 21:21:55,052 INFO  L226             Difference]: Without dead ends: 121
[2025-04-28 21:21:55,054 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,057 INFO  L437           NwaCegarLoop]: 201 mSDtfsCounter, 1 mSDsluCounter, 538 mSDsCounter, 0 mSdLazyCounter, 246 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 739 SdHoareTripleChecker+Invalid, 252 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 246 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,058 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 739 Invalid, 252 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [6 Valid, 246 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:55,072 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 121 states.
[2025-04-28 21:21:55,126 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 121 to 121.
[2025-04-28 21:21:55,127 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 121 states, 27 states have (on average 3.4444444444444446) internal successors, (93), 93 states have internal predecessors, (93), 79 states have call successors, (79), 13 states have call predecessors, (79), 14 states have return successors, (124), 14 states have call predecessors, (124), 79 states have call successors, (124)
[2025-04-28 21:21:55,133 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 121 states to 121 states and 296 transitions.
[2025-04-28 21:21:55,134 INFO  L79                 Accepts]: Start accepts. Automaton has 121 states and 296 transitions. Word has length 20
[2025-04-28 21:21:55,135 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,135 INFO  L485      AbstractCegarLoop]: Abstraction has 121 states and 296 transitions.
[2025-04-28 21:21:55,135 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 2.5) internal successors, (10), 5 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:55,136 INFO  L278                IsEmpty]: Start isEmpty. Operand 121 states and 296 transitions.
[2025-04-28 21:21:55,142 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:55,143 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,143 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]
[2025-04-28 21:21:55,143 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:55,143 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,144 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,144 INFO  L85        PathProgramCache]: Analyzing trace with hash 379419455, now seen corresponding path program 1 times
[2025-04-28 21:21:55,145 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,145 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1895521238]
[2025-04-28 21:21:55,145 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,145 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,174 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:55,194 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:55,194 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,194 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,393 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,394 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,395 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1895521238]
[2025-04-28 21:21:55,395 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1895521238] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,395 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,395 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:55,395 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1032947508]
[2025-04-28 21:21:55,395 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,396 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:55,397 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,398 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:55,398 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:55,399 INFO  L87              Difference]: Start difference. First operand 121 states and 296 transitions. Second operand  has 5 states, 4 states have (on average 3.5) internal successors, (14), 5 states have internal predecessors, (14), 3 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:56,251 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,252 INFO  L93              Difference]: Finished difference Result 127 states and 350 transitions.
[2025-04-28 21:21:56,253 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:56,253 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 3.5) internal successors, (14), 5 states have internal predecessors, (14), 3 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 3 states have call successors, (7) Word has length 28
[2025-04-28 21:21:56,254 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,257 INFO  L225             Difference]: With dead ends: 127
[2025-04-28 21:21:56,258 INFO  L226             Difference]: Without dead ends: 127
[2025-04-28 21:21:56,258 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,259 INFO  L437           NwaCegarLoop]: 253 mSDtfsCounter, 1 mSDsluCounter, 651 mSDsCounter, 0 mSdLazyCounter, 293 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 904 SdHoareTripleChecker+Invalid, 297 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 293 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,259 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 904 Invalid, 297 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 293 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:56,260 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 127 states.
[2025-04-28 21:21:56,307 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 127 to 125.
[2025-04-28 21:21:56,309 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 29 states have (on average 3.2758620689655173) internal successors, (95), 95 states have internal predecessors, (95), 79 states have call successors, (79), 13 states have call predecessors, (79), 16 states have return successors, (174), 16 states have call predecessors, (174), 79 states have call successors, (174)
[2025-04-28 21:21:56,313 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 348 transitions.
[2025-04-28 21:21:56,316 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 348 transitions. Word has length 28
[2025-04-28 21:21:56,316 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,316 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 348 transitions.
[2025-04-28 21:21:56,317 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 3.5) internal successors, (14), 5 states have internal predecessors, (14), 3 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:56,317 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 348 transitions.
[2025-04-28 21:21:56,321 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:56,321 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,321 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]
[2025-04-28 21:21:56,321 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:56,321 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,322 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,322 INFO  L85        PathProgramCache]: Analyzing trace with hash 1643164575, now seen corresponding path program 1 times
[2025-04-28 21:21:56,322 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,322 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1237224272]
[2025-04-28 21:21:56,322 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,322 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,352 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:56,370 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:56,370 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,370 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,488 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,488 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,488 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1237224272]
[2025-04-28 21:21:56,488 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1237224272] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:56,488 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:56,488 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:56,488 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [599629683]
[2025-04-28 21:21:56,488 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,489 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:56,489 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,489 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:56,489 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:56,489 INFO  L87              Difference]: Start difference. First operand 125 states and 348 transitions. Second operand  has 5 states, 4 states have (on average 3.5) internal successors, (14), 5 states have internal predecessors, (14), 3 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:57,196 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,196 INFO  L93              Difference]: Finished difference Result 127 states and 323 transitions.
[2025-04-28 21:21:57,197 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:57,197 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 3.5) internal successors, (14), 5 states have internal predecessors, (14), 3 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 3 states have call successors, (7) Word has length 28
[2025-04-28 21:21:57,197 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,200 INFO  L225             Difference]: With dead ends: 127
[2025-04-28 21:21:57,200 INFO  L226             Difference]: Without dead ends: 127
[2025-04-28 21:21:57,201 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:57,201 INFO  L437           NwaCegarLoop]: 233 mSDtfsCounter, 1 mSDsluCounter, 575 mSDsCounter, 0 mSdLazyCounter, 141 mSolverCounterSat, 62 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 33 SdHoareTripleChecker+Valid, 808 SdHoareTripleChecker+Invalid, 203 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 62 IncrementalHoareTripleChecker+Valid, 141 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,202 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [33 Valid, 808 Invalid, 203 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [62 Valid, 141 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:57,202 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 127 states.
[2025-04-28 21:21:57,220 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 127 to 125.
[2025-04-28 21:21:57,221 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 29 states have (on average 3.2758620689655173) internal successors, (95), 95 states have internal predecessors, (95), 79 states have call successors, (79), 13 states have call predecessors, (79), 16 states have return successors, (144), 16 states have call predecessors, (144), 79 states have call successors, (144)
[2025-04-28 21:21:57,223 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 318 transitions.
[2025-04-28 21:21:57,224 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 318 transitions. Word has length 28
[2025-04-28 21:21:57,224 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,224 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 318 transitions.
[2025-04-28 21:21:57,224 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 3.5) internal successors, (14), 5 states have internal predecessors, (14), 3 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:57,224 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 318 transitions.
[2025-04-28 21:21:57,228 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:57,228 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,228 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:57,229 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:57,229 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,229 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,230 INFO  L85        PathProgramCache]: Analyzing trace with hash -1739466638, now seen corresponding path program 1 times
[2025-04-28 21:21:57,230 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,230 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1903177026]
[2025-04-28 21:21:57,230 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,230 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,261 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:57,287 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:57,288 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,288 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,550 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,550 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,550 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1903177026]
[2025-04-28 21:21:57,550 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1903177026] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:57,551 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:57,551 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:57,551 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [263811994]
[2025-04-28 21:21:57,551 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,551 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:57,551 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,552 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:57,552 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:57,552 INFO  L87              Difference]: Start difference. First operand 125 states and 318 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:58,240 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,240 INFO  L93              Difference]: Finished difference Result 133 states and 420 transitions.
[2025-04-28 21:21:58,241 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:58,241 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:58,241 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,244 INFO  L225             Difference]: With dead ends: 133
[2025-04-28 21:21:58,245 INFO  L226             Difference]: Without dead ends: 133
[2025-04-28 21:21:58,245 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:58,245 INFO  L437           NwaCegarLoop]: 251 mSDtfsCounter, 1 mSDsluCounter, 685 mSDsCounter, 0 mSdLazyCounter, 229 mSolverCounterSat, 31 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 936 SdHoareTripleChecker+Invalid, 260 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 31 IncrementalHoareTripleChecker+Valid, 229 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,246 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 936 Invalid, 260 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [31 Valid, 229 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:58,247 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-04-28 21:21:58,287 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 129.
[2025-04-28 21:21:58,288 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 129 states, 31 states have (on average 3.129032258064516) internal successors, (97), 97 states have internal predecessors, (97), 79 states have call successors, (79), 13 states have call predecessors, (79), 18 states have return successors, (193), 18 states have call predecessors, (193), 79 states have call successors, (193)
[2025-04-28 21:21:58,292 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 129 states to 129 states and 369 transitions.
[2025-04-28 21:21:58,292 INFO  L79                 Accepts]: Start accepts. Automaton has 129 states and 369 transitions. Word has length 32
[2025-04-28 21:21:58,293 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,293 INFO  L485      AbstractCegarLoop]: Abstraction has 129 states and 369 transitions.
[2025-04-28 21:21:58,293 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:58,293 INFO  L278                IsEmpty]: Start isEmpty. Operand 129 states and 369 transitions.
[2025-04-28 21:21:58,299 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:58,299 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,299 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:58,299 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:58,299 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,301 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,301 INFO  L85        PathProgramCache]: Analyzing trace with hash -1795833616, now seen corresponding path program 1 times
[2025-04-28 21:21:58,302 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,302 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1685343710]
[2025-04-28 21:21:58,302 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,302 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,333 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:58,351 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:58,351 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,351 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,497 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:58,498 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,498 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1685343710]
[2025-04-28 21:21:58,498 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1685343710] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:58,498 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:58,498 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:58,498 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [792222113]
[2025-04-28 21:21:58,498 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,498 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:58,499 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,499 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:58,499 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:58,499 INFO  L87              Difference]: Start difference. First operand 129 states and 369 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:59,328 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,329 INFO  L93              Difference]: Finished difference Result 133 states and 420 transitions.
[2025-04-28 21:21:59,329 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:59,329 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:59,329 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,332 INFO  L225             Difference]: With dead ends: 133
[2025-04-28 21:21:59,332 INFO  L226             Difference]: Without dead ends: 133
[2025-04-28 21:21:59,332 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:59,333 INFO  L437           NwaCegarLoop]: 251 mSDtfsCounter, 1 mSDsluCounter, 644 mSDsCounter, 0 mSdLazyCounter, 292 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 895 SdHoareTripleChecker+Invalid, 298 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 292 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,333 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 895 Invalid, 298 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 292 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:59,334 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-04-28 21:21:59,365 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 133.
[2025-04-28 21:21:59,366 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 33 states have (on average 3.0) internal successors, (99), 99 states have internal predecessors, (99), 79 states have call successors, (79), 13 states have call predecessors, (79), 20 states have return successors, (242), 20 states have call predecessors, (242), 79 states have call successors, (242)
[2025-04-28 21:21:59,368 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 420 transitions.
[2025-04-28 21:21:59,369 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 420 transitions. Word has length 32
[2025-04-28 21:21:59,369 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,369 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 420 transitions.
[2025-04-28 21:21:59,369 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:59,369 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 420 transitions.
[2025-04-28 21:21:59,375 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:59,375 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,375 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:59,375 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:59,375 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,376 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,376 INFO  L85        PathProgramCache]: Analyzing trace with hash 1779333002, now seen corresponding path program 1 times
[2025-04-28 21:21:59,376 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,376 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1123710559]
[2025-04-28 21:21:59,376 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,377 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,408 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:59,424 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:59,424 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,424 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,542 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,542 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,542 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1123710559]
[2025-04-28 21:21:59,542 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1123710559] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,542 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:59,542 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:59,542 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1902328974]
[2025-04-28 21:21:59,543 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,545 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:59,545 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,546 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:59,546 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:59,546 INFO  L87              Difference]: Start difference. First operand 133 states and 420 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:22:00,313 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,313 INFO  L93              Difference]: Finished difference Result 141 states and 522 transitions.
[2025-04-28 21:22:00,314 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:00,314 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:22:00,314 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,317 INFO  L225             Difference]: With dead ends: 141
[2025-04-28 21:22:00,318 INFO  L226             Difference]: Without dead ends: 141
[2025-04-28 21:22:00,318 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:00,319 INFO  L437           NwaCegarLoop]: 251 mSDtfsCounter, 1 mSDsluCounter, 645 mSDsCounter, 0 mSdLazyCounter, 293 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 896 SdHoareTripleChecker+Invalid, 298 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 293 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,319 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 896 Invalid, 298 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 293 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:00,320 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-04-28 21:22:00,358 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 133.
[2025-04-28 21:22:00,359 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 33 states have (on average 3.0) internal successors, (99), 99 states have internal predecessors, (99), 79 states have call successors, (79), 13 states have call predecessors, (79), 20 states have return successors, (242), 20 states have call predecessors, (242), 79 states have call successors, (242)
[2025-04-28 21:22:00,361 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 420 transitions.
[2025-04-28 21:22:00,361 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 420 transitions. Word has length 32
[2025-04-28 21:22:00,362 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,362 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 420 transitions.
[2025-04-28 21:22:00,362 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:22:00,362 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 420 transitions.
[2025-04-28 21:22:00,375 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:00,375 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,375 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:22:00,375 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:22:00,375 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,376 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,378 INFO  L85        PathProgramCache]: Analyzing trace with hash 1076371430, now seen corresponding path program 1 times
[2025-04-28 21:22:00,378 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,379 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1234135394]
[2025-04-28 21:22:00,379 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,379 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,403 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:00,415 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:00,416 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,416 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,532 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,532 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,532 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1234135394]
[2025-04-28 21:22:00,532 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1234135394] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:00,533 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:00,533 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:00,533 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1452945684]
[2025-04-28 21:22:00,533 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,533 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:00,533 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,534 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:00,534 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:00,534 INFO  L87              Difference]: Start difference. First operand 133 states and 420 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:22:01,236 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,236 INFO  L93              Difference]: Finished difference Result 139 states and 474 transitions.
[2025-04-28 21:22:01,237 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:01,237 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:22:01,237 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,240 INFO  L225             Difference]: With dead ends: 139
[2025-04-28 21:22:01,240 INFO  L226             Difference]: Without dead ends: 139
[2025-04-28 21:22:01,241 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,241 INFO  L437           NwaCegarLoop]: 251 mSDtfsCounter, 1 mSDsluCounter, 648 mSDsCounter, 0 mSdLazyCounter, 299 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 899 SdHoareTripleChecker+Invalid, 301 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 299 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,242 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 899 Invalid, 301 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 299 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:01,242 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 139 states.
[2025-04-28 21:22:01,275 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 139 to 137.
[2025-04-28 21:22:01,276 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 35 states have (on average 2.8857142857142857) internal successors, (101), 101 states have internal predecessors, (101), 79 states have call successors, (79), 13 states have call predecessors, (79), 22 states have return successors, (292), 22 states have call predecessors, (292), 79 states have call successors, (292)
[2025-04-28 21:22:01,278 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 472 transitions.
[2025-04-28 21:22:01,278 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 472 transitions. Word has length 32
[2025-04-28 21:22:01,279 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,279 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 472 transitions.
[2025-04-28 21:22:01,279 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:22:01,279 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 472 transitions.
[2025-04-28 21:22:01,284 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:01,284 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,284 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:22:01,284 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:22:01,284 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,285 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,285 INFO  L85        PathProgramCache]: Analyzing trace with hash 1356479113, now seen corresponding path program 1 times
[2025-04-28 21:22:01,285 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,285 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1660753468]
[2025-04-28 21:22:01,285 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,285 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,309 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:01,320 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:01,321 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,321 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,452 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,452 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,452 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1660753468]
[2025-04-28 21:22:01,452 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1660753468] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:01,452 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:01,452 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:01,452 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1380044291]
[2025-04-28 21:22:01,452 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,453 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:01,453 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,453 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:01,453 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:01,453 INFO  L87              Difference]: Start difference. First operand 137 states and 472 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:22:02,211 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,211 INFO  L93              Difference]: Finished difference Result 143 states and 526 transitions.
[2025-04-28 21:22:02,211 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:02,212 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:22:02,212 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,214 INFO  L225             Difference]: With dead ends: 143
[2025-04-28 21:22:02,214 INFO  L226             Difference]: Without dead ends: 143
[2025-04-28 21:22:02,215 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:02,215 INFO  L437           NwaCegarLoop]: 251 mSDtfsCounter, 1 mSDsluCounter, 649 mSDsCounter, 0 mSdLazyCounter, 300 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 900 SdHoareTripleChecker+Invalid, 301 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 300 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,216 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 900 Invalid, 301 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 300 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:02,216 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 143 states.
[2025-04-28 21:22:02,252 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 143 to 137.
[2025-04-28 21:22:02,252 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 35 states have (on average 2.8857142857142857) internal successors, (101), 101 states have internal predecessors, (101), 79 states have call successors, (79), 13 states have call predecessors, (79), 22 states have return successors, (292), 22 states have call predecessors, (292), 79 states have call successors, (292)
[2025-04-28 21:22:02,254 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 472 transitions.
[2025-04-28 21:22:02,254 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 472 transitions. Word has length 32
[2025-04-28 21:22:02,255 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:02,255 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 472 transitions.
[2025-04-28 21:22:02,255 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:22:02,255 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 472 transitions.
[2025-04-28 21:22:02,261 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:02,263 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:02,263 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:22:02,263 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:22:02,263 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,264 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,264 INFO  L85        PathProgramCache]: Analyzing trace with hash 238812553, now seen corresponding path program 1 times
[2025-04-28 21:22:02,264 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,264 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1570953220]
[2025-04-28 21:22:02,264 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:02,264 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,295 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:02,306 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:02,307 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,307 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,415 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,415 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,415 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1570953220]
[2025-04-28 21:22:02,415 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1570953220] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:02,415 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:02,415 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:02,415 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [512812252]
[2025-04-28 21:22:02,415 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:02,416 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:02,416 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:02,416 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:02,416 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:02,417 INFO  L87              Difference]: Start difference. First operand 137 states and 472 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:22:03,180 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,180 INFO  L93              Difference]: Finished difference Result 143 states and 525 transitions.
[2025-04-28 21:22:03,181 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:03,181 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:22:03,181 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,185 INFO  L225             Difference]: With dead ends: 143
[2025-04-28 21:22:03,185 INFO  L226             Difference]: Without dead ends: 143
[2025-04-28 21:22:03,185 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,186 INFO  L437           NwaCegarLoop]: 253 mSDtfsCounter, 1 mSDsluCounter, 654 mSDsCounter, 0 mSdLazyCounter, 296 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 907 SdHoareTripleChecker+Invalid, 297 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 296 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,187 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 907 Invalid, 297 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 296 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:03,188 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 143 states.
[2025-04-28 21:22:03,228 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 143 to 137.
[2025-04-28 21:22:03,229 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 35 states have (on average 2.8857142857142857) internal successors, (101), 101 states have internal predecessors, (101), 79 states have call successors, (79), 13 states have call predecessors, (79), 22 states have return successors, (292), 22 states have call predecessors, (292), 79 states have call successors, (292)
[2025-04-28 21:22:03,233 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 472 transitions.
[2025-04-28 21:22:03,234 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 472 transitions. Word has length 32
[2025-04-28 21:22:03,234 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,234 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 472 transitions.
[2025-04-28 21:22:03,234 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:22:03,234 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 472 transitions.
[2025-04-28 21:22:03,238 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:03,239 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,239 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:22:03,239 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:22:03,240 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,241 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,241 INFO  L85        PathProgramCache]: Analyzing trace with hash -1481291229, now seen corresponding path program 1 times
[2025-04-28 21:22:03,241 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,241 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [907645044]
[2025-04-28 21:22:03,241 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:03,242 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,278 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:03,287 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:03,287 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,288 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,365 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,365 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,366 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [907645044]
[2025-04-28 21:22:03,366 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [907645044] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:03,366 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:03,366 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:03,366 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [504959052]
[2025-04-28 21:22:03,366 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,366 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:03,367 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,367 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:03,367 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:03,367 INFO  L87              Difference]: Start difference. First operand 137 states and 472 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:22:04,115 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,116 INFO  L93              Difference]: Finished difference Result 141 states and 523 transitions.
[2025-04-28 21:22:04,116 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:04,116 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:22:04,117 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,120 INFO  L225             Difference]: With dead ends: 141
[2025-04-28 21:22:04,120 INFO  L226             Difference]: Without dead ends: 141
[2025-04-28 21:22:04,120 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:04,121 INFO  L437           NwaCegarLoop]: 216 mSDtfsCounter, 1 mSDsluCounter, 545 mSDsCounter, 0 mSdLazyCounter, 295 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 761 SdHoareTripleChecker+Invalid, 298 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 295 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,122 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 761 Invalid, 298 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 295 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:04,123 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-04-28 21:22:04,159 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 137.
[2025-04-28 21:22:04,160 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 35 states have (on average 2.8857142857142857) internal successors, (101), 101 states have internal predecessors, (101), 79 states have call successors, (79), 13 states have call predecessors, (79), 22 states have return successors, (292), 22 states have call predecessors, (292), 79 states have call successors, (292)
[2025-04-28 21:22:04,162 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 472 transitions.
[2025-04-28 21:22:04,162 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 472 transitions. Word has length 32
[2025-04-28 21:22:04,164 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,164 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 472 transitions.
[2025-04-28 21:22:04,164 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:22:04,164 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 472 transitions.
[2025-04-28 21:22:04,168 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:04,168 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,168 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:22:04,169 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:22:04,169 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,169 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,170 INFO  L85        PathProgramCache]: Analyzing trace with hash -1403882068, now seen corresponding path program 1 times
[2025-04-28 21:22:04,170 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,170 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [265286678]
[2025-04-28 21:22:04,170 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:04,170 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,193 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:04,203 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:04,204 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,204 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,326 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,326 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,326 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [265286678]
[2025-04-28 21:22:04,326 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [265286678] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:04,326 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:04,326 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:04,326 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [544958167]
[2025-04-28 21:22:04,326 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:04,327 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:04,327 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:04,327 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:04,327 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:04,327 INFO  L87              Difference]: Start difference. First operand 137 states and 472 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:22:05,077 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:05,078 INFO  L93              Difference]: Finished difference Result 139 states and 473 transitions.
[2025-04-28 21:22:05,078 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:05,079 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:22:05,079 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:05,083 INFO  L225             Difference]: With dead ends: 139
[2025-04-28 21:22:05,083 INFO  L226             Difference]: Without dead ends: 139
[2025-04-28 21:22:05,083 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:05,084 INFO  L437           NwaCegarLoop]: 253 mSDtfsCounter, 1 mSDsluCounter, 653 mSDsCounter, 0 mSdLazyCounter, 295 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 906 SdHoareTripleChecker+Invalid, 297 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 295 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:05,085 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 906 Invalid, 297 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 295 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:05,086 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 139 states.
[2025-04-28 21:22:05,113 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 139 to 133.
[2025-04-28 21:22:05,114 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 33 states have (on average 3.0) internal successors, (99), 99 states have internal predecessors, (99), 79 states have call successors, (79), 13 states have call predecessors, (79), 20 states have return successors, (242), 20 states have call predecessors, (242), 79 states have call successors, (242)
[2025-04-28 21:22:05,120 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 420 transitions.
[2025-04-28 21:22:05,120 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 420 transitions. Word has length 32
[2025-04-28 21:22:05,120 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:05,120 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 420 transitions.
[2025-04-28 21:22:05,124 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:22:05,125 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 420 transitions.
[2025-04-28 21:22:05,128 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:05,128 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:05,128 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:22:05,132 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:22:05,133 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:05,133 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:05,133 INFO  L85        PathProgramCache]: Analyzing trace with hash 1186449250, now seen corresponding path program 1 times
[2025-04-28 21:22:05,133 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:05,133 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1333948554]
[2025-04-28 21:22:05,133 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:05,134 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:05,153 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:05,163 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:05,164 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:05,164 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:05,259 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,259 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:05,259 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1333948554]
[2025-04-28 21:22:05,259 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1333948554] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:05,259 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:05,259 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:05,259 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1547354047]
[2025-04-28 21:22:05,259 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,260 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:05,260 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,260 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:05,260 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:05,261 INFO  L87              Difference]: Start difference. First operand 133 states and 420 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:22:06,043 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,044 INFO  L93              Difference]: Finished difference Result 143 states and 525 transitions.
[2025-04-28 21:22:06,044 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:06,045 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:22:06,045 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,048 INFO  L225             Difference]: With dead ends: 143
[2025-04-28 21:22:06,048 INFO  L226             Difference]: Without dead ends: 143
[2025-04-28 21:22:06,049 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:06,049 INFO  L437           NwaCegarLoop]: 252 mSDtfsCounter, 1 mSDsluCounter, 649 mSDsCounter, 0 mSdLazyCounter, 296 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 901 SdHoareTripleChecker+Invalid, 299 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 296 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,049 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 901 Invalid, 299 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 296 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:06,050 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 143 states.
[2025-04-28 21:22:06,087 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 143 to 137.
[2025-04-28 21:22:06,087 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 35 states have (on average 2.8857142857142857) internal successors, (101), 101 states have internal predecessors, (101), 79 states have call successors, (79), 13 states have call predecessors, (79), 22 states have return successors, (292), 22 states have call predecessors, (292), 79 states have call successors, (292)
[2025-04-28 21:22:06,090 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 472 transitions.
[2025-04-28 21:22:06,090 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 472 transitions. Word has length 32
[2025-04-28 21:22:06,090 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,090 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 472 transitions.
[2025-04-28 21:22:06,090 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:22:06,091 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 472 transitions.
[2025-04-28 21:22:06,095 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:06,095 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,095 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:22:06,095 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:22:06,095 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,096 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,096 INFO  L85        PathProgramCache]: Analyzing trace with hash 1786752292, now seen corresponding path program 1 times
[2025-04-28 21:22:06,096 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,096 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1804790043]
[2025-04-28 21:22:06,096 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,096 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,117 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:06,141 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:06,143 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,143 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,228 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,228 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,229 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1804790043]
[2025-04-28 21:22:06,229 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1804790043] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:06,229 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:06,229 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:06,229 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1277562446]
[2025-04-28 21:22:06,229 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:06,229 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:06,229 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:06,230 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:06,230 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:06,230 INFO  L87              Difference]: Start difference. First operand 137 states and 472 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:22:06,945 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,945 INFO  L93              Difference]: Finished difference Result 143 states and 524 transitions.
[2025-04-28 21:22:06,946 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:06,946 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:22:06,946 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,949 INFO  L225             Difference]: With dead ends: 143
[2025-04-28 21:22:06,949 INFO  L226             Difference]: Without dead ends: 143
[2025-04-28 21:22:06,949 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:06,949 INFO  L437           NwaCegarLoop]: 216 mSDtfsCounter, 1 mSDsluCounter, 547 mSDsCounter, 0 mSdLazyCounter, 292 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 763 SdHoareTripleChecker+Invalid, 295 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 292 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,950 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 763 Invalid, 295 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 292 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:06,950 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 143 states.
[2025-04-28 21:22:06,986 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 143 to 133.
[2025-04-28 21:22:06,989 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 33 states have (on average 3.0) internal successors, (99), 99 states have internal predecessors, (99), 79 states have call successors, (79), 13 states have call predecessors, (79), 20 states have return successors, (242), 20 states have call predecessors, (242), 79 states have call successors, (242)
[2025-04-28 21:22:06,991 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 420 transitions.
[2025-04-28 21:22:06,991 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 420 transitions. Word has length 32
[2025-04-28 21:22:06,991 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,991 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 420 transitions.
[2025-04-28 21:22:06,991 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:22:06,991 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 420 transitions.
[2025-04-28 21:22:06,995 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:06,995 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,995 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,996 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:22:06,996 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,996 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,996 INFO  L85        PathProgramCache]: Analyzing trace with hash 323662445, now seen corresponding path program 1 times
[2025-04-28 21:22:06,997 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,997 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1238388854]
[2025-04-28 21:22:06,997 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,997 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,016 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:07,027 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,027 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,028 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,144 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,145 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,145 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1238388854]
[2025-04-28 21:22:07,145 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1238388854] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:07,146 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:07,146 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:07,146 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [550947931]
[2025-04-28 21:22:07,146 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,147 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:07,147 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,147 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:07,147 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:07,147 INFO  L87              Difference]: Start difference. First operand 133 states and 420 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:07,932 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,933 INFO  L93              Difference]: Finished difference Result 141 states and 521 transitions.
[2025-04-28 21:22:07,933 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:07,933 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:07,934 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,936 INFO  L225             Difference]: With dead ends: 141
[2025-04-28 21:22:07,936 INFO  L226             Difference]: Without dead ends: 141
[2025-04-28 21:22:07,936 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:07,937 INFO  L437           NwaCegarLoop]: 213 mSDtfsCounter, 1 mSDsluCounter, 748 mSDsCounter, 0 mSdLazyCounter, 355 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 961 SdHoareTripleChecker+Invalid, 365 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 355 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,937 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 961 Invalid, 365 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 355 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:07,938 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-04-28 21:22:07,971 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 137.
[2025-04-28 21:22:07,972 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 35 states have (on average 2.8857142857142857) internal successors, (101), 101 states have internal predecessors, (101), 79 states have call successors, (79), 13 states have call predecessors, (79), 22 states have return successors, (249), 22 states have call predecessors, (249), 79 states have call successors, (249)
[2025-04-28 21:22:07,973 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 429 transitions.
[2025-04-28 21:22:07,974 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 429 transitions. Word has length 36
[2025-04-28 21:22:07,974 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,974 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 429 transitions.
[2025-04-28 21:22:07,974 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:07,974 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 429 transitions.
[2025-04-28 21:22:07,977 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:07,977 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,978 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,978 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:22:07,978 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,978 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,978 INFO  L85        PathProgramCache]: Analyzing trace with hash -1146241966, now seen corresponding path program 1 times
[2025-04-28 21:22:07,978 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,978 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1107439038]
[2025-04-28 21:22:07,978 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,979 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,999 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:08,007 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:08,007 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:08,007 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,086 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:08,086 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:08,086 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1107439038]
[2025-04-28 21:22:08,086 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1107439038] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:08,086 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:08,086 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:08,086 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [486250583]
[2025-04-28 21:22:08,086 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,087 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:08,087 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,087 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:08,087 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:08,088 INFO  L87              Difference]: Start difference. First operand 137 states and 429 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:08,810 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:08,810 INFO  L93              Difference]: Finished difference Result 141 states and 480 transitions.
[2025-04-28 21:22:08,811 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:08,811 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:08,811 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,813 INFO  L225             Difference]: With dead ends: 141
[2025-04-28 21:22:08,813 INFO  L226             Difference]: Without dead ends: 141
[2025-04-28 21:22:08,813 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:08,814 INFO  L437           NwaCegarLoop]: 251 mSDtfsCounter, 1 mSDsluCounter, 646 mSDsCounter, 0 mSdLazyCounter, 294 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 897 SdHoareTripleChecker+Invalid, 298 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 294 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,814 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 897 Invalid, 298 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 294 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:08,815 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-04-28 21:22:08,843 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 137.
[2025-04-28 21:22:08,844 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 35 states have (on average 2.8857142857142857) internal successors, (101), 101 states have internal predecessors, (101), 79 states have call successors, (79), 13 states have call predecessors, (79), 22 states have return successors, (249), 22 states have call predecessors, (249), 79 states have call successors, (249)
[2025-04-28 21:22:08,846 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 429 transitions.
[2025-04-28 21:22:08,846 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 429 transitions. Word has length 36
[2025-04-28 21:22:08,846 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,846 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 429 transitions.
[2025-04-28 21:22:08,846 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:08,846 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 429 transitions.
[2025-04-28 21:22:08,850 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:08,851 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,851 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:08,851 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:22:08,851 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:08,851 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:08,852 INFO  L85        PathProgramCache]: Analyzing trace with hash -427188984, now seen corresponding path program 1 times
[2025-04-28 21:22:08,852 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:08,852 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [157050790]
[2025-04-28 21:22:08,852 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:08,852 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:08,890 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:08,899 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:08,899 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:08,899 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,996 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:08,996 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:08,996 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [157050790]
[2025-04-28 21:22:08,996 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [157050790] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:08,997 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:08,997 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:08,997 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2089350878]
[2025-04-28 21:22:08,997 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,997 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:08,999 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,999 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:08,999 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:09,000 INFO  L87              Difference]: Start difference. First operand 137 states and 429 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:09,756 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:09,757 INFO  L93              Difference]: Finished difference Result 149 states and 581 transitions.
[2025-04-28 21:22:09,757 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:09,757 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:09,758 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:09,761 INFO  L225             Difference]: With dead ends: 149
[2025-04-28 21:22:09,761 INFO  L226             Difference]: Without dead ends: 149
[2025-04-28 21:22:09,761 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:09,762 INFO  L437           NwaCegarLoop]: 213 mSDtfsCounter, 1 mSDsluCounter, 749 mSDsCounter, 0 mSdLazyCounter, 356 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 962 SdHoareTripleChecker+Invalid, 365 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 356 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:09,763 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 962 Invalid, 365 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 356 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:09,763 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-04-28 21:22:09,807 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 139.
[2025-04-28 21:22:09,807 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 139 states, 36 states have (on average 2.8333333333333335) internal successors, (102), 102 states have internal predecessors, (102), 79 states have call successors, (79), 13 states have call predecessors, (79), 23 states have return successors, (253), 23 states have call predecessors, (253), 79 states have call successors, (253)
[2025-04-28 21:22:09,809 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 139 states to 139 states and 434 transitions.
[2025-04-28 21:22:09,810 INFO  L79                 Accepts]: Start accepts. Automaton has 139 states and 434 transitions. Word has length 36
[2025-04-28 21:22:09,810 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:09,810 INFO  L485      AbstractCegarLoop]: Abstraction has 139 states and 434 transitions.
[2025-04-28 21:22:09,810 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:09,810 INFO  L278                IsEmpty]: Start isEmpty. Operand 139 states and 434 transitions.
[2025-04-28 21:22:09,814 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:09,815 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:09,815 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:09,815 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:22:09,817 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,817 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,817 INFO  L85        PathProgramCache]: Analyzing trace with hash 2104125539, now seen corresponding path program 1 times
[2025-04-28 21:22:09,817 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,817 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1276605739]
[2025-04-28 21:22:09,817 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:09,818 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,843 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:09,852 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:09,852 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:09,852 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,961 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:09,961 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:09,961 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1276605739]
[2025-04-28 21:22:09,961 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1276605739] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:09,961 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:09,961 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:09,961 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [657412414]
[2025-04-28 21:22:09,961 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:09,962 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:09,963 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:09,963 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:09,964 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:09,964 INFO  L87              Difference]: Start difference. First operand 139 states and 434 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:10,759 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:10,759 INFO  L93              Difference]: Finished difference Result 149 states and 538 transitions.
[2025-04-28 21:22:10,760 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:10,760 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:10,760 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:10,763 INFO  L225             Difference]: With dead ends: 149
[2025-04-28 21:22:10,763 INFO  L226             Difference]: Without dead ends: 149
[2025-04-28 21:22:10,764 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:10,764 INFO  L437           NwaCegarLoop]: 252 mSDtfsCounter, 1 mSDsluCounter, 899 mSDsCounter, 0 mSdLazyCounter, 363 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1151 SdHoareTripleChecker+Invalid, 369 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 363 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:10,764 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1151 Invalid, 369 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 363 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:10,765 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-04-28 21:22:10,800 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 143.
[2025-04-28 21:22:10,804 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 143 states, 38 states have (on average 2.736842105263158) internal successors, (104), 104 states have internal predecessors, (104), 79 states have call successors, (79), 13 states have call predecessors, (79), 25 states have return successors, (260), 25 states have call predecessors, (260), 79 states have call successors, (260)
[2025-04-28 21:22:10,806 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 143 states to 143 states and 443 transitions.
[2025-04-28 21:22:10,807 INFO  L79                 Accepts]: Start accepts. Automaton has 143 states and 443 transitions. Word has length 36
[2025-04-28 21:22:10,807 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:10,807 INFO  L485      AbstractCegarLoop]: Abstraction has 143 states and 443 transitions.
[2025-04-28 21:22:10,807 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:10,807 INFO  L278                IsEmpty]: Start isEmpty. Operand 143 states and 443 transitions.
[2025-04-28 21:22:10,811 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:10,811 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:10,811 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:10,811 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:22:10,811 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:10,812 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:10,812 INFO  L85        PathProgramCache]: Analyzing trace with hash -399675319, now seen corresponding path program 1 times
[2025-04-28 21:22:10,812 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:10,812 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [187980216]
[2025-04-28 21:22:10,813 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:10,813 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:10,835 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:10,843 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:10,843 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:10,844 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,947 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:10,947 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:10,947 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [187980216]
[2025-04-28 21:22:10,947 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [187980216] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:10,947 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:10,948 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:10,948 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [44297952]
[2025-04-28 21:22:10,948 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:10,948 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:10,948 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:10,949 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:10,949 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:10,949 INFO  L87              Difference]: Start difference. First operand 143 states and 443 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:11,713 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:11,713 INFO  L93              Difference]: Finished difference Result 153 states and 547 transitions.
[2025-04-28 21:22:11,713 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:11,714 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:11,714 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:11,716 INFO  L225             Difference]: With dead ends: 153
[2025-04-28 21:22:11,717 INFO  L226             Difference]: Without dead ends: 153
[2025-04-28 21:22:11,717 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:11,717 INFO  L437           NwaCegarLoop]: 252 mSDtfsCounter, 1 mSDsluCounter, 900 mSDsCounter, 0 mSdLazyCounter, 364 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1152 SdHoareTripleChecker+Invalid, 369 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 364 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:11,718 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1152 Invalid, 369 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 364 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:11,718 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-04-28 21:22:11,751 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 149.
[2025-04-28 21:22:11,752 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 149 states, 41 states have (on average 2.6097560975609757) internal successors, (107), 107 states have internal predecessors, (107), 79 states have call successors, (79), 13 states have call predecessors, (79), 28 states have return successors, (313), 28 states have call predecessors, (313), 79 states have call successors, (313)
[2025-04-28 21:22:11,754 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 149 states to 149 states and 499 transitions.
[2025-04-28 21:22:11,754 INFO  L79                 Accepts]: Start accepts. Automaton has 149 states and 499 transitions. Word has length 36
[2025-04-28 21:22:11,754 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:11,754 INFO  L485      AbstractCegarLoop]: Abstraction has 149 states and 499 transitions.
[2025-04-28 21:22:11,755 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:11,755 INFO  L278                IsEmpty]: Start isEmpty. Operand 149 states and 499 transitions.
[2025-04-28 21:22:11,757 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:11,758 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:11,758 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:11,758 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-04-28 21:22:11,758 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:11,758 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:11,758 INFO  L85        PathProgramCache]: Analyzing trace with hash -703901764, now seen corresponding path program 1 times
[2025-04-28 21:22:11,758 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:11,759 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [898533438]
[2025-04-28 21:22:11,759 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:11,759 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:11,779 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:11,787 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:11,787 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:11,787 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:11,886 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:11,886 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:11,887 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [898533438]
[2025-04-28 21:22:11,887 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [898533438] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:11,887 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:11,887 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:11,887 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1247055895]
[2025-04-28 21:22:11,887 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:11,887 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:11,888 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:11,888 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:11,888 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:11,888 INFO  L87              Difference]: Start difference. First operand 149 states and 499 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:12,648 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,648 INFO  L93              Difference]: Finished difference Result 155 states and 593 transitions.
[2025-04-28 21:22:12,648 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:12,649 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:12,649 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,651 INFO  L225             Difference]: With dead ends: 155
[2025-04-28 21:22:12,651 INFO  L226             Difference]: Without dead ends: 155
[2025-04-28 21:22:12,652 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:12,652 INFO  L437           NwaCegarLoop]: 254 mSDtfsCounter, 1 mSDsluCounter, 906 mSDsCounter, 0 mSdLazyCounter, 358 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1160 SdHoareTripleChecker+Invalid, 364 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 358 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,652 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1160 Invalid, 364 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 358 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:12,653 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 155 states.
[2025-04-28 21:22:12,696 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 155 to 145.
[2025-04-28 21:22:12,697 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 145 states, 39 states have (on average 2.6923076923076925) internal successors, (105), 105 states have internal predecessors, (105), 79 states have call successors, (79), 13 states have call predecessors, (79), 26 states have return successors, (306), 26 states have call predecessors, (306), 79 states have call successors, (306)
[2025-04-28 21:22:12,699 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 145 states to 145 states and 490 transitions.
[2025-04-28 21:22:12,699 INFO  L79                 Accepts]: Start accepts. Automaton has 145 states and 490 transitions. Word has length 36
[2025-04-28 21:22:12,699 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:12,699 INFO  L485      AbstractCegarLoop]: Abstraction has 145 states and 490 transitions.
[2025-04-28 21:22:12,699 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:12,699 INFO  L278                IsEmpty]: Start isEmpty. Operand 145 states and 490 transitions.
[2025-04-28 21:22:12,702 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:12,702 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:12,702 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:12,703 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-04-28 21:22:12,704 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:12,704 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:12,704 INFO  L85        PathProgramCache]: Analyzing trace with hash -1101719904, now seen corresponding path program 1 times
[2025-04-28 21:22:12,704 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:12,704 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1790068431]
[2025-04-28 21:22:12,704 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:12,704 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:12,724 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:12,745 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:12,746 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:12,746 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:12,837 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:12,837 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:12,837 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1790068431]
[2025-04-28 21:22:12,837 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1790068431] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:12,837 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:12,837 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:12,837 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [864257645]
[2025-04-28 21:22:12,837 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,838 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:12,838 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,839 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:12,839 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:12,839 INFO  L87              Difference]: Start difference. First operand 145 states and 490 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:13,612 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:13,612 INFO  L93              Difference]: Finished difference Result 153 states and 591 transitions.
[2025-04-28 21:22:13,613 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:13,613 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:13,613 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:13,615 INFO  L225             Difference]: With dead ends: 153
[2025-04-28 21:22:13,615 INFO  L226             Difference]: Without dead ends: 153
[2025-04-28 21:22:13,615 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:13,616 INFO  L437           NwaCegarLoop]: 213 mSDtfsCounter, 1 mSDsluCounter, 751 mSDsCounter, 0 mSdLazyCounter, 358 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 964 SdHoareTripleChecker+Invalid, 365 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 358 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:13,616 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 964 Invalid, 365 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 358 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:13,617 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-04-28 21:22:13,660 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 145.
[2025-04-28 21:22:13,661 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 145 states, 39 states have (on average 2.6923076923076925) internal successors, (105), 105 states have internal predecessors, (105), 79 states have call successors, (79), 13 states have call predecessors, (79), 26 states have return successors, (306), 26 states have call predecessors, (306), 79 states have call successors, (306)
[2025-04-28 21:22:13,663 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 145 states to 145 states and 490 transitions.
[2025-04-28 21:22:13,663 INFO  L79                 Accepts]: Start accepts. Automaton has 145 states and 490 transitions. Word has length 36
[2025-04-28 21:22:13,665 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,665 INFO  L485      AbstractCegarLoop]: Abstraction has 145 states and 490 transitions.
[2025-04-28 21:22:13,665 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:13,665 INFO  L278                IsEmpty]: Start isEmpty. Operand 145 states and 490 transitions.
[2025-04-28 21:22:13,668 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:13,669 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,669 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:13,669 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-04-28 21:22:13,669 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,669 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,670 INFO  L85        PathProgramCache]: Analyzing trace with hash 2019466570, now seen corresponding path program 1 times
[2025-04-28 21:22:13,670 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,670 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1279424102]
[2025-04-28 21:22:13,670 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,670 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,694 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:13,704 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:13,704 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,704 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,801 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:13,801 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,801 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1279424102]
[2025-04-28 21:22:13,801 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1279424102] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:13,802 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:13,802 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:13,802 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1815032791]
[2025-04-28 21:22:13,802 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:13,802 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:13,802 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:13,803 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:13,803 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:13,803 INFO  L87              Difference]: Start difference. First operand 145 states and 490 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:14,644 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:14,644 INFO  L93              Difference]: Finished difference Result 149 states and 537 transitions.
[2025-04-28 21:22:14,645 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:14,645 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:14,645 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:14,648 INFO  L225             Difference]: With dead ends: 149
[2025-04-28 21:22:14,648 INFO  L226             Difference]: Without dead ends: 149
[2025-04-28 21:22:14,648 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:14,648 INFO  L437           NwaCegarLoop]: 252 mSDtfsCounter, 1 mSDsluCounter, 900 mSDsCounter, 0 mSdLazyCounter, 359 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1152 SdHoareTripleChecker+Invalid, 364 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 359 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:14,649 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1152 Invalid, 364 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 359 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:14,649 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-04-28 21:22:14,677 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 139.
[2025-04-28 21:22:14,678 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 139 states, 36 states have (on average 2.8333333333333335) internal successors, (102), 102 states have internal predecessors, (102), 79 states have call successors, (79), 13 states have call predecessors, (79), 23 states have return successors, (253), 23 states have call predecessors, (253), 79 states have call successors, (253)
[2025-04-28 21:22:14,680 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 139 states to 139 states and 434 transitions.
[2025-04-28 21:22:14,680 INFO  L79                 Accepts]: Start accepts. Automaton has 139 states and 434 transitions. Word has length 36
[2025-04-28 21:22:14,680 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:14,680 INFO  L485      AbstractCegarLoop]: Abstraction has 139 states and 434 transitions.
[2025-04-28 21:22:14,680 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:14,680 INFO  L278                IsEmpty]: Start isEmpty. Operand 139 states and 434 transitions.
[2025-04-28 21:22:14,683 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:14,683 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:14,683 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:14,683 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-04-28 21:22:14,683 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:14,684 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:14,684 INFO  L85        PathProgramCache]: Analyzing trace with hash 1485313052, now seen corresponding path program 1 times
[2025-04-28 21:22:14,684 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:14,684 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2058493122]
[2025-04-28 21:22:14,684 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:14,684 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:14,703 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:14,711 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:14,711 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:14,712 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:14,814 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:14,814 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:14,814 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2058493122]
[2025-04-28 21:22:14,814 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2058493122] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:14,814 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:14,814 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:14,814 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [730020135]
[2025-04-28 21:22:14,814 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:14,815 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:14,815 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:14,815 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:14,815 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:14,815 INFO  L87              Difference]: Start difference. First operand 139 states and 434 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:15,681 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:15,681 INFO  L93              Difference]: Finished difference Result 153 states and 589 transitions.
[2025-04-28 21:22:15,682 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:15,682 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:15,682 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:15,685 INFO  L225             Difference]: With dead ends: 153
[2025-04-28 21:22:15,685 INFO  L226             Difference]: Without dead ends: 153
[2025-04-28 21:22:15,685 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:15,687 INFO  L437           NwaCegarLoop]: 253 mSDtfsCounter, 1 mSDsluCounter, 901 mSDsCounter, 0 mSdLazyCounter, 360 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1154 SdHoareTripleChecker+Invalid, 367 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 360 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:15,687 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1154 Invalid, 367 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 360 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:15,688 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-04-28 21:22:15,731 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 147.
[2025-04-28 21:22:15,732 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 147 states, 40 states have (on average 2.65) internal successors, (106), 106 states have internal predecessors, (106), 79 states have call successors, (79), 13 states have call predecessors, (79), 27 states have return successors, (310), 27 states have call predecessors, (310), 79 states have call successors, (310)
[2025-04-28 21:22:15,734 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 147 states to 147 states and 495 transitions.
[2025-04-28 21:22:15,734 INFO  L79                 Accepts]: Start accepts. Automaton has 147 states and 495 transitions. Word has length 36
[2025-04-28 21:22:15,734 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:15,735 INFO  L485      AbstractCegarLoop]: Abstraction has 147 states and 495 transitions.
[2025-04-28 21:22:15,735 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:15,735 INFO  L278                IsEmpty]: Start isEmpty. Operand 147 states and 495 transitions.
[2025-04-28 21:22:15,738 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:15,738 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:15,738 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:15,739 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-04-28 21:22:15,739 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:15,739 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:15,739 INFO  L85        PathProgramCache]: Analyzing trace with hash 539165728, now seen corresponding path program 1 times
[2025-04-28 21:22:15,739 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:15,739 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2119607794]
[2025-04-28 21:22:15,739 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:15,740 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:15,762 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:15,770 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:15,770 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:15,770 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:15,864 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:15,864 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:15,864 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2119607794]
[2025-04-28 21:22:15,865 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2119607794] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:15,865 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:15,865 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:15,865 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1121751312]
[2025-04-28 21:22:15,865 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:15,865 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:15,865 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:15,866 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:15,866 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:15,866 INFO  L87              Difference]: Start difference. First operand 147 states and 495 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:16,677 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:16,677 INFO  L93              Difference]: Finished difference Result 153 states and 588 transitions.
[2025-04-28 21:22:16,678 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:16,678 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:16,678 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:16,681 INFO  L225             Difference]: With dead ends: 153
[2025-04-28 21:22:16,681 INFO  L226             Difference]: Without dead ends: 153
[2025-04-28 21:22:16,681 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:16,682 INFO  L437           NwaCegarLoop]: 252 mSDtfsCounter, 1 mSDsluCounter, 898 mSDsCounter, 0 mSdLazyCounter, 355 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1150 SdHoareTripleChecker+Invalid, 362 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 355 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:16,683 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1150 Invalid, 362 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 355 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:16,683 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-04-28 21:22:16,722 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 139.
[2025-04-28 21:22:16,723 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 139 states, 36 states have (on average 2.8333333333333335) internal successors, (102), 102 states have internal predecessors, (102), 79 states have call successors, (79), 13 states have call predecessors, (79), 23 states have return successors, (253), 23 states have call predecessors, (253), 79 states have call successors, (253)
[2025-04-28 21:22:16,725 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 139 states to 139 states and 434 transitions.
[2025-04-28 21:22:16,725 INFO  L79                 Accepts]: Start accepts. Automaton has 139 states and 434 transitions. Word has length 36
[2025-04-28 21:22:16,725 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:16,726 INFO  L485      AbstractCegarLoop]: Abstraction has 139 states and 434 transitions.
[2025-04-28 21:22:16,726 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:16,726 INFO  L278                IsEmpty]: Start isEmpty. Operand 139 states and 434 transitions.
[2025-04-28 21:22:16,729 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:22:16,729 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:16,729 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:16,729 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-04-28 21:22:16,729 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:16,730 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:16,730 INFO  L85        PathProgramCache]: Analyzing trace with hash 513616099, now seen corresponding path program 1 times
[2025-04-28 21:22:16,730 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:16,730 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [377565213]
[2025-04-28 21:22:16,730 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:16,730 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:16,763 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:22:16,794 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:22:16,797 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:16,797 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:16,947 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:16,947 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:16,947 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [377565213]
[2025-04-28 21:22:16,948 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [377565213] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:16,948 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:16,948 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:16,948 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1116591033]
[2025-04-28 21:22:16,948 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:16,948 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:16,948 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:16,949 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:16,949 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:16,949 INFO  L87              Difference]: Start difference. First operand 139 states and 434 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, (10), 4 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:22:17,731 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:17,731 INFO  L93              Difference]: Finished difference Result 149 states and 539 transitions.
[2025-04-28 21:22:17,732 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:17,732 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, (10), 4 states have call predecessors, (10), 3 states have call successors, (10) Word has length 40
[2025-04-28 21:22:17,733 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:17,735 INFO  L225             Difference]: With dead ends: 149
[2025-04-28 21:22:17,735 INFO  L226             Difference]: Without dead ends: 149
[2025-04-28 21:22:17,735 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:17,736 INFO  L437           NwaCegarLoop]: 253 mSDtfsCounter, 1 mSDsluCounter, 649 mSDsCounter, 0 mSdLazyCounter, 289 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 902 SdHoareTripleChecker+Invalid, 295 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 289 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:17,736 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 902 Invalid, 295 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 289 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:17,737 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-04-28 21:22:17,767 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 139.
[2025-04-28 21:22:17,767 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 139 states, 36 states have (on average 2.8333333333333335) internal successors, (102), 102 states have internal predecessors, (102), 79 states have call successors, (79), 13 states have call predecessors, (79), 23 states have return successors, (253), 23 states have call predecessors, (253), 79 states have call successors, (253)
[2025-04-28 21:22:17,769 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 139 states to 139 states and 434 transitions.
[2025-04-28 21:22:17,769 INFO  L79                 Accepts]: Start accepts. Automaton has 139 states and 434 transitions. Word has length 40
[2025-04-28 21:22:17,769 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:17,770 INFO  L485      AbstractCegarLoop]: Abstraction has 139 states and 434 transitions.
[2025-04-28 21:22:17,770 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, (10), 4 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:22:17,770 INFO  L278                IsEmpty]: Start isEmpty. Operand 139 states and 434 transitions.
[2025-04-28 21:22:17,772 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:22:17,772 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:17,773 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, 1, 1, 1, 1]
[2025-04-28 21:22:17,773 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable24
[2025-04-28 21:22:17,773 INFO  L403      AbstractCegarLoop]: === Iteration 25 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:17,773 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:17,773 INFO  L85        PathProgramCache]: Analyzing trace with hash -84336241, now seen corresponding path program 1 times
[2025-04-28 21:22:17,773 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:17,773 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [954554870]
[2025-04-28 21:22:17,774 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:17,774 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:17,796 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:22:17,803 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:22:17,803 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:17,804 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:17,900 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:17,901 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:17,901 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [954554870]
[2025-04-28 21:22:17,901 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [954554870] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:17,901 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:17,901 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:17,901 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [487230705]
[2025-04-28 21:22:17,901 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:17,901 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:17,902 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:17,902 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:17,902 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:17,902 INFO  L87              Difference]: Start difference. First operand 139 states and 434 transitions. Second operand  has 6 states, 5 states have (on average 4.0) internal successors, (20), 6 states have internal predecessors, (20), 3 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 5 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:22:18,790 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:18,790 INFO  L93              Difference]: Finished difference Result 145 states and 530 transitions.
[2025-04-28 21:22:18,791 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:18,791 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.0) internal successors, (20), 6 states have internal predecessors, (20), 3 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 5 states have call predecessors, (10), 3 states have call successors, (10) Word has length 40
[2025-04-28 21:22:18,791 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:18,794 INFO  L225             Difference]: With dead ends: 145
[2025-04-28 21:22:18,794 INFO  L226             Difference]: Without dead ends: 145
[2025-04-28 21:22:18,794 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:18,795 INFO  L437           NwaCegarLoop]: 252 mSDtfsCounter, 1 mSDsluCounter, 897 mSDsCounter, 0 mSdLazyCounter, 357 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1149 SdHoareTripleChecker+Invalid, 365 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 357 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:18,795 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1149 Invalid, 365 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 357 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:22:18,796 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 145 states.
[2025-04-28 21:22:18,826 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 145 to 137.
[2025-04-28 21:22:18,831 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 35 states have (on average 2.8857142857142857) internal successors, (101), 101 states have internal predecessors, (101), 79 states have call successors, (79), 13 states have call predecessors, (79), 22 states have return successors, (249), 22 states have call predecessors, (249), 79 states have call successors, (249)
[2025-04-28 21:22:18,833 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 429 transitions.
[2025-04-28 21:22:18,833 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 429 transitions. Word has length 40
[2025-04-28 21:22:18,837 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:18,837 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 429 transitions.
[2025-04-28 21:22:18,838 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.0) internal successors, (20), 6 states have internal predecessors, (20), 3 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 5 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:22:18,838 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 429 transitions.
[2025-04-28 21:22:18,843 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:22:18,843 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:18,843 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:18,843 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable25
[2025-04-28 21:22:18,843 INFO  L403      AbstractCegarLoop]: === Iteration 26 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:18,844 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:18,844 INFO  L85        PathProgramCache]: Analyzing trace with hash -1376015808, now seen corresponding path program 1 times
[2025-04-28 21:22:18,844 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:18,844 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1280520359]
[2025-04-28 21:22:18,844 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:18,844 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:18,866 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:22:18,873 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:22:18,873 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:18,873 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:18,958 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:18,958 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:18,958 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1280520359]
[2025-04-28 21:22:18,959 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1280520359] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:18,959 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:18,959 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:18,959 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [817390470]
[2025-04-28 21:22:18,959 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:18,960 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:18,960 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:18,960 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:18,961 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:18,961 INFO  L87              Difference]: Start difference. First operand 137 states and 429 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, (10), 4 states have call predecessors, (10), 3 states have call successors, (10)
