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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:33,489 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:33,582 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_90223976-0105-401b-82f2-c05b07c17173/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:33,589 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:33,590 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:33,630 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:33,630 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:33,631 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:33,631 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:33,632 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:33,633 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:33,633 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:33,634 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:33,634 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:33,634 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:33,635 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:33,635 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:33,635 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:33,635 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:33,635 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:33,635 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:33,635 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:33,636 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:33,636 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:33,636 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:33,637 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:33,637 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:33,967 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:33,977 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:33,979 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:33,983 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:33,984 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:33,985 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_90223976-0105-401b-82f2-c05b07c17173/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-216.smt2
[2025-04-28 21:21:33,988 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:33,992 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:35,091 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_90223976-0105-401b-82f2-c05b07c17173/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-216.smt2
[2025-04-28 21:21:35,098 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:35,100 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:35,102 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:35,102 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:35,102 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:35,106 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,198 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35 Unit
[2025-04-28 21:21:35,198 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:35,200 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:35,201 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:35,201 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:35,221 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,222 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,264 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,264 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,291 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,294 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,302 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,315 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,324 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,367 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:35,371 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:35,371 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:35,371 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:35,372 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,377 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:35,392 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,408 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:35,412 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:35,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:35,426 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:35,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:35,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main456 given in one single declaration
[2025-04-28 21:21:35,426 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main456
[2025-04-28 21:21:35,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main456
[2025-04-28 21:21:35,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main448 given in one single declaration
[2025-04-28 21:21:35,426 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main448
[2025-04-28 21:21:35,427 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main448
[2025-04-28 21:21:35,427 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main111 given in one single declaration
[2025-04-28 21:21:35,427 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main111
[2025-04-28 21:21:35,427 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main111
[2025-04-28 21:21:35,427 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main100 given in one single declaration
[2025-04-28 21:21:35,428 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main100
[2025-04-28 21:21:35,429 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main100
[2025-04-28 21:21:35,429 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main4 given in one single declaration
[2025-04-28 21:21:35,429 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main4
[2025-04-28 21:21:35,429 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main4
[2025-04-28 21:21:35,429 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main486 given in one single declaration
[2025-04-28 21:21:35,429 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main486
[2025-04-28 21:21:35,429 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main486
[2025-04-28 21:21:35,429 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main192 given in one single declaration
[2025-04-28 21:21:35,429 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main192
[2025-04-28 21:21:35,430 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main192
[2025-04-28 21:21:35,430 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main323 given in one single declaration
[2025-04-28 21:21:35,430 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main323
[2025-04-28 21:21:35,430 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main323
[2025-04-28 21:21:35,430 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main248 given in one single declaration
[2025-04-28 21:21:35,430 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main248
[2025-04-28 21:21:35,430 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main248
[2025-04-28 21:21:35,430 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main329 given in one single declaration
[2025-04-28 21:21:35,430 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main329
[2025-04-28 21:21:35,430 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main329
[2025-04-28 21:21:35,431 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main451 given in one single declaration
[2025-04-28 21:21:35,431 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main451
[2025-04-28 21:21:35,431 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main451
[2025-04-28 21:21:35,431 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main412 given in one single declaration
[2025-04-28 21:21:35,431 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main412
[2025-04-28 21:21:35,431 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main412
[2025-04-28 21:21:35,432 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main291 given in one single declaration
[2025-04-28 21:21:35,432 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main291
[2025-04-28 21:21:35,432 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main291
[2025-04-28 21:21:35,432 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main265 given in one single declaration
[2025-04-28 21:21:35,432 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main265
[2025-04-28 21:21:35,432 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main265
[2025-04-28 21:21:35,432 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:35,433 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:35,433 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:35,738 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:35,741 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:37,130 INFO  L?                        ?]: Removed 144 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:37,130 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:37,156 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:37,158 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:37,159 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:37 BoogieIcfgContainer
[2025-04-28 21:21:37,159 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:37,162 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:37,163 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:37,167 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:37,168 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:35" (1/3) ...
[2025-04-28 21:21:37,168 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7e130827 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:37, skipping insertion in model container
[2025-04-28 21:21:37,169 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (2/3) ...
[2025-04-28 21:21:37,169 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7e130827 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:37, skipping insertion in model container
[2025-04-28 21:21:37,169 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:37" (3/3) ...
[2025-04-28 21:21:37,170 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:37,187 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:37,190 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 16 procedures, 133 locations, 357 edges, 16 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:37,240 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:37,265 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;@36e28eb5, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:37,265 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:37,270 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 133 states, 31 states have (on average 3.2903225806451615) internal successors, (102), 102 states have internal predecessors, (102), 85 states have call successors, (85), 15 states have call predecessors, (85), 15 states have return successors, (85), 15 states have call predecessors, (85), 85 states have call successors, (85)
[2025-04-28 21:21:37,312 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:37,312 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,313 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,314 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,323 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,324 INFO  L85        PathProgramCache]: Analyzing trace with hash -373783365, now seen corresponding path program 1 times
[2025-04-28 21:21:37,333 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,334 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1159977890]
[2025-04-28 21:21:37,334 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,334 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,402 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:37,517 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:37,520 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,522 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,995 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:37,996 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,997 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1159977890]
[2025-04-28 21:21:37,997 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1159977890] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,997 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,001 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:38,003 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1421323326]
[2025-04-28 21:21:38,004 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,011 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:38,011 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,118 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:38,122 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:38,125 INFO  L87              Difference]: Start difference. First operand  has 133 states, 31 states have (on average 3.2903225806451615) internal successors, (102), 102 states have internal predecessors, (102), 85 states have call successors, (85), 15 states have call predecessors, (85), 15 states have return successors, (85), 15 states have call predecessors, (85), 85 states have call successors, (85) Second operand  has 6 states, 5 states have (on average 2.4) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:39,195 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,198 INFO  L93              Difference]: Finished difference Result 128 states and 295 transitions.
[2025-04-28 21:21:39,200 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:39,201 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 2.4) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:39,202 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,216 INFO  L225             Difference]: With dead ends: 128
[2025-04-28 21:21:39,216 INFO  L226             Difference]: Without dead ends: 128
[2025-04-28 21:21:39,218 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:39,223 INFO  L437           NwaCegarLoop]: 200 mSDtfsCounter, 1 mSDsluCounter, 742 mSDsCounter, 0 mSdLazyCounter, 290 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 942 SdHoareTripleChecker+Invalid, 295 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 290 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,225 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 942 Invalid, 295 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [5 Valid, 290 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:39,250 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 128 states.
[2025-04-28 21:21:39,336 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 128 to 128.
[2025-04-28 21:21:39,341 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 128 states, 32 states have (on average 2.96875) internal successors, (95), 95 states have internal predecessors, (95), 78 states have call successors, (78), 15 states have call predecessors, (78), 17 states have return successors, (122), 17 states have call predecessors, (122), 78 states have call successors, (122)
[2025-04-28 21:21:39,356 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 295 transitions.
[2025-04-28 21:21:39,358 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 295 transitions. Word has length 24
[2025-04-28 21:21:39,360 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,361 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 295 transitions.
[2025-04-28 21:21:39,362 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 2.4) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:39,362 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 295 transitions.
[2025-04-28 21:21:39,371 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:39,372 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,372 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:39,373 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:39,373 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,375 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,375 INFO  L85        PathProgramCache]: Analyzing trace with hash 928320062, now seen corresponding path program 1 times
[2025-04-28 21:21:39,375 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,375 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1681961328]
[2025-04-28 21:21:39,376 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,376 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,423 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:39,459 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:39,459 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,459 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,685 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:39,685 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,685 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1681961328]
[2025-04-28 21:21:39,685 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1681961328] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,685 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,685 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:39,686 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2109801805]
[2025-04-28 21:21:39,686 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,687 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:39,687 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,689 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:39,689 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:39,689 INFO  L87              Difference]: Start difference. First operand 128 states and 295 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:40,654 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,655 INFO  L93              Difference]: Finished difference Result 132 states and 341 transitions.
[2025-04-28 21:21:40,658 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:40,659 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:40,659 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,666 INFO  L225             Difference]: With dead ends: 132
[2025-04-28 21:21:40,666 INFO  L226             Difference]: Without dead ends: 132
[2025-04-28 21:21:40,666 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:40,667 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 1 mSDsluCounter, 640 mSDsCounter, 0 mSdLazyCounter, 263 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 888 SdHoareTripleChecker+Invalid, 273 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 263 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,667 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 888 Invalid, 273 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 263 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:40,668 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-04-28 21:21:40,718 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 132.
[2025-04-28 21:21:40,720 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 132 states, 34 states have (on average 2.8529411764705883) internal successors, (97), 97 states have internal predecessors, (97), 78 states have call successors, (78), 15 states have call predecessors, (78), 19 states have return successors, (166), 19 states have call predecessors, (166), 78 states have call successors, (166)
[2025-04-28 21:21:40,728 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 132 states to 132 states and 341 transitions.
[2025-04-28 21:21:40,728 INFO  L79                 Accepts]: Start accepts. Automaton has 132 states and 341 transitions. Word has length 32
[2025-04-28 21:21:40,728 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,729 INFO  L485      AbstractCegarLoop]: Abstraction has 132 states and 341 transitions.
[2025-04-28 21:21:40,729 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:40,729 INFO  L278                IsEmpty]: Start isEmpty. Operand 132 states and 341 transitions.
[2025-04-28 21:21:40,737 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:40,737 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,742 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:40,742 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:40,742 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,743 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,743 INFO  L85        PathProgramCache]: Analyzing trace with hash -124686163, now seen corresponding path program 1 times
[2025-04-28 21:21:40,743 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,743 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [482842351]
[2025-04-28 21:21:40,743 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,743 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,785 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:40,818 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:40,818 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,818 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,153 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:41,154 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,154 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [482842351]
[2025-04-28 21:21:41,154 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [482842351] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,154 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,154 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:41,154 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [445037384]
[2025-04-28 21:21:41,154 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,154 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:41,155 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,155 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:41,155 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:41,155 INFO  L87              Difference]: Start difference. First operand 132 states and 341 transitions. Second operand  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:41,947 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,947 INFO  L93              Difference]: Finished difference Result 142 states and 438 transitions.
[2025-04-28 21:21:41,948 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:41,948 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:21:41,949 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,955 INFO  L225             Difference]: With dead ends: 142
[2025-04-28 21:21:41,956 INFO  L226             Difference]: Without dead ends: 142
[2025-04-28 21:21:41,956 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:41,957 INFO  L437           NwaCegarLoop]: 196 mSDtfsCounter, 1 mSDsluCounter, 935 mSDsCounter, 0 mSdLazyCounter, 350 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1131 SdHoareTripleChecker+Invalid, 376 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 350 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,958 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1131 Invalid, 376 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 350 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:41,960 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-04-28 21:21:42,042 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 138.
[2025-04-28 21:21:42,045 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 138 states, 37 states have (on average 2.7027027027027026) internal successors, (100), 100 states have internal predecessors, (100), 78 states have call successors, (78), 15 states have call predecessors, (78), 22 states have return successors, (214), 22 states have call predecessors, (214), 78 states have call successors, (214)
[2025-04-28 21:21:42,049 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 138 states to 138 states and 392 transitions.
[2025-04-28 21:21:42,050 INFO  L79                 Accepts]: Start accepts. Automaton has 138 states and 392 transitions. Word has length 32
[2025-04-28 21:21:42,050 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,051 INFO  L485      AbstractCegarLoop]: Abstraction has 138 states and 392 transitions.
[2025-04-28 21:21:42,051 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:42,051 INFO  L278                IsEmpty]: Start isEmpty. Operand 138 states and 392 transitions.
[2025-04-28 21:21:42,058 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:42,058 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,058 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,058 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:42,059 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,060 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,063 INFO  L85        PathProgramCache]: Analyzing trace with hash -510517557, now seen corresponding path program 1 times
[2025-04-28 21:21:42,063 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,063 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [994189891]
[2025-04-28 21:21:42,063 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,064 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,096 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:42,117 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:42,117 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,117 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,297 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:42,297 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,297 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [994189891]
[2025-04-28 21:21:42,297 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [994189891] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,297 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,297 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:42,297 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1591143596]
[2025-04-28 21:21:42,298 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,298 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:42,298 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,299 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:42,299 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,299 INFO  L87              Difference]: Start difference. First operand 138 states and 392 transitions. Second operand  has 6 states, 5 states have (on average 3.2) internal successors, (16), 6 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:42,968 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,968 INFO  L93              Difference]: Finished difference Result 148 states and 489 transitions.
[2025-04-28 21:21:42,969 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:42,969 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.2) internal successors, (16), 6 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:21:42,969 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,972 INFO  L225             Difference]: With dead ends: 148
[2025-04-28 21:21:42,972 INFO  L226             Difference]: Without dead ends: 148
[2025-04-28 21:21:42,973 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,973 INFO  L437           NwaCegarLoop]: 243 mSDtfsCounter, 1 mSDsluCounter, 910 mSDsCounter, 0 mSdLazyCounter, 278 mSolverCounterSat, 24 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1153 SdHoareTripleChecker+Invalid, 302 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 24 IncrementalHoareTripleChecker+Valid, 278 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,974 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1153 Invalid, 302 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [24 Valid, 278 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:42,976 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 148 states.
[2025-04-28 21:21:43,021 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 148 to 138.
[2025-04-28 21:21:43,025 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 138 states, 37 states have (on average 2.7027027027027026) internal successors, (100), 100 states have internal predecessors, (100), 78 states have call successors, (78), 15 states have call predecessors, (78), 22 states have return successors, (214), 22 states have call predecessors, (214), 78 states have call successors, (214)
[2025-04-28 21:21:43,028 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 138 states to 138 states and 392 transitions.
[2025-04-28 21:21:43,028 INFO  L79                 Accepts]: Start accepts. Automaton has 138 states and 392 transitions. Word has length 32
[2025-04-28 21:21:43,028 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,029 INFO  L485      AbstractCegarLoop]: Abstraction has 138 states and 392 transitions.
[2025-04-28 21:21:43,029 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.2) internal successors, (16), 6 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:43,030 INFO  L278                IsEmpty]: Start isEmpty. Operand 138 states and 392 transitions.
[2025-04-28 21:21:43,034 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:43,034 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,034 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,035 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:43,035 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,035 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,035 INFO  L85        PathProgramCache]: Analyzing trace with hash -1303369502, now seen corresponding path program 1 times
[2025-04-28 21:21:43,036 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,036 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [305944278]
[2025-04-28 21:21:43,036 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,036 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,067 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:43,088 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:43,088 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,089 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,298 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:43,298 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,298 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [305944278]
[2025-04-28 21:21:43,299 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [305944278] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,299 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,300 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:43,300 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [210805174]
[2025-04-28 21:21:43,300 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,300 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:43,301 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,301 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:43,301 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:43,301 INFO  L87              Difference]: Start difference. First operand 138 states and 392 transitions. Second operand  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:44,848 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,849 INFO  L93              Difference]: Finished difference Result 190 states and 598 transitions.
[2025-04-28 21:21:44,849 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:44,849 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9) Word has length 36
[2025-04-28 21:21:44,850 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,854 INFO  L225             Difference]: With dead ends: 190
[2025-04-28 21:21:44,854 INFO  L226             Difference]: Without dead ends: 190
[2025-04-28 21:21:44,854 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:44,855 INFO  L437           NwaCegarLoop]: 308 mSDtfsCounter, 27 mSDsluCounter, 1358 mSDsCounter, 0 mSdLazyCounter, 676 mSolverCounterSat, 55 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 54 SdHoareTripleChecker+Valid, 1666 SdHoareTripleChecker+Invalid, 731 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 55 IncrementalHoareTripleChecker+Valid, 676 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,855 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [54 Valid, 1666 Invalid, 731 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [55 Valid, 676 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-04-28 21:21:44,856 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 190 states.
[2025-04-28 21:21:44,894 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 190 to 180.
[2025-04-28 21:21:44,895 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 180 states, 47 states have (on average 2.851063829787234) internal successors, (134), 132 states have internal predecessors, (134), 103 states have call successors, (103), 18 states have call predecessors, (103), 29 states have return successors, (308), 29 states have call predecessors, (308), 103 states have call successors, (308)
[2025-04-28 21:21:44,897 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 180 states to 180 states and 545 transitions.
[2025-04-28 21:21:44,897 INFO  L79                 Accepts]: Start accepts. Automaton has 180 states and 545 transitions. Word has length 36
[2025-04-28 21:21:44,897 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,898 INFO  L485      AbstractCegarLoop]: Abstraction has 180 states and 545 transitions.
[2025-04-28 21:21:44,898 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:44,898 INFO  L278                IsEmpty]: Start isEmpty. Operand 180 states and 545 transitions.
[2025-04-28 21:21:44,902 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:44,903 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,903 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,903 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:44,903 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,903 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,903 INFO  L85        PathProgramCache]: Analyzing trace with hash -1756184482, now seen corresponding path program 1 times
[2025-04-28 21:21:44,904 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,904 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [690568680]
[2025-04-28 21:21:44,904 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,904 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,927 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:44,942 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:44,942 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,942 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,172 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:45,172 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,172 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [690568680]
[2025-04-28 21:21:45,172 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [690568680] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,172 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,172 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:45,172 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [664086136]
[2025-04-28 21:21:45,173 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,173 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:45,173 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,173 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:45,173 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:45,174 INFO  L87              Difference]: Start difference. First operand 180 states and 545 transitions. Second operand  has 7 states, 6 states have (on average 3.0) internal successors, (18), 7 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:45,921 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,921 INFO  L93              Difference]: Finished difference Result 216 states and 824 transitions.
[2025-04-28 21:21:45,922 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:45,922 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.0) internal successors, (18), 7 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:45,922 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,928 INFO  L225             Difference]: With dead ends: 216
[2025-04-28 21:21:45,928 INFO  L226             Difference]: Without dead ends: 216
[2025-04-28 21:21:45,929 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:45,931 INFO  L437           NwaCegarLoop]: 249 mSDtfsCounter, 1 mSDsluCounter, 1176 mSDsCounter, 0 mSdLazyCounter, 344 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1425 SdHoareTripleChecker+Invalid, 372 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 344 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,932 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1425 Invalid, 372 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 344 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:45,933 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 216 states.
[2025-04-28 21:21:46,043 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 216 to 212.
[2025-04-28 21:21:46,045 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 212 states, 63 states have (on average 2.380952380952381) internal successors, (150), 148 states have internal predecessors, (150), 103 states have call successors, (103), 18 states have call predecessors, (103), 45 states have return successors, (565), 45 states have call predecessors, (565), 103 states have call successors, (565)
[2025-04-28 21:21:46,050 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 212 states to 212 states and 818 transitions.
[2025-04-28 21:21:46,050 INFO  L79                 Accepts]: Start accepts. Automaton has 212 states and 818 transitions. Word has length 36
[2025-04-28 21:21:46,051 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,051 INFO  L485      AbstractCegarLoop]: Abstraction has 212 states and 818 transitions.
[2025-04-28 21:21:46,051 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.0) internal successors, (18), 7 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:46,051 INFO  L278                IsEmpty]: Start isEmpty. Operand 212 states and 818 transitions.
[2025-04-28 21:21:46,063 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:46,063 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,063 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,063 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:46,063 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,064 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,064 INFO  L85        PathProgramCache]: Analyzing trace with hash 1237794332, now seen corresponding path program 1 times
[2025-04-28 21:21:46,064 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,064 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1241637715]
[2025-04-28 21:21:46,064 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,064 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,093 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:46,112 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:46,113 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,113 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,289 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:46,290 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,290 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1241637715]
[2025-04-28 21:21:46,290 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1241637715] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,290 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,290 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:46,290 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2035223532]
[2025-04-28 21:21:46,291 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,291 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:46,291 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,292 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:46,292 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:46,292 INFO  L87              Difference]: Start difference. First operand 212 states and 818 transitions. Second operand  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:47,796 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,796 INFO  L93              Difference]: Finished difference Result 292 states and 1183 transitions.
[2025-04-28 21:21:47,797 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:47,797 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9) Word has length 36
[2025-04-28 21:21:47,797 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,805 INFO  L225             Difference]: With dead ends: 292
[2025-04-28 21:21:47,805 INFO  L226             Difference]: Without dead ends: 292
[2025-04-28 21:21:47,805 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:47,806 INFO  L437           NwaCegarLoop]: 312 mSDtfsCounter, 27 mSDsluCounter, 1375 mSDsCounter, 0 mSdLazyCounter, 664 mSolverCounterSat, 53 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 53 SdHoareTripleChecker+Valid, 1687 SdHoareTripleChecker+Invalid, 717 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 53 IncrementalHoareTripleChecker+Valid, 664 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,806 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [53 Valid, 1687 Invalid, 717 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [53 Valid, 664 Invalid, 0 Unknown, 0 Unchecked, 1.4s Time]
[2025-04-28 21:21:47,807 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 292 states.
[2025-04-28 21:21:47,906 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 292 to 268.
[2025-04-28 21:21:47,907 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 268 states, 80 states have (on average 2.375) internal successors, (190), 187 states have internal predecessors, (190), 128 states have call successors, (128), 21 states have call predecessors, (128), 59 states have return successors, (763), 59 states have call predecessors, (763), 128 states have call successors, (763)
[2025-04-28 21:21:47,912 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 268 states to 268 states and 1081 transitions.
[2025-04-28 21:21:47,912 INFO  L79                 Accepts]: Start accepts. Automaton has 268 states and 1081 transitions. Word has length 36
[2025-04-28 21:21:47,912 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,912 INFO  L485      AbstractCegarLoop]: Abstraction has 268 states and 1081 transitions.
[2025-04-28 21:21:47,912 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 3.6) internal successors, (18), 7 states have internal predecessors, (18), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:47,913 INFO  L278                IsEmpty]: Start isEmpty. Operand 268 states and 1081 transitions.
[2025-04-28 21:21:47,921 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:47,921 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,922 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,922 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:47,922 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,922 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,922 INFO  L85        PathProgramCache]: Analyzing trace with hash -1121677466, now seen corresponding path program 1 times
[2025-04-28 21:21:47,922 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,922 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2027413003]
[2025-04-28 21:21:47,923 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,923 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,949 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:47,963 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:47,963 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,963 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,085 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:48,085 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,085 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2027413003]
[2025-04-28 21:21:48,085 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2027413003] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,085 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,085 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:48,085 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [221538217]
[2025-04-28 21:21:48,087 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,087 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:48,087 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,088 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:48,088 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:48,088 INFO  L87              Difference]: Start difference. First operand 268 states and 1081 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:48,884 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,885 INFO  L93              Difference]: Finished difference Result 334 states and 1552 transitions.
[2025-04-28 21:21:48,885 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:48,885 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:48,886 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,894 INFO  L225             Difference]: With dead ends: 334
[2025-04-28 21:21:48,895 INFO  L226             Difference]: Without dead ends: 334
[2025-04-28 21:21:48,895 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:48,895 INFO  L437           NwaCegarLoop]: 250 mSDtfsCounter, 1 mSDsluCounter, 897 mSDsCounter, 0 mSdLazyCounter, 333 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1147 SdHoareTripleChecker+Invalid, 341 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 333 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,896 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1147 Invalid, 341 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 333 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:48,897 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 334 states.
[2025-04-28 21:21:49,033 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 334 to 308.
[2025-04-28 21:21:49,034 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 308 states, 100 states have (on average 2.1) internal successors, (210), 207 states have internal predecessors, (210), 128 states have call successors, (128), 21 states have call predecessors, (128), 79 states have return successors, (1069), 79 states have call predecessors, (1069), 128 states have call successors, (1069)
[2025-04-28 21:21:49,040 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 308 states to 308 states and 1407 transitions.
[2025-04-28 21:21:49,040 INFO  L79                 Accepts]: Start accepts. Automaton has 308 states and 1407 transitions. Word has length 36
[2025-04-28 21:21:49,040 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,041 INFO  L485      AbstractCegarLoop]: Abstraction has 308 states and 1407 transitions.
[2025-04-28 21:21:49,041 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:49,041 INFO  L278                IsEmpty]: Start isEmpty. Operand 308 states and 1407 transitions.
[2025-04-28 21:21:49,052 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:49,053 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,055 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,059 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:49,059 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,059 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,059 INFO  L85        PathProgramCache]: Analyzing trace with hash 1410894052, now seen corresponding path program 1 times
[2025-04-28 21:21:49,060 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,060 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1658852435]
[2025-04-28 21:21:49,060 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,060 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,087 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:49,099 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:49,099 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,099 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,234 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:49,235 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,235 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1658852435]
[2025-04-28 21:21:49,235 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1658852435] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,235 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,235 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:49,235 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1002389362]
[2025-04-28 21:21:49,235 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,235 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:49,236 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,236 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:49,236 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:49,236 INFO  L87              Difference]: Start difference. First operand 308 states and 1407 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:50,036 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,036 INFO  L93              Difference]: Finished difference Result 368 states and 1853 transitions.
[2025-04-28 21:21:50,037 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:50,037 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:50,037 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,048 INFO  L225             Difference]: With dead ends: 368
[2025-04-28 21:21:50,048 INFO  L226             Difference]: Without dead ends: 368
[2025-04-28 21:21:50,049 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:50,050 INFO  L437           NwaCegarLoop]: 237 mSDtfsCounter, 1 mSDsluCounter, 853 mSDsCounter, 0 mSdLazyCounter, 327 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1090 SdHoareTripleChecker+Invalid, 337 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 327 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,050 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1090 Invalid, 337 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 327 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:50,051 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 368 states.
[2025-04-28 21:21:50,238 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 368 to 338.
[2025-04-28 21:21:50,239 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 338 states, 115 states have (on average 1.9565217391304348) internal successors, (225), 222 states have internal predecessors, (225), 128 states have call successors, (128), 21 states have call predecessors, (128), 94 states have return successors, (1212), 94 states have call predecessors, (1212), 128 states have call successors, (1212)
[2025-04-28 21:21:50,246 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 338 states to 338 states and 1565 transitions.
[2025-04-28 21:21:50,246 INFO  L79                 Accepts]: Start accepts. Automaton has 338 states and 1565 transitions. Word has length 36
[2025-04-28 21:21:50,248 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,248 INFO  L485      AbstractCegarLoop]: Abstraction has 338 states and 1565 transitions.
[2025-04-28 21:21:50,248 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:50,248 INFO  L278                IsEmpty]: Start isEmpty. Operand 338 states and 1565 transitions.
[2025-04-28 21:21:50,260 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:50,260 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,260 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,260 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:50,261 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,262 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,262 INFO  L85        PathProgramCache]: Analyzing trace with hash 191542445, now seen corresponding path program 1 times
[2025-04-28 21:21:50,262 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,262 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [341220506]
[2025-04-28 21:21:50,262 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,263 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,293 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:50,305 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:50,306 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,306 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,406 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:50,406 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,406 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [341220506]
[2025-04-28 21:21:50,406 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [341220506] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,407 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,407 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:50,407 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [485492078]
[2025-04-28 21:21:50,407 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,407 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:50,407 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,408 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:50,408 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:50,408 INFO  L87              Difference]: Start difference. First operand 338 states and 1565 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:51,149 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,149 INFO  L93              Difference]: Finished difference Result 350 states and 1623 transitions.
[2025-04-28 21:21:51,150 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:51,150 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:51,150 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,159 INFO  L225             Difference]: With dead ends: 350
[2025-04-28 21:21:51,159 INFO  L226             Difference]: Without dead ends: 350
[2025-04-28 21:21:51,160 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:51,161 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 1 mSDsluCounter, 646 mSDsCounter, 0 mSdLazyCounter, 273 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 894 SdHoareTripleChecker+Invalid, 277 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 273 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,161 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 894 Invalid, 277 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 273 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:51,162 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 350 states.
[2025-04-28 21:21:51,312 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 350 to 342.
[2025-04-28 21:21:51,313 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 342 states, 117 states have (on average 1.9401709401709402) internal successors, (227), 224 states have internal predecessors, (227), 128 states have call successors, (128), 21 states have call predecessors, (128), 96 states have return successors, (1216), 96 states have call predecessors, (1216), 128 states have call successors, (1216)
[2025-04-28 21:21:51,321 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 342 states to 342 states and 1571 transitions.
[2025-04-28 21:21:51,321 INFO  L79                 Accepts]: Start accepts. Automaton has 342 states and 1571 transitions. Word has length 36
[2025-04-28 21:21:51,322 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,322 INFO  L485      AbstractCegarLoop]: Abstraction has 342 states and 1571 transitions.
[2025-04-28 21:21:51,322 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:51,322 INFO  L278                IsEmpty]: Start isEmpty. Operand 342 states and 1571 transitions.
[2025-04-28 21:21:51,333 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:51,334 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,334 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,334 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:51,334 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,335 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,335 INFO  L85        PathProgramCache]: Analyzing trace with hash -96801177, now seen corresponding path program 1 times
[2025-04-28 21:21:51,335 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,335 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [556829182]
[2025-04-28 21:21:51,335 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,335 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,366 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:51,379 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:51,379 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,380 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,489 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:51,489 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,489 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [556829182]
[2025-04-28 21:21:51,489 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [556829182] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,489 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,490 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:51,490 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1497759570]
[2025-04-28 21:21:51,490 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,490 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:51,490 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,491 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:51,491 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:51,491 INFO  L87              Difference]: Start difference. First operand 342 states and 1571 transitions. Second operand  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:52,298 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,298 INFO  L93              Difference]: Finished difference Result 402 states and 2017 transitions.
[2025-04-28 21:21:52,299 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:52,300 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:52,300 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,311 INFO  L225             Difference]: With dead ends: 402
[2025-04-28 21:21:52,311 INFO  L226             Difference]: Without dead ends: 402
[2025-04-28 21:21:52,311 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:52,312 INFO  L437           NwaCegarLoop]: 249 mSDtfsCounter, 1 mSDsluCounter, 894 mSDsCounter, 0 mSdLazyCounter, 331 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1143 SdHoareTripleChecker+Invalid, 339 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 331 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,312 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1143 Invalid, 339 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 331 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:52,313 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 402 states.
[2025-04-28 21:21:52,509 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 402 to 342.
[2025-04-28 21:21:52,511 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 342 states, 117 states have (on average 1.9401709401709402) internal successors, (227), 224 states have internal predecessors, (227), 128 states have call successors, (128), 21 states have call predecessors, (128), 96 states have return successors, (1216), 96 states have call predecessors, (1216), 128 states have call successors, (1216)
[2025-04-28 21:21:52,518 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 342 states to 342 states and 1571 transitions.
[2025-04-28 21:21:52,518 INFO  L79                 Accepts]: Start accepts. Automaton has 342 states and 1571 transitions. Word has length 36
[2025-04-28 21:21:52,519 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,519 INFO  L485      AbstractCegarLoop]: Abstraction has 342 states and 1571 transitions.
[2025-04-28 21:21:52,519 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 3.6) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:52,519 INFO  L278                IsEmpty]: Start isEmpty. Operand 342 states and 1571 transitions.
[2025-04-28 21:21:52,531 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:52,531 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,531 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,531 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:52,532 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,532 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,533 INFO  L85        PathProgramCache]: Analyzing trace with hash 1639224285, now seen corresponding path program 1 times
[2025-04-28 21:21:52,533 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,533 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [580113861]
[2025-04-28 21:21:52,534 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,534 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,564 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:52,582 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:52,583 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,583 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,785 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:52,785 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,785 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [580113861]
[2025-04-28 21:21:52,786 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [580113861] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,786 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,786 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:52,786 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [885477766]
[2025-04-28 21:21:52,786 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,786 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:52,786 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,787 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:52,787 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:52,787 INFO  L87              Difference]: Start difference. First operand 342 states and 1571 transitions. Second operand  has 8 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 8 states have internal predecessors, (17), 3 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:53,680 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,681 INFO  L93              Difference]: Finished difference Result 404 states and 2002 transitions.
[2025-04-28 21:21:53,681 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:53,682 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 8 states have internal predecessors, (17), 3 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:53,682 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,692 INFO  L225             Difference]: With dead ends: 404
[2025-04-28 21:21:53,692 INFO  L226             Difference]: Without dead ends: 404
[2025-04-28 21:21:53,693 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:53,693 INFO  L437           NwaCegarLoop]: 195 mSDtfsCounter, 1 mSDsluCounter, 1127 mSDsCounter, 0 mSdLazyCounter, 422 mSolverCounterSat, 30 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 1322 SdHoareTripleChecker+Invalid, 452 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 30 IncrementalHoareTripleChecker+Valid, 422 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,693 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 1322 Invalid, 452 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [30 Valid, 422 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:53,694 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 404 states.
[2025-04-28 21:21:53,897 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 404 to 400.
[2025-04-28 21:21:53,899 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 400 states, 146 states have (on average 1.7534246575342465) internal successors, (256), 253 states have internal predecessors, (256), 128 states have call successors, (128), 21 states have call predecessors, (128), 125 states have return successors, (1612), 125 states have call predecessors, (1612), 128 states have call successors, (1612)
[2025-04-28 21:21:53,906 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 400 states to 400 states and 1996 transitions.
[2025-04-28 21:21:53,907 INFO  L79                 Accepts]: Start accepts. Automaton has 400 states and 1996 transitions. Word has length 36
[2025-04-28 21:21:53,907 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,907 INFO  L485      AbstractCegarLoop]: Abstraction has 400 states and 1996 transitions.
[2025-04-28 21:21:53,907 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 8 states have internal predecessors, (17), 3 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:53,907 INFO  L278                IsEmpty]: Start isEmpty. Operand 400 states and 1996 transitions.
[2025-04-28 21:21:53,917 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:53,917 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,917 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,917 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:53,917 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,918 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,918 INFO  L85        PathProgramCache]: Analyzing trace with hash -106488750, now seen corresponding path program 1 times
[2025-04-28 21:21:53,918 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,918 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1940920426]
[2025-04-28 21:21:53,918 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,918 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,941 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:53,950 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:53,950 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,950 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,028 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:54,029 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,029 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1940920426]
[2025-04-28 21:21:54,029 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1940920426] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,029 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,029 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:54,029 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [850335749]
[2025-04-28 21:21:54,029 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,029 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:54,030 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,030 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:54,030 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:54,031 INFO  L87              Difference]: Start difference. First operand 400 states and 1996 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:54,747 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,748 INFO  L93              Difference]: Finished difference Result 412 states and 2054 transitions.
[2025-04-28 21:21:54,748 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:54,749 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:54,749 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,763 INFO  L225             Difference]: With dead ends: 412
[2025-04-28 21:21:54,763 INFO  L226             Difference]: Without dead ends: 412
[2025-04-28 21:21:54,763 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:54,764 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 1 mSDsluCounter, 646 mSDsCounter, 0 mSdLazyCounter, 273 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 894 SdHoareTripleChecker+Invalid, 277 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 273 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,764 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 894 Invalid, 277 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 273 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:54,765 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 412 states.
[2025-04-28 21:21:55,037 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 412 to 400.
[2025-04-28 21:21:55,039 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 400 states, 146 states have (on average 1.7534246575342465) internal successors, (256), 253 states have internal predecessors, (256), 128 states have call successors, (128), 21 states have call predecessors, (128), 125 states have return successors, (1612), 125 states have call predecessors, (1612), 128 states have call successors, (1612)
[2025-04-28 21:21:55,046 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 400 states to 400 states and 1996 transitions.
[2025-04-28 21:21:55,046 INFO  L79                 Accepts]: Start accepts. Automaton has 400 states and 1996 transitions. Word has length 36
[2025-04-28 21:21:55,047 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,047 INFO  L485      AbstractCegarLoop]: Abstraction has 400 states and 1996 transitions.
[2025-04-28 21:21:55,047 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:55,047 INFO  L278                IsEmpty]: Start isEmpty. Operand 400 states and 1996 transitions.
[2025-04-28 21:21:55,056 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:55,056 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,056 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,057 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:55,057 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,057 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,057 INFO  L85        PathProgramCache]: Analyzing trace with hash -1965679158, now seen corresponding path program 1 times
[2025-04-28 21:21:55,058 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,058 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1807509854]
[2025-04-28 21:21:55,058 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,058 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,082 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:55,092 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:55,092 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,092 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,173 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,173 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,174 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1807509854]
[2025-04-28 21:21:55,174 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1807509854] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,174 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,174 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:55,174 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [524903963]
[2025-04-28 21:21:55,174 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,174 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:55,174 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,175 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:55,175 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:55,175 INFO  L87              Difference]: Start difference. First operand 400 states and 1996 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:55,918 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,918 INFO  L93              Difference]: Finished difference Result 412 states and 2054 transitions.
[2025-04-28 21:21:55,919 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:55,919 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:55,920 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,930 INFO  L225             Difference]: With dead ends: 412
[2025-04-28 21:21:55,930 INFO  L226             Difference]: Without dead ends: 412
[2025-04-28 21:21:55,931 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,932 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 1 mSDsluCounter, 647 mSDsCounter, 0 mSdLazyCounter, 274 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 895 SdHoareTripleChecker+Invalid, 277 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 274 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,933 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 895 Invalid, 277 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 274 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:55,934 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 412 states.
[2025-04-28 21:21:56,144 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 412 to 400.
[2025-04-28 21:21:56,146 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 400 states, 146 states have (on average 1.7534246575342465) internal successors, (256), 253 states have internal predecessors, (256), 128 states have call successors, (128), 21 states have call predecessors, (128), 125 states have return successors, (1612), 125 states have call predecessors, (1612), 128 states have call successors, (1612)
[2025-04-28 21:21:56,161 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 400 states to 400 states and 1996 transitions.
[2025-04-28 21:21:56,161 INFO  L79                 Accepts]: Start accepts. Automaton has 400 states and 1996 transitions. Word has length 36
[2025-04-28 21:21:56,161 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,162 INFO  L485      AbstractCegarLoop]: Abstraction has 400 states and 1996 transitions.
[2025-04-28 21:21:56,162 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:56,163 INFO  L278                IsEmpty]: Start isEmpty. Operand 400 states and 1996 transitions.
[2025-04-28 21:21:56,172 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:56,172 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,172 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,173 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:56,173 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,174 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,174 INFO  L85        PathProgramCache]: Analyzing trace with hash 1582046325, now seen corresponding path program 1 times
[2025-04-28 21:21:56,174 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,174 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1145983504]
[2025-04-28 21:21:56,174 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,174 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,200 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:56,211 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:56,211 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,211 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,309 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,310 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,310 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1145983504]
[2025-04-28 21:21:56,310 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1145983504] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:56,310 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:56,310 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:56,310 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1417869578]
[2025-04-28 21:21:56,310 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,310 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:56,311 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,311 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:56,311 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:56,311 INFO  L87              Difference]: Start difference. First operand 400 states and 1996 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:57,011 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,011 INFO  L93              Difference]: Finished difference Result 412 states and 2054 transitions.
[2025-04-28 21:21:57,012 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:57,012 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:57,012 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,021 INFO  L225             Difference]: With dead ends: 412
[2025-04-28 21:21:57,021 INFO  L226             Difference]: Without dead ends: 412
[2025-04-28 21:21:57,022 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,022 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 1 mSDsluCounter, 646 mSDsCounter, 0 mSdLazyCounter, 273 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 894 SdHoareTripleChecker+Invalid, 277 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 273 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,022 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 894 Invalid, 277 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 273 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:57,023 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 412 states.
[2025-04-28 21:21:57,196 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 412 to 400.
[2025-04-28 21:21:57,198 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 400 states, 146 states have (on average 1.7534246575342465) internal successors, (256), 253 states have internal predecessors, (256), 128 states have call successors, (128), 21 states have call predecessors, (128), 125 states have return successors, (1612), 125 states have call predecessors, (1612), 128 states have call successors, (1612)
[2025-04-28 21:21:57,204 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 400 states to 400 states and 1996 transitions.
[2025-04-28 21:21:57,204 INFO  L79                 Accepts]: Start accepts. Automaton has 400 states and 1996 transitions. Word has length 36
[2025-04-28 21:21:57,204 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,204 INFO  L485      AbstractCegarLoop]: Abstraction has 400 states and 1996 transitions.
[2025-04-28 21:21:57,205 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:57,205 INFO  L278                IsEmpty]: Start isEmpty. Operand 400 states and 1996 transitions.
[2025-04-28 21:21:57,212 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:57,212 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,212 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,213 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:21:57,213 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,213 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,213 INFO  L85        PathProgramCache]: Analyzing trace with hash 2070840674, now seen corresponding path program 1 times
[2025-04-28 21:21:57,213 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,213 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [659986964]
[2025-04-28 21:21:57,213 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,214 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,234 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:57,243 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:57,243 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,243 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,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:21:57,326 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,326 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [659986964]
[2025-04-28 21:21:57,326 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [659986964] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:57,326 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:57,328 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:57,328 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1387380400]
[2025-04-28 21:21:57,328 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,329 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:57,329 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,329 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:57,329 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:57,329 INFO  L87              Difference]: Start difference. First operand 400 states and 1996 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:57,981 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,981 INFO  L93              Difference]: Finished difference Result 446 states and 2266 transitions.
[2025-04-28 21:21:57,982 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:57,982 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:57,982 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,991 INFO  L225             Difference]: With dead ends: 446
[2025-04-28 21:21:57,991 INFO  L226             Difference]: Without dead ends: 446
[2025-04-28 21:21:57,992 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,993 INFO  L437           NwaCegarLoop]: 251 mSDtfsCounter, 1 mSDsluCounter, 657 mSDsCounter, 0 mSdLazyCounter, 277 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 908 SdHoareTripleChecker+Invalid, 279 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 277 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,993 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 908 Invalid, 279 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 277 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:57,994 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 446 states.
[2025-04-28 21:21:58,219 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 446 to 370.
[2025-04-28 21:21:58,221 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 370 states, 131 states have (on average 1.8396946564885497) internal successors, (241), 238 states have internal predecessors, (241), 128 states have call successors, (128), 21 states have call predecessors, (128), 110 states have return successors, (1422), 110 states have call predecessors, (1422), 128 states have call successors, (1422)
[2025-04-28 21:21:58,227 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 370 states to 370 states and 1791 transitions.
[2025-04-28 21:21:58,227 INFO  L79                 Accepts]: Start accepts. Automaton has 370 states and 1791 transitions. Word has length 36
[2025-04-28 21:21:58,228 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,229 INFO  L485      AbstractCegarLoop]: Abstraction has 370 states and 1791 transitions.
[2025-04-28 21:21:58,229 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:58,229 INFO  L278                IsEmpty]: Start isEmpty. Operand 370 states and 1791 transitions.
[2025-04-28 21:21:58,237 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:58,237 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,237 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,237 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:21:58,237 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,238 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,238 INFO  L85        PathProgramCache]: Analyzing trace with hash -1584098528, now seen corresponding path program 1 times
[2025-04-28 21:21:58,238 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,239 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1104377177]
[2025-04-28 21:21:58,239 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,239 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,266 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:58,275 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:58,275 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,275 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,360 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,360 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,360 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1104377177]
[2025-04-28 21:21:58,360 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1104377177] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:58,360 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:58,360 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:58,360 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1202301674]
[2025-04-28 21:21:58,361 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,361 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:58,361 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,362 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:58,362 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:58,362 INFO  L87              Difference]: Start difference. First operand 370 states and 1791 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:58,997 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,997 INFO  L93              Difference]: Finished difference Result 388 states and 1813 transitions.
[2025-04-28 21:21:58,998 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:58,998 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:58,998 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,006 INFO  L225             Difference]: With dead ends: 388
[2025-04-28 21:21:59,006 INFO  L226             Difference]: Without dead ends: 388
[2025-04-28 21:21:59,007 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,007 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 1 mSDsluCounter, 648 mSDsCounter, 0 mSdLazyCounter, 273 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 896 SdHoareTripleChecker+Invalid, 275 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 273 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,007 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 896 Invalid, 275 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 273 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:59,008 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 388 states.
[2025-04-28 21:21:59,164 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 388 to 360.
[2025-04-28 21:21:59,165 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 360 states, 126 states have (on average 1.873015873015873) internal successors, (236), 233 states have internal predecessors, (236), 128 states have call successors, (128), 21 states have call predecessors, (128), 105 states have return successors, (1290), 105 states have call predecessors, (1290), 128 states have call successors, (1290)
[2025-04-28 21:21:59,170 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 360 states to 360 states and 1654 transitions.
[2025-04-28 21:21:59,170 INFO  L79                 Accepts]: Start accepts. Automaton has 360 states and 1654 transitions. Word has length 36
[2025-04-28 21:21:59,171 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,171 INFO  L485      AbstractCegarLoop]: Abstraction has 360 states and 1654 transitions.
[2025-04-28 21:21:59,171 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 5 states have internal predecessors, (18), 3 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:59,171 INFO  L278                IsEmpty]: Start isEmpty. Operand 360 states and 1654 transitions.
[2025-04-28 21:21:59,178 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:59,178 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,178 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,178 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:21:59,178 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,179 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,179 INFO  L85        PathProgramCache]: Analyzing trace with hash 1888788775, now seen corresponding path program 1 times
[2025-04-28 21:21:59,179 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,179 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2067204279]
[2025-04-28 21:21:59,180 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,180 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,199 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:59,207 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:59,208 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,208 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,285 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,286 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,286 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2067204279]
[2025-04-28 21:21:59,286 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2067204279] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,286 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:59,286 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:59,286 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1780269618]
[2025-04-28 21:21:59,286 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,287 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:59,287 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,288 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:59,288 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:59,288 INFO  L87              Difference]: Start difference. First operand 360 states and 1654 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:00,135 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,135 INFO  L93              Difference]: Finished difference Result 372 states and 1708 transitions.
[2025-04-28 21:22:00,136 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:00,136 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:00,136 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,145 INFO  L225             Difference]: With dead ends: 372
[2025-04-28 21:22:00,145 INFO  L226             Difference]: Without dead ends: 372
[2025-04-28 21:22:00,146 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,146 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 1 mSDsluCounter, 645 mSDsCounter, 0 mSdLazyCounter, 272 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 893 SdHoareTripleChecker+Invalid, 277 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 272 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,147 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 893 Invalid, 277 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 272 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:00,148 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 372 states.
[2025-04-28 21:22:00,289 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 372 to 360.
[2025-04-28 21:22:00,291 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 360 states, 126 states have (on average 1.873015873015873) internal successors, (236), 233 states have internal predecessors, (236), 128 states have call successors, (128), 21 states have call predecessors, (128), 105 states have return successors, (1286), 105 states have call predecessors, (1286), 128 states have call successors, (1286)
[2025-04-28 21:22:00,298 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 360 states to 360 states and 1650 transitions.
[2025-04-28 21:22:00,298 INFO  L79                 Accepts]: Start accepts. Automaton has 360 states and 1650 transitions. Word has length 36
[2025-04-28 21:22:00,298 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,298 INFO  L485      AbstractCegarLoop]: Abstraction has 360 states and 1650 transitions.
[2025-04-28 21:22:00,299 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:00,299 INFO  L278                IsEmpty]: Start isEmpty. Operand 360 states and 1650 transitions.
[2025-04-28 21:22:00,307 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:22:00,307 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,307 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:00,307 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-04-28 21:22:00,307 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,309 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,309 INFO  L85        PathProgramCache]: Analyzing trace with hash 1708720126, now seen corresponding path program 1 times
[2025-04-28 21:22:00,309 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,309 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [757577489]
[2025-04-28 21:22:00,309 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,309 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,333 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:22:00,343 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:22:00,343 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,343 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,493 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,493 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,493 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [757577489]
[2025-04-28 21:22:00,493 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [757577489] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:00,494 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:00,494 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:00,494 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [880616815]
[2025-04-28 21:22:00,494 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,494 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:00,495 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,496 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:00,496 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:00,496 INFO  L87              Difference]: Start difference. First operand 360 states and 1650 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)
