./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-131.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:52,359 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:52,420 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ae00af4d-6c77-4d28-9af9-baff64e83b32/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:52,424 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:52,424 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:52,466 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:52,467 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:52,467 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:52,468 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:52,468 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:52,468 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:52,468 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:52,468 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:52,468 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:52,470 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:52,470 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:52,470 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:52,471 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:52,471 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:52,471 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:52,471 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:52,471 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:52,471 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:52,471 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:52,471 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:52,472 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:52,472 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:52,789 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:52,800 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:52,802 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:52,805 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:52,805 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:52,806 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ae00af4d-6c77-4d28-9af9-baff64e83b32/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-131.smt2
[2025-04-28 21:21:52,810 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:52,813 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:53,021 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ae00af4d-6c77-4d28-9af9-baff64e83b32/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-131.smt2
[2025-04-28 21:21:53,025 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:53,026 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:53,026 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:53,027 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:53,027 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:53,029 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,051 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53 Unit
[2025-04-28 21:21:53,051 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:53,052 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:53,052 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:53,052 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:53,068 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,068 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,100 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,100 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,102 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,103 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,107 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,108 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,109 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,126 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:53,127 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:53,127 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:53,128 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:53,129 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (1/1) ...
[2025-04-28 21:21:53,131 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:53,148 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,166 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:53,169 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:53,184 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:53,184 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:53,184 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:53,184 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:53,184 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:53,185 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:53,185 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure zip.DLRunknown.CLN7 given in one single declaration
[2025-04-28 21:21:53,185 INFO  L130     BoogieDeclarations]: Found specification of procedure zip.DLRunknown.CLN7
[2025-04-28 21:21:53,185 INFO  L138     BoogieDeclarations]: Found implementation of procedure zip.DLRunknown.CLN7
[2025-04-28 21:21:53,186 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure map.DLRunknown.CLN4 given in one single declaration
[2025-04-28 21:21:53,186 INFO  L130     BoogieDeclarations]: Found specification of procedure map.DLRunknown.CLN4
[2025-04-28 21:21:53,186 INFO  L138     BoogieDeclarations]: Found implementation of procedure map.DLRunknown.CLN4
[2025-04-28 21:21:53,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure zip.DLRunknown.CLN6 given in one single declaration
[2025-04-28 21:21:53,187 INFO  L130     BoogieDeclarations]: Found specification of procedure zip.DLRunknown.CLN6
[2025-04-28 21:21:53,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure zip.DLRunknown.CLN6
[2025-04-28 21:21:53,187 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:53,187 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:53,187 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:53,246 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:53,249 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:53,408 INFO  L?                        ?]: Removed 13 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:53,408 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:53,424 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:53,424 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:53,426 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:53 BoogieIcfgContainer
[2025-04-28 21:21:53,427 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:53,429 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:53,429 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:53,435 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:53,435 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:53" (1/3) ...
[2025-04-28 21:21:53,437 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@390f41bb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:53, skipping insertion in model container
[2025-04-28 21:21:53,437 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:53" (2/3) ...
[2025-04-28 21:21:53,438 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@390f41bb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:53, skipping insertion in model container
[2025-04-28 21:21:53,438 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:53" (3/3) ...
[2025-04-28 21:21:53,439 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:53,458 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:53,460 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 6 procedures, 29 locations, 50 edges, 6 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:53,516 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:53,528 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;@133e263d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:53,528 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:53,532 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 29 states, 11 states have (on average 1.5454545454545454) internal successors, (17), 17 states have internal predecessors, (17), 11 states have call successors, (11), 5 states have call predecessors, (11), 5 states have return successors, (11), 8 states have call predecessors, (11), 11 states have call successors, (11)
[2025-04-28 21:21:53,540 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:53,541 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,542 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,543 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,550 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,550 INFO  L85        PathProgramCache]: Analyzing trace with hash 1653476773, now seen corresponding path program 1 times
[2025-04-28 21:21:53,558 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,559 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [728260924]
[2025-04-28 21:21:53,559 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,560 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,591 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:53,615 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:53,615 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,615 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,848 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:53,850 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,850 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [728260924]
[2025-04-28 21:21:53,851 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [728260924] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,851 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,854 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:53,856 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [690641511]
[2025-04-28 21:21:53,860 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,864 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:53,865 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,899 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:53,900 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:53,902 INFO  L87              Difference]: Start difference. First operand  has 29 states, 11 states have (on average 1.5454545454545454) internal successors, (17), 17 states have internal predecessors, (17), 11 states have call successors, (11), 5 states have call predecessors, (11), 5 states have return successors, (11), 8 states have call predecessors, (11), 11 states have call successors, (11) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:53,984 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,984 INFO  L93              Difference]: Finished difference Result 31 states and 44 transitions.
[2025-04-28 21:21:53,985 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:53,987 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:53,987 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,994 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:53,994 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:53,997 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:54,003 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 1 mSDsluCounter, 58 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 93 SdHoareTripleChecker+Invalid, 20 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,004 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 93 Invalid, 20 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:54,025 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:54,042 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 29.
[2025-04-28 21:21:54,043 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 11 states have (on average 1.4545454545454546) internal successors, (16), 16 states have internal predecessors, (16), 11 states have call successors, (11), 5 states have call predecessors, (11), 6 states have return successors, (15), 8 states have call predecessors, (15), 11 states have call successors, (15)
[2025-04-28 21:21:54,070 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 42 transitions.
[2025-04-28 21:21:54,072 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 42 transitions. Word has length 12
[2025-04-28 21:21:54,072 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,072 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 42 transitions.
[2025-04-28 21:21:54,072 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:54,073 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 42 transitions.
[2025-04-28 21:21:54,074 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:54,074 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,075 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,075 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:54,075 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,076 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,077 INFO  L85        PathProgramCache]: Analyzing trace with hash 1801252930, now seen corresponding path program 1 times
[2025-04-28 21:21:54,077 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,077 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1812288843]
[2025-04-28 21:21:54,077 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,077 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,081 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:54,085 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:54,086 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,086 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,278 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:54,278 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,278 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1812288843]
[2025-04-28 21:21:54,278 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1812288843] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,278 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,278 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:54,279 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1689093386]
[2025-04-28 21:21:54,279 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,280 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:54,280 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,281 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:54,281 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:54,282 INFO  L87              Difference]: Start difference. First operand 29 states and 42 transitions. Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:54,356 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,357 INFO  L93              Difference]: Finished difference Result 31 states and 43 transitions.
[2025-04-28 21:21:54,357 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:54,358 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:54,358 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,359 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:54,359 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:54,359 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:54,360 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 1 mSDsluCounter, 57 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 91 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,361 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 91 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:54,362 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:54,366 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 29.
[2025-04-28 21:21:54,367 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 11 states have (on average 1.4545454545454546) internal successors, (16), 16 states have internal predecessors, (16), 11 states have call successors, (11), 5 states have call predecessors, (11), 6 states have return successors, (14), 8 states have call predecessors, (14), 11 states have call successors, (14)
[2025-04-28 21:21:54,368 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 41 transitions.
[2025-04-28 21:21:54,368 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 41 transitions. Word has length 12
[2025-04-28 21:21:54,368 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,368 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 41 transitions.
[2025-04-28 21:21:54,368 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:54,369 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 41 transitions.
[2025-04-28 21:21:54,370 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:54,370 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,370 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,370 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:54,370 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,371 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,371 INFO  L85        PathProgramCache]: Analyzing trace with hash -1813421820, now seen corresponding path program 1 times
[2025-04-28 21:21:54,371 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,371 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1185292335]
[2025-04-28 21:21:54,371 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,371 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,376 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:54,382 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:54,382 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,382 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,562 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:54,562 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,562 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1185292335]
[2025-04-28 21:21:54,562 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1185292335] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,562 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,562 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:54,563 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1746637319]
[2025-04-28 21:21:54,563 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,563 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:54,563 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,565 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:54,566 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:54,566 INFO  L87              Difference]: Start difference. First operand 29 states and 41 transitions. Second operand  has 5 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:54,660 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,660 INFO  L93              Difference]: Finished difference Result 29 states and 40 transitions.
[2025-04-28 21:21:54,661 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:54,661 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 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:54,662 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,662 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:54,662 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:54,663 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:54,663 INFO  L437           NwaCegarLoop]: 33 mSDtfsCounter, 1 mSDsluCounter, 78 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 111 SdHoareTripleChecker+Invalid, 39 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,664 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 111 Invalid, 39 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:54,664 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:54,668 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 28.
[2025-04-28 21:21:54,668 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 15 states have internal predecessors, (15), 10 states have call successors, (10), 5 states have call predecessors, (10), 6 states have return successors, (13), 8 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:54,669 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 38 transitions.
[2025-04-28 21:21:54,669 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 38 transitions. Word has length 16
[2025-04-28 21:21:54,669 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,669 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 38 transitions.
[2025-04-28 21:21:54,672 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:54,672 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 38 transitions.
[2025-04-28 21:21:54,675 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:54,675 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,675 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,675 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:54,675 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,676 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,676 INFO  L85        PathProgramCache]: Analyzing trace with hash 232801767, now seen corresponding path program 1 times
[2025-04-28 21:21:54,676 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,676 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [438951914]
[2025-04-28 21:21:54,676 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,676 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,686 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:54,694 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:54,694 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,694 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,959 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:54,959 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,959 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [438951914]
[2025-04-28 21:21:54,959 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [438951914] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,959 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,959 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:54,959 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1802308557]
[2025-04-28 21:21:54,960 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,960 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:54,960 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,960 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:54,960 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:54,961 INFO  L87              Difference]: Start difference. First operand 28 states and 38 transitions. Second operand  has 5 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:55,051 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,052 INFO  L93              Difference]: Finished difference Result 28 states and 37 transitions.
[2025-04-28 21:21:55,052 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:55,052 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 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:55,052 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,053 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:55,053 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:55,053 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,055 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 1 mSDsluCounter, 75 mSDsCounter, 0 mSdLazyCounter, 32 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 106 SdHoareTripleChecker+Invalid, 32 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 32 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,057 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 106 Invalid, 32 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 32 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:55,058 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:55,063 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 25.
[2025-04-28 21:21:55,066 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 25 states, 10 states have (on average 1.3) internal successors, (13), 13 states have internal predecessors, (13), 9 states have call successors, (9), 5 states have call predecessors, (9), 5 states have return successors, (9), 8 states have call predecessors, (9), 9 states have call successors, (9)
[2025-04-28 21:21:55,067 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 31 transitions.
[2025-04-28 21:21:55,067 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 31 transitions. Word has length 16
[2025-04-28 21:21:55,067 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,067 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 31 transitions.
[2025-04-28 21:21:55,067 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:55,069 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 31 transitions.
[2025-04-28 21:21:55,069 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:55,070 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,070 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,070 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:55,070 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,071 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,073 INFO  L85        PathProgramCache]: Analyzing trace with hash 1301912590, now seen corresponding path program 1 times
[2025-04-28 21:21:55,073 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,074 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [601263281]
[2025-04-28 21:21:55,074 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,074 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,078 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:55,088 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:55,090 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,090 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,185 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:55,185 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,185 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [601263281]
[2025-04-28 21:21:55,185 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [601263281] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,185 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,185 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:55,185 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1273768170]
[2025-04-28 21:21:55,185 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,186 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:55,186 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,187 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:55,187 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,187 INFO  L87              Difference]: Start difference. First operand 25 states and 31 transitions. Second operand  has 6 states, 4 states have (on average 2.5) internal successors, (10), 5 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:55,256 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,256 INFO  L93              Difference]: Finished difference Result 32 states and 41 transitions.
[2025-04-28 21:21:55,257 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:55,257 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 5 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:55,258 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,258 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:55,258 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:55,259 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:55,260 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 3 mSDsluCounter, 98 mSDsCounter, 0 mSdLazyCounter, 25 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 126 SdHoareTripleChecker+Invalid, 27 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 25 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,260 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 126 Invalid, 27 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 25 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:55,263 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:55,271 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 30.
[2025-04-28 21:21:55,272 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 30 states, 12 states have (on average 1.25) internal successors, (15), 15 states have internal predecessors, (15), 10 states have call successors, (10), 5 states have call predecessors, (10), 7 states have return successors, (14), 10 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:21:55,273 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 39 transitions.
[2025-04-28 21:21:55,273 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 39 transitions. Word has length 20
[2025-04-28 21:21:55,273 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,273 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 39 transitions.
[2025-04-28 21:21:55,273 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 5 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:55,274 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 39 transitions.
[2025-04-28 21:21:55,274 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:55,275 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,275 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]
[2025-04-28 21:21:55,275 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:55,275 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,275 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,278 INFO  L85        PathProgramCache]: Analyzing trace with hash -1330710574, now seen corresponding path program 1 times
[2025-04-28 21:21:55,278 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,278 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [618751437]
[2025-04-28 21:21:55,278 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,278 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,286 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:55,292 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:55,292 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,292 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,389 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,389 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,389 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [618751437]
[2025-04-28 21:21:55,389 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [618751437] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,389 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,390 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:55,390 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1115403447]
[2025-04-28 21:21:55,390 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,390 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:55,390 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,391 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:55,392 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,392 INFO  L87              Difference]: Start difference. First operand 30 states and 39 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 5 states have internal predecessors, (12), 5 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:55,443 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,443 INFO  L93              Difference]: Finished difference Result 32 states and 40 transitions.
[2025-04-28 21:21:55,446 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:55,446 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 5 states have internal predecessors, (12), 5 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 5 states have call successors, (6) Word has length 24
[2025-04-28 21:21:55,446 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,447 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:55,447 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:55,447 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,448 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 2 mSDsluCounter, 86 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 121 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 22 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,448 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 121 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:55,449 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:55,453 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 27.
[2025-04-28 21:21:55,453 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 14 states have internal predecessors, (14), 9 states have call successors, (9), 5 states have call predecessors, (9), 6 states have return successors, (10), 9 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:21:55,454 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 33 transitions.
[2025-04-28 21:21:55,454 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 33 transitions. Word has length 24
[2025-04-28 21:21:55,454 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,454 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 33 transitions.
[2025-04-28 21:21:55,454 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 5 states have internal predecessors, (12), 5 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:55,454 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 33 transitions.
[2025-04-28 21:21:55,455 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:55,455 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,455 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,455 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:55,455 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,456 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,456 INFO  L85        PathProgramCache]: Analyzing trace with hash -1175628520, now seen corresponding path program 1 times
[2025-04-28 21:21:55,456 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,456 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1884970999]
[2025-04-28 21:21:55,456 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,456 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,461 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:55,464 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:55,465 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,465 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,568 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:55,568 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,568 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1884970999]
[2025-04-28 21:21:55,568 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1884970999] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,568 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [535804833]
[2025-04-28 21:21:55,569 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,569 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,572 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,579 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:55,584 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,624 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:55,644 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:55,644 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,644 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,646 INFO  L256         TraceCheckSpWp]: Trace formula consists of 94 conjuncts, 27 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,655 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,873 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:55,874 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,621 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:56,621 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [535804833] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,622 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,622 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 9, 9] total 14
[2025-04-28 21:21:56,622 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [60944998]
[2025-04-28 21:21:56,622 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,622 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:56,623 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,623 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:56,623 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=36, Invalid=146, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:56,624 INFO  L87              Difference]: Start difference. First operand 27 states and 33 transitions. Second operand  has 14 states, 8 states have (on average 2.375) internal successors, (19), 11 states have internal predecessors, (19), 9 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (13), 9 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:56,964 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,964 INFO  L93              Difference]: Finished difference Result 39 states and 61 transitions.
[2025-04-28 21:21:56,965 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:56,965 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 8 states have (on average 2.375) internal successors, (19), 11 states have internal predecessors, (19), 9 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (13), 9 states have call predecessors, (13), 9 states have call successors, (13) Word has length 28
[2025-04-28 21:21:56,966 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,967 INFO  L225             Difference]: With dead ends: 39
[2025-04-28 21:21:56,969 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:56,970 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 69 GetRequests, 50 SyntacticMatches, 0 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 35 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=102, Invalid=318, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:56,970 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 6 mSDsluCounter, 138 mSDsCounter, 0 mSdLazyCounter, 111 mSolverCounterSat, 27 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 161 SdHoareTripleChecker+Invalid, 138 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 27 IncrementalHoareTripleChecker+Valid, 111 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,971 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 161 Invalid, 138 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [27 Valid, 111 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:56,972 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:56,979 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 29.
[2025-04-28 21:21:56,982 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 12 states have (on average 1.25) internal successors, (15), 15 states have internal predecessors, (15), 9 states have call successors, (9), 5 states have call predecessors, (9), 7 states have return successors, (11), 9 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:56,983 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 35 transitions.
[2025-04-28 21:21:56,983 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 35 transitions. Word has length 28
[2025-04-28 21:21:56,983 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,983 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 35 transitions.
[2025-04-28 21:21:56,983 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 8 states have (on average 2.375) internal successors, (19), 11 states have internal predecessors, (19), 9 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (13), 9 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:56,983 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 35 transitions.
[2025-04-28 21:21:56,984 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:56,984 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,984 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,991 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:57,185 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable7
[2025-04-28 21:21:57,185 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,185 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,185 INFO  L85        PathProgramCache]: Analyzing trace with hash 266120412, now seen corresponding path program 1 times
[2025-04-28 21:21:57,186 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,186 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1499783554]
[2025-04-28 21:21:57,186 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,186 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,191 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:57,200 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:57,200 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,200 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,527 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:57,527 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,528 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1499783554]
[2025-04-28 21:21:57,528 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1499783554] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,528 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1506542314]
[2025-04-28 21:21:57,528 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,528 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,531 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,533 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:57,538 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,579 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:57,596 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:57,597 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,597 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,598 INFO  L256         TraceCheckSpWp]: Trace formula consists of 110 conjuncts, 37 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,600 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,861 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:57,862 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,573 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:58,573 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1506542314] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:58,573 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:58,573 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 11, 11] total 21
[2025-04-28 21:21:58,573 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [341427705]
[2025-04-28 21:21:58,574 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,574 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:58,574 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,575 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:58,575 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=51, Invalid=369, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:58,575 INFO  L87              Difference]: Start difference. First operand 29 states and 35 transitions. Second operand  has 21 states, 10 states have (on average 2.5) internal successors, (25), 17 states have internal predecessors, (25), 14 states have call successors, (16), 1 states have call predecessors, (16), 10 states have return successors, (17), 12 states have call predecessors, (17), 14 states have call successors, (17)
[2025-04-28 21:21:59,062 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,063 INFO  L93              Difference]: Finished difference Result 33 states and 47 transitions.
[2025-04-28 21:21:59,063 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:59,063 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 10 states have (on average 2.5) internal successors, (25), 17 states have internal predecessors, (25), 14 states have call successors, (16), 1 states have call predecessors, (16), 10 states have return successors, (17), 12 states have call predecessors, (17), 14 states have call successors, (17) Word has length 32
[2025-04-28 21:21:59,064 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,064 INFO  L225             Difference]: With dead ends: 33
[2025-04-28 21:21:59,064 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:59,065 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 82 GetRequests, 54 SyntacticMatches, 0 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 58 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=119, Invalid=751, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:59,065 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 11 mSDsluCounter, 204 mSDsCounter, 0 mSdLazyCounter, 188 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 226 SdHoareTripleChecker+Invalid, 229 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 188 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,066 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 226 Invalid, 229 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 188 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:59,066 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:59,069 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:59,069 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:21:59,069 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:59,069 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 32
[2025-04-28 21:21:59,070 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,070 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:59,070 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 10 states have (on average 2.5) internal successors, (25), 17 states have internal predecessors, (25), 14 states have call successors, (16), 1 states have call predecessors, (16), 10 states have return successors, (17), 12 states have call predecessors, (17), 14 states have call successors, (17)
[2025-04-28 21:21:59,070 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:59,070 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:59,077 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:59,091 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:59,278 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,282 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,284 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:59,287 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:59 BoogieIcfgContainer
[2025-04-28 21:21:59,288 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:59,288 INFO  L158              Benchmark]: Toolchain (without parser) took 6262.50ms. Allocated memory is still 234.9MB. Free memory was 160.4MB in the beginning and 209.3MB in the end (delta: -48.9MB). Peak memory consumption was 41.5MB. Max. memory is 33.6GB.
[2025-04-28 21:21:59,289 INFO  L158              Benchmark]: SmtParser took 2.20ms. Allocated memory is still 234.9MB. Free memory was 171.4MB in the beginning and 170.8MB in the end (delta: 587.2kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:59,289 INFO  L158              Benchmark]: ChcToBoogie took 25.16ms. Allocated memory is still 234.9MB. Free memory was 160.4MB in the beginning and 159.8MB in the end (delta: 592.7kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:59,289 INFO  L158              Benchmark]: Boogie Preprocessor took 74.39ms. Allocated memory is still 234.9MB. Free memory was 159.8MB in the beginning and 157.4MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:59,289 INFO  L158              Benchmark]: RCFGBuilder took 299.52ms. Allocated memory is still 234.9MB. Free memory was 157.4MB in the beginning and 147.3MB in the end (delta: 10.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:59,290 INFO  L158              Benchmark]: TraceAbstraction took 5858.67ms. Allocated memory is still 234.9MB. Free memory was 146.7MB in the beginning and 209.3MB in the end (delta: -62.6MB). Peak memory consumption was 24.7MB. Max. memory is 33.6GB.
[2025-04-28 21:21:59,291 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 2.20ms. Allocated memory is still 234.9MB. Free memory was 171.4MB in the beginning and 170.8MB in the end (delta: 587.2kB). There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 25.16ms. Allocated memory is still 234.9MB. Free memory was 160.4MB in the beginning and 159.8MB in the end (delta: 592.7kB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 74.39ms. Allocated memory is still 234.9MB. Free memory was 159.8MB in the beginning and 157.4MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 299.52ms. Allocated memory is still 234.9MB. Free memory was 157.4MB in the beginning and 147.3MB in the end (delta: 10.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 5858.67ms. Allocated memory is still 234.9MB. Free memory was 146.7MB in the beginning and 209.3MB in the end (delta: -62.6MB). Peak memory consumption was 24.7MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 6 procedures, 29 locations, 50 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 5.8s, OverallIterations: 8, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.4s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 44 SdHoareTripleChecker+Valid, 0.7s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 26 mSDsluCounter, 1035 SdHoareTripleChecker+Invalid, 0.6s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 794 mSDsCounter, 70 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 454 IncrementalHoareTripleChecker+Invalid, 524 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 70 mSolverCounterUnsat, 241 mSDtfsCounter, 454 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 186 GetRequests, 118 SyntacticMatches, 0 SemanticMatches, 68 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 94 ImplicationChecksByTransitivity, 1.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=30occurred in iteration=5, InterpolantAutomatonStates: 60, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 8 MinimizatonAttempts, 18 StatesRemovedByMinimization, 6 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 3.4s InterpolantComputationTime, 220 NumberOfCodeBlocks, 220 NumberOfCodeBlocksAsserted, 10 NumberOfCheckSat, 268 ConstructedInterpolants, 0 QuantifiedInterpolants, 738 SizeOfPredicates, 16 NumberOfNonLiveVariables, 204 ConjunctsInSsa, 64 ConjunctsInUnsatCore, 12 InterpolantComputations, 6 PerfectInterpolantSequences, 32/54 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:21:59,311 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
sat
