./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-042.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:23,846 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:23,931 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8be6e6c0-daa7-4bbf-89dd-a6b2f29773b5/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:23,937 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:23,937 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:23,982 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:23,983 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:23,984 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:23,984 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:23,986 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:23,986 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:23,986 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:23,986 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:23,987 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:23,987 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:23,987 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:23,987 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:23,987 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:23,987 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:23,988 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:23,988 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:23,988 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:23,988 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:23,988 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:23,990 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:23,991 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:23,991 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:24,390 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:24,404 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:24,407 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:24,411 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:24,411 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:24,413 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8be6e6c0-daa7-4bbf-89dd-a6b2f29773b5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-042.smt2
[2025-04-28 21:21:24,417 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:24,421 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:27,926 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8be6e6c0-daa7-4bbf-89dd-a6b2f29773b5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-042.smt2
[2025-04-28 21:21:27,931 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:27,934 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:27,935 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:27,936 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:27,936 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:27,941 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:28,177 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28 Unit
[2025-04-28 21:21:28,177 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:28,179 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:28,179 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:28,180 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:28,197 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,197 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,312 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,316 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,403 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,417 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,422 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,454 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,474 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,569 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:28,570 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:28,570 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:28,571 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:28,572 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,575 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:28,591 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,606 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:28,611 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:28,624 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:28,624 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:28,624 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:28,624 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:28,624 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:28,624 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:28,625 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcmainStart__syn given in one single declaration
[2025-04-28 21:21:28,625 INFO  L130     BoogieDeclarations]: Found specification of procedure funcmainStart__syn
[2025-04-28 21:21:28,625 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcmainStart__syn
[2025-04-28 21:21:28,625 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:28,625 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:28,626 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:28,626 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT12__syn given in one single declaration
[2025-04-28 21:21:28,626 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT12__syn
[2025-04-28 21:21:28,626 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT12__syn
[2025-04-28 21:21:28,626 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT14__syn given in one single declaration
[2025-04-28 21:21:28,626 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT14__syn
[2025-04-28 21:21:28,626 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT14__syn
[2025-04-28 21:21:28,628 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT15__syn given in one single declaration
[2025-04-28 21:21:28,628 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT15__syn
[2025-04-28 21:21:28,628 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT15__syn
[2025-04-28 21:21:28,629 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT9__syn given in one single declaration
[2025-04-28 21:21:28,629 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT9__syn
[2025-04-28 21:21:28,629 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT9__syn
[2025-04-28 21:21:28,629 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT11__syn given in one single declaration
[2025-04-28 21:21:28,629 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT11__syn
[2025-04-28 21:21:28,629 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT11__syn
[2025-04-28 21:21:28,629 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT5__syn given in one single declaration
[2025-04-28 21:21:28,629 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT5__syn
[2025-04-28 21:21:28,629 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT5__syn
[2025-04-28 21:21:28,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT6__syn given in one single declaration
[2025-04-28 21:21:28,630 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT6__syn
[2025-04-28 21:21:28,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT6__syn
[2025-04-28 21:21:28,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT7__syn given in one single declaration
[2025-04-28 21:21:28,630 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT7__syn
[2025-04-28 21:21:28,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT7__syn
[2025-04-28 21:21:28,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT4__syn given in one single declaration
[2025-04-28 21:21:28,630 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT4__syn
[2025-04-28 21:21:28,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT4__syn
[2025-04-28 21:21:28,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT8__syn given in one single declaration
[2025-04-28 21:21:28,630 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT8__syn
[2025-04-28 21:21:28,630 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT8__syn
[2025-04-28 21:21:28,630 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT3__syn given in one single declaration
[2025-04-28 21:21:28,631 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT3__syn
[2025-04-28 21:21:28,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT3__syn
[2025-04-28 21:21:28,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT10__syn given in one single declaration
[2025-04-28 21:21:28,631 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT10__syn
[2025-04-28 21:21:28,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT10__syn
[2025-04-28 21:21:28,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT2__syn given in one single declaration
[2025-04-28 21:21:28,631 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT2__syn
[2025-04-28 21:21:28,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT2__syn
[2025-04-28 21:21:28,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT13__syn given in one single declaration
[2025-04-28 21:21:28,631 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT13__syn
[2025-04-28 21:21:28,631 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT13__syn
[2025-04-28 21:21:28,631 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT1__syn given in one single declaration
[2025-04-28 21:21:28,631 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT1__syn
[2025-04-28 21:21:28,632 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT1__syn
[2025-04-28 21:21:28,632 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:28,632 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:28,632 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:29,593 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:29,598 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:36,570 INFO  L?                        ?]: Removed 455 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:36,570 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:36,600 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:36,601 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:36,601 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:36 BoogieIcfgContainer
[2025-04-28 21:21:36,602 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:36,604 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:36,604 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:36,609 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:36,609 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:27" (1/3) ...
[2025-04-28 21:21:36,610 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@167081d6 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:36, skipping insertion in model container
[2025-04-28 21:21:36,611 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (2/3) ...
[2025-04-28 21:21:36,611 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@167081d6 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:36, skipping insertion in model container
[2025-04-28 21:21:36,611 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:36" (3/3) ...
[2025-04-28 21:21:36,613 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:36,632 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:36,636 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 20 procedures, 319 locations, 928 edges, 20 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:36,729 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:36,749 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;@770b192f, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:36,751 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:36,757 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 319 states, 39 states have (on average 3.871794871794872) internal successors, (151), 133 states have internal predecessors, (151), 259 states have call successors, (259), 19 states have call predecessors, (259), 19 states have return successors, (259), 168 states have call predecessors, (259), 259 states have call successors, (259)
[2025-04-28 21:21:36,800 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:36,800 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,801 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,802 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,809 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,809 INFO  L85        PathProgramCache]: Analyzing trace with hash -1620155766, now seen corresponding path program 1 times
[2025-04-28 21:21:36,819 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,820 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [806035511]
[2025-04-28 21:21:36,820 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,821 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,929 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:37,187 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:37,191 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,192 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,519 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:39,520 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,523 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [806035511]
[2025-04-28 21:21:39,524 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [806035511] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,524 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,531 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:39,533 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1044196596]
[2025-04-28 21:21:39,538 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,546 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:39,548 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,626 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:39,631 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:39,634 INFO  L87              Difference]: Start difference. First operand  has 319 states, 39 states have (on average 3.871794871794872) internal successors, (151), 133 states have internal predecessors, (151), 259 states have call successors, (259), 19 states have call predecessors, (259), 19 states have return successors, (259), 168 states have call predecessors, (259), 259 states have call successors, (259) Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:40,444 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,444 INFO  L93              Difference]: Finished difference Result 321 states and 670 transitions.
[2025-04-28 21:21:40,447 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:40,448 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:40,449 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,476 INFO  L225             Difference]: With dead ends: 321
[2025-04-28 21:21:40,480 INFO  L226             Difference]: Without dead ends: 317
[2025-04-28 21:21:40,483 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:40,488 INFO  L437           NwaCegarLoop]: 665 mSDtfsCounter, 3 mSDsluCounter, 2607 mSDsCounter, 0 mSdLazyCounter, 55 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 3272 SdHoareTripleChecker+Invalid, 56 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 55 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,489 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 3272 Invalid, 56 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [1 Valid, 55 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:40,511 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 317 states.
[2025-04-28 21:21:40,630 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 317 to 317.
[2025-04-28 21:21:40,633 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 317 states, 38 states have (on average 3.8684210526315788) internal successors, (147), 131 states have internal predecessors, (147), 259 states have call successors, (259), 19 states have call predecessors, (259), 19 states have return successors, (259), 168 states have call predecessors, (259), 259 states have call successors, (259)
[2025-04-28 21:21:40,658 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 317 states to 317 states and 665 transitions.
[2025-04-28 21:21:40,661 INFO  L79                 Accepts]: Start accepts. Automaton has 317 states and 665 transitions. Word has length 16
[2025-04-28 21:21:40,662 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,662 INFO  L485      AbstractCegarLoop]: Abstraction has 317 states and 665 transitions.
[2025-04-28 21:21:40,662 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:40,662 INFO  L278                IsEmpty]: Start isEmpty. Operand 317 states and 665 transitions.
[2025-04-28 21:21:40,676 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:40,677 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,677 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,677 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:40,678 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,678 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,678 INFO  L85        PathProgramCache]: Analyzing trace with hash 1973746952, now seen corresponding path program 1 times
[2025-04-28 21:21:40,679 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,679 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [785651229]
[2025-04-28 21:21:40,679 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,679 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,743 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:40,780 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:40,780 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,780 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,176 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:42,176 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,176 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [785651229]
[2025-04-28 21:21:42,176 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [785651229] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,176 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,176 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:42,177 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [950737048]
[2025-04-28 21:21:42,177 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,179 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:42,179 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,181 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:42,181 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,182 INFO  L87              Difference]: Start difference. First operand 317 states and 665 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:42,713 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,714 INFO  L93              Difference]: Finished difference Result 321 states and 668 transitions.
[2025-04-28 21:21:42,717 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:42,717 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:42,718 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,727 INFO  L225             Difference]: With dead ends: 321
[2025-04-28 21:21:42,729 INFO  L226             Difference]: Without dead ends: 317
[2025-04-28 21:21:42,730 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:42,731 INFO  L437           NwaCegarLoop]: 663 mSDtfsCounter, 3 mSDsluCounter, 2601 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 3264 SdHoareTripleChecker+Invalid, 54 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,731 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 3264 Invalid, 54 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:42,732 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 317 states.
[2025-04-28 21:21:42,800 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 317 to 317.
[2025-04-28 21:21:42,803 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 317 states, 38 states have (on average 3.8421052631578947) internal successors, (146), 131 states have internal predecessors, (146), 259 states have call successors, (259), 19 states have call predecessors, (259), 19 states have return successors, (259), 168 states have call predecessors, (259), 259 states have call successors, (259)
[2025-04-28 21:21:42,811 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 317 states to 317 states and 664 transitions.
[2025-04-28 21:21:42,811 INFO  L79                 Accepts]: Start accepts. Automaton has 317 states and 664 transitions. Word has length 16
[2025-04-28 21:21:42,811 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,812 INFO  L485      AbstractCegarLoop]: Abstraction has 317 states and 664 transitions.
[2025-04-28 21:21:42,812 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:42,812 INFO  L278                IsEmpty]: Start isEmpty. Operand 317 states and 664 transitions.
[2025-04-28 21:21:42,817 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:42,818 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,818 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,818 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:42,819 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,819 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,819 INFO  L85        PathProgramCache]: Analyzing trace with hash 709676480, now seen corresponding path program 1 times
[2025-04-28 21:21:42,819 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,820 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1517358495]
[2025-04-28 21:21:42,820 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,820 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,873 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:42,899 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:42,899 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,900 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,262 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:44,263 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,263 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1517358495]
[2025-04-28 21:21:44,264 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1517358495] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,264 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,264 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:44,264 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [840173857]
[2025-04-28 21:21:44,264 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,265 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:44,265 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,266 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:44,267 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:44,267 INFO  L87              Difference]: Start difference. First operand 317 states and 664 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:44,727 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,727 INFO  L93              Difference]: Finished difference Result 321 states and 667 transitions.
[2025-04-28 21:21:44,729 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:44,729 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:44,729 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,735 INFO  L225             Difference]: With dead ends: 321
[2025-04-28 21:21:44,736 INFO  L226             Difference]: Without dead ends: 317
[2025-04-28 21:21:44,736 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:44,737 INFO  L437           NwaCegarLoop]: 662 mSDtfsCounter, 3 mSDsluCounter, 2598 mSDsCounter, 0 mSdLazyCounter, 53 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 3260 SdHoareTripleChecker+Invalid, 53 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 53 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,737 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 3260 Invalid, 53 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 53 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:44,741 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 317 states.
[2025-04-28 21:21:44,791 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 317 to 317.
[2025-04-28 21:21:44,795 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 317 states, 38 states have (on average 3.8157894736842106) internal successors, (145), 131 states have internal predecessors, (145), 259 states have call successors, (259), 19 states have call predecessors, (259), 19 states have return successors, (259), 168 states have call predecessors, (259), 259 states have call successors, (259)
[2025-04-28 21:21:44,805 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 317 states to 317 states and 663 transitions.
[2025-04-28 21:21:44,805 INFO  L79                 Accepts]: Start accepts. Automaton has 317 states and 663 transitions. Word has length 16
[2025-04-28 21:21:44,805 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,805 INFO  L485      AbstractCegarLoop]: Abstraction has 317 states and 663 transitions.
[2025-04-28 21:21:44,806 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:44,806 INFO  L278                IsEmpty]: Start isEmpty. Operand 317 states and 663 transitions.
[2025-04-28 21:21:44,811 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:44,812 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,812 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,812 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:44,812 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,813 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,816 INFO  L85        PathProgramCache]: Analyzing trace with hash 2030406580, now seen corresponding path program 1 times
[2025-04-28 21:21:44,816 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,816 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1191303881]
[2025-04-28 21:21:44,816 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,816 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,875 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:44,907 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:44,907 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,907 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,825 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:45,826 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,826 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1191303881]
[2025-04-28 21:21:45,826 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1191303881] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,826 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,826 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:45,826 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [579434869]
[2025-04-28 21:21:45,827 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,827 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:45,827 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,828 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:45,828 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:45,828 INFO  L87              Difference]: Start difference. First operand 317 states and 663 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:46,253 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,253 INFO  L93              Difference]: Finished difference Result 321 states and 666 transitions.
[2025-04-28 21:21:46,255 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:46,255 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:46,256 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,264 INFO  L225             Difference]: With dead ends: 321
[2025-04-28 21:21:46,264 INFO  L226             Difference]: Without dead ends: 317
[2025-04-28 21:21:46,265 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:46,266 INFO  L437           NwaCegarLoop]: 661 mSDtfsCounter, 2 mSDsluCounter, 1937 mSDsCounter, 0 mSdLazyCounter, 50 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 2598 SdHoareTripleChecker+Invalid, 50 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 50 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,268 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 2598 Invalid, 50 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 50 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:46,269 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 317 states.
[2025-04-28 21:21:46,296 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 317 to 317.
[2025-04-28 21:21:46,298 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 317 states, 38 states have (on average 3.789473684210526) internal successors, (144), 131 states have internal predecessors, (144), 259 states have call successors, (259), 19 states have call predecessors, (259), 19 states have return successors, (259), 168 states have call predecessors, (259), 259 states have call successors, (259)
[2025-04-28 21:21:46,304 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 317 states to 317 states and 662 transitions.
[2025-04-28 21:21:46,307 INFO  L79                 Accepts]: Start accepts. Automaton has 317 states and 662 transitions. Word has length 16
[2025-04-28 21:21:46,307 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,308 INFO  L485      AbstractCegarLoop]: Abstraction has 317 states and 662 transitions.
[2025-04-28 21:21:46,308 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:46,308 INFO  L278                IsEmpty]: Start isEmpty. Operand 317 states and 662 transitions.
[2025-04-28 21:21:46,312 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:46,312 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,313 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,313 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:46,313 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,313 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,313 INFO  L85        PathProgramCache]: Analyzing trace with hash 1467400686, now seen corresponding path program 1 times
[2025-04-28 21:21:46,313 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,313 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [979548659]
[2025-04-28 21:21:46,314 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,314 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,368 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:46,398 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:46,398 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,399 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,441 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:47,441 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,441 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [979548659]
[2025-04-28 21:21:47,441 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [979548659] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,441 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,441 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:47,441 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [71224104]
[2025-04-28 21:21:47,441 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,442 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:47,442 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,442 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:47,442 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:47,443 INFO  L87              Difference]: Start difference. First operand 317 states and 662 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:47,857 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,858 INFO  L93              Difference]: Finished difference Result 321 states and 665 transitions.
[2025-04-28 21:21:47,859 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:47,860 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:47,860 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,865 INFO  L225             Difference]: With dead ends: 321
[2025-04-28 21:21:47,866 INFO  L226             Difference]: Without dead ends: 317
[2025-04-28 21:21:47,866 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:47,867 INFO  L437           NwaCegarLoop]: 660 mSDtfsCounter, 3 mSDsluCounter, 2592 mSDsCounter, 0 mSdLazyCounter, 51 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 3252 SdHoareTripleChecker+Invalid, 51 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 51 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,867 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 3252 Invalid, 51 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 51 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:47,868 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 317 states.
[2025-04-28 21:21:47,892 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 317 to 317.
[2025-04-28 21:21:47,893 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 317 states, 38 states have (on average 3.763157894736842) internal successors, (143), 131 states have internal predecessors, (143), 259 states have call successors, (259), 19 states have call predecessors, (259), 19 states have return successors, (259), 168 states have call predecessors, (259), 259 states have call successors, (259)
[2025-04-28 21:21:47,898 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 317 states to 317 states and 661 transitions.
[2025-04-28 21:21:47,899 INFO  L79                 Accepts]: Start accepts. Automaton has 317 states and 661 transitions. Word has length 16
[2025-04-28 21:21:47,899 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,899 INFO  L485      AbstractCegarLoop]: Abstraction has 317 states and 661 transitions.
[2025-04-28 21:21:47,899 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:47,899 INFO  L278                IsEmpty]: Start isEmpty. Operand 317 states and 661 transitions.
[2025-04-28 21:21:47,903 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:47,904 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,904 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,904 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:47,904 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,905 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,905 INFO  L85        PathProgramCache]: Analyzing trace with hash 681346666, now seen corresponding path program 1 times
[2025-04-28 21:21:47,905 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,905 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1535218689]
[2025-04-28 21:21:47,905 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,905 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,946 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:47,967 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:47,967 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,967 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,804 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:48,804 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,804 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1535218689]
[2025-04-28 21:21:48,805 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1535218689] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,805 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,805 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:48,805 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2025039449]
[2025-04-28 21:21:48,805 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,805 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:48,805 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,806 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:48,806 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:48,806 INFO  L87              Difference]: Start difference. First operand 317 states and 661 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:49,174 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,175 INFO  L93              Difference]: Finished difference Result 321 states and 664 transitions.
[2025-04-28 21:21:49,176 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:49,177 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:49,177 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,181 INFO  L225             Difference]: With dead ends: 321
[2025-04-28 21:21:49,182 INFO  L226             Difference]: Without dead ends: 317
[2025-04-28 21:21:49,182 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:49,183 INFO  L437           NwaCegarLoop]: 659 mSDtfsCounter, 3 mSDsluCounter, 2589 mSDsCounter, 0 mSdLazyCounter, 50 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 3248 SdHoareTripleChecker+Invalid, 50 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 50 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,183 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 3248 Invalid, 50 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 50 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:49,184 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 317 states.
[2025-04-28 21:21:49,206 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 317 to 317.
[2025-04-28 21:21:49,207 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 317 states, 38 states have (on average 3.736842105263158) internal successors, (142), 131 states have internal predecessors, (142), 259 states have call successors, (259), 19 states have call predecessors, (259), 19 states have return successors, (259), 168 states have call predecessors, (259), 259 states have call successors, (259)
[2025-04-28 21:21:49,211 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 317 states to 317 states and 660 transitions.
[2025-04-28 21:21:49,212 INFO  L79                 Accepts]: Start accepts. Automaton has 317 states and 660 transitions. Word has length 16
[2025-04-28 21:21:49,212 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,212 INFO  L485      AbstractCegarLoop]: Abstraction has 317 states and 660 transitions.
[2025-04-28 21:21:49,212 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:49,212 INFO  L278                IsEmpty]: Start isEmpty. Operand 317 states and 660 transitions.
[2025-04-28 21:21:49,216 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:49,216 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,216 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,216 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:49,216 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,217 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,217 INFO  L85        PathProgramCache]: Analyzing trace with hash -832306553, now seen corresponding path program 1 times
[2025-04-28 21:21:49,217 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,217 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [427580175]
[2025-04-28 21:21:49,217 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,217 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,258 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:49,278 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:49,278 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,278 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,094 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:50,094 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,094 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [427580175]
[2025-04-28 21:21:50,094 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [427580175] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,094 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,095 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:50,095 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [22833272]
[2025-04-28 21:21:50,095 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,095 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:50,095 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,095 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:50,096 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:50,096 INFO  L87              Difference]: Start difference. First operand 317 states and 660 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:50,538 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,539 INFO  L93              Difference]: Finished difference Result 321 states and 663 transitions.
[2025-04-28 21:21:50,540 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:50,541 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:50,542 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,548 INFO  L225             Difference]: With dead ends: 321
[2025-04-28 21:21:50,548 INFO  L226             Difference]: Without dead ends: 317
[2025-04-28 21:21:50,548 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:50,549 INFO  L437           NwaCegarLoop]: 658 mSDtfsCounter, 3 mSDsluCounter, 2586 mSDsCounter, 0 mSdLazyCounter, 49 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 3244 SdHoareTripleChecker+Invalid, 49 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 49 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,550 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 3244 Invalid, 49 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 49 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:50,551 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 317 states.
[2025-04-28 21:21:50,579 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 317 to 317.
[2025-04-28 21:21:50,580 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 317 states, 38 states have (on average 3.710526315789474) internal successors, (141), 131 states have internal predecessors, (141), 259 states have call successors, (259), 19 states have call predecessors, (259), 19 states have return successors, (259), 168 states have call predecessors, (259), 259 states have call successors, (259)
[2025-04-28 21:21:50,585 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 317 states to 317 states and 659 transitions.
[2025-04-28 21:21:50,585 INFO  L79                 Accepts]: Start accepts. Automaton has 317 states and 659 transitions. Word has length 16
[2025-04-28 21:21:50,585 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,585 INFO  L485      AbstractCegarLoop]: Abstraction has 317 states and 659 transitions.
[2025-04-28 21:21:50,585 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:50,586 INFO  L278                IsEmpty]: Start isEmpty. Operand 317 states and 659 transitions.
[2025-04-28 21:21:50,590 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:50,590 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,590 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,590 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:50,590 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,591 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,591 INFO  L85        PathProgramCache]: Analyzing trace with hash 1301012188, now seen corresponding path program 1 times
[2025-04-28 21:21:50,591 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,591 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [915167657]
[2025-04-28 21:21:50,591 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,591 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,635 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:50,657 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:50,657 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,658 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,564 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:51,564 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,564 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [915167657]
[2025-04-28 21:21:51,564 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [915167657] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,564 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,564 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:51,564 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1931005182]
[2025-04-28 21:21:51,564 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,565 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:51,565 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,565 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:51,565 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:51,565 INFO  L87              Difference]: Start difference. First operand 317 states and 659 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
