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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:53,447 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:53,524 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_aa7a68c1-a475-4c21-a578-552e0b486e0b/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:53,531 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:53,532 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:53,567 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:53,568 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:53,569 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:53,570 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:53,570 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:53,571 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:53,571 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:53,571 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:53,571 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:53,571 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:53,572 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:53,573 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:53,573 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:53,573 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:53,573 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:53,574 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:53,574 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:53,574 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:53,574 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:53,574 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:53,575 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:53,575 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:53,891 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:53,901 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:53,906 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:53,909 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:53,909 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:53,910 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_aa7a68c1-a475-4c21-a578-552e0b486e0b/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-115.smt2
[2025-04-28 21:21:53,912 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:53,918 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:54,200 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_aa7a68c1-a475-4c21-a578-552e0b486e0b/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-115.smt2
[2025-04-28 21:21:54,207 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:54,209 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:54,209 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:54,209 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:54,210 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:54,214 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,242 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54 Unit
[2025-04-28 21:21:54,243 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:54,244 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:54,244 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:54,244 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:54,259 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,259 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,279 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,280 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,284 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,285 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,289 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,290 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,291 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,314 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:54,316 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:54,316 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:54,317 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:54,317 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,320 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:54,331 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,344 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:54,349 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:54,358 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:54,358 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:54,359 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:54,359 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:54,359 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:54,359 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:54,359 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Inv given in one single declaration
[2025-04-28 21:21:54,360 INFO  L130     BoogieDeclarations]: Found specification of procedure Inv
[2025-04-28 21:21:54,360 INFO  L138     BoogieDeclarations]: Found implementation of procedure Inv
[2025-04-28 21:21:54,360 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:54,360 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:54,360 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:54,402 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:54,405 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:54,753 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:54,755 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:54,770 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:54,771 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:54,772 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:54 BoogieIcfgContainer
[2025-04-28 21:21:54,773 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:54,775 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:54,776 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:54,781 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:54,781 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:54" (1/3) ...
[2025-04-28 21:21:54,782 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@733aed60 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:54, skipping insertion in model container
[2025-04-28 21:21:54,782 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (2/3) ...
[2025-04-28 21:21:54,782 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@733aed60 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:54, skipping insertion in model container
[2025-04-28 21:21:54,782 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:54" (3/3) ...
[2025-04-28 21:21:54,784 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:54,801 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:54,805 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 54 locations, 165 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:54,857 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:54,869 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;@6717bf5f, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:54,870 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:54,873 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 54 states, 8 states have (on average 4.5) internal successors, (36), 36 states have internal predecessors, (36), 43 states have call successors, (43), 3 states have call predecessors, (43), 3 states have return successors, (43), 16 states have call predecessors, (43), 43 states have call successors, (43)
[2025-04-28 21:21:54,897 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-04-28 21:21:54,898 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,898 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-04-28 21:21:54,899 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,903 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,904 INFO  L85        PathProgramCache]: Analyzing trace with hash 261517080, now seen corresponding path program 1 times
[2025-04-28 21:21:54,912 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,912 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [637882671]
[2025-04-28 21:21:54,912 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,913 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,932 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-04-28 21:21:54,934 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-04-28 21:21:54,935 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,935 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,965 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,967 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,967 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [637882671]
[2025-04-28 21:21:54,968 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [637882671] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,968 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,972 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-04-28 21:21:54,974 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [923462411]
[2025-04-28 21:21:54,974 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,978 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-04-28 21:21:54,978 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,013 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-04-28 21:21:55,013 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:55,015 INFO  L87              Difference]: Start difference. First operand  has 54 states, 8 states have (on average 4.5) internal successors, (36), 36 states have internal predecessors, (36), 43 states have call successors, (43), 3 states have call predecessors, (43), 3 states have return successors, (43), 16 states have call predecessors, (43), 43 states have call successors, (43) Second operand  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:55,052 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,056 INFO  L93              Difference]: Finished difference Result 52 states and 119 transitions.
[2025-04-28 21:21:55,059 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-04-28 21:21:55,060 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1) Word has length 5
[2025-04-28 21:21:55,060 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,072 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:55,073 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:55,075 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:55,079 INFO  L437           NwaCegarLoop]: 119 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 119 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,081 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 119 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:55,102 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:55,144 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 52.
[2025-04-28 21:21:55,146 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 6 states have (on average 5.5) internal successors, (33), 33 states have internal predecessors, (33), 43 states have call successors, (43), 3 states have call predecessors, (43), 3 states have return successors, (43), 16 states have call predecessors, (43), 43 states have call successors, (43)
[2025-04-28 21:21:55,157 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 119 transitions.
[2025-04-28 21:21:55,162 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 119 transitions. Word has length 5
[2025-04-28 21:21:55,162 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,162 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 119 transitions.
[2025-04-28 21:21:55,162 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:55,162 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 119 transitions.
[2025-04-28 21:21:55,184 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:55,184 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,184 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,184 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:55,184 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,185 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,185 INFO  L85        PathProgramCache]: Analyzing trace with hash 439808401, now seen corresponding path program 1 times
[2025-04-28 21:21:55,185 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,185 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1775662121]
[2025-04-28 21:21:55,185 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,185 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,196 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:55,210 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:55,211 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,212 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,412 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,412 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,412 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1775662121]
[2025-04-28 21:21:55,412 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1775662121] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,412 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,413 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:55,413 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1194395081]
[2025-04-28 21:21:55,413 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,414 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:55,414 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,414 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:55,414 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:55,415 INFO  L87              Difference]: Start difference. First operand 52 states and 119 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:56,135 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,137 INFO  L93              Difference]: Finished difference Result 77 states and 223 transitions.
[2025-04-28 21:21:56,138 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:56,138 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:56,138 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,149 INFO  L225             Difference]: With dead ends: 77
[2025-04-28 21:21:56,149 INFO  L226             Difference]: Without dead ends: 77
[2025-04-28 21:21:56,149 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:56,150 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 11 mSDsluCounter, 130 mSDsCounter, 0 mSdLazyCounter, 225 mSolverCounterSat, 50 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 245 SdHoareTripleChecker+Invalid, 275 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 50 IncrementalHoareTripleChecker+Valid, 225 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,151 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 245 Invalid, 275 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [50 Valid, 225 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:56,152 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 77 states.
[2025-04-28 21:21:56,216 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 77 to 77.
[2025-04-28 21:21:56,222 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 77 states, 8 states have (on average 5.625) internal successors, (45), 44 states have internal predecessors, (45), 66 states have call successors, (66), 4 states have call predecessors, (66), 4 states have return successors, (112), 29 states have call predecessors, (112), 66 states have call successors, (112)
[2025-04-28 21:21:56,235 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 77 states to 77 states and 223 transitions.
[2025-04-28 21:21:56,235 INFO  L79                 Accepts]: Start accepts. Automaton has 77 states and 223 transitions. Word has length 12
[2025-04-28 21:21:56,240 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,240 INFO  L485      AbstractCegarLoop]: Abstraction has 77 states and 223 transitions.
[2025-04-28 21:21:56,240 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:56,240 INFO  L278                IsEmpty]: Start isEmpty. Operand 77 states and 223 transitions.
[2025-04-28 21:21:56,269 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:56,269 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,269 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,270 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:56,270 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,271 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,276 INFO  L85        PathProgramCache]: Analyzing trace with hash -1171890709, now seen corresponding path program 1 times
[2025-04-28 21:21:56,276 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,276 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [489405541]
[2025-04-28 21:21:56,276 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,277 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,289 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:56,313 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:56,314 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,314 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,403 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:56,403 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,403 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [489405541]
[2025-04-28 21:21:56,403 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [489405541] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,403 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1742227557]
[2025-04-28 21:21:56,403 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,404 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,406 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,409 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:56,422 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,454 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:56,473 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:56,473 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,473 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,475 INFO  L256         TraceCheckSpWp]: Trace formula consists of 69 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,480 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,533 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:56,533 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,757 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:56,757 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1742227557] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,757 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,757 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-04-28 21:21:56,757 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1396108074]
[2025-04-28 21:21:56,758 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,758 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:56,758 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,759 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:56,759 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:56,759 INFO  L87              Difference]: Start difference. First operand 77 states and 223 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:58,342 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,342 INFO  L93              Difference]: Finished difference Result 195 states and 941 transitions.
[2025-04-28 21:21:58,343 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:58,343 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 15
[2025-04-28 21:21:58,343 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,374 INFO  L225             Difference]: With dead ends: 195
[2025-04-28 21:21:58,374 INFO  L226             Difference]: Without dead ends: 195
[2025-04-28 21:21:58,375 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 36 GetRequests, 29 SyntacticMatches, 2 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:58,376 INFO  L437           NwaCegarLoop]: 174 mSDtfsCounter, 38 mSDsluCounter, 317 mSDsCounter, 0 mSdLazyCounter, 696 mSolverCounterSat, 218 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 79 SdHoareTripleChecker+Valid, 491 SdHoareTripleChecker+Invalid, 914 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 218 IncrementalHoareTripleChecker+Valid, 696 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,376 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [79 Valid, 491 Invalid, 914 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [218 Valid, 696 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-04-28 21:21:58,377 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 195 states.
[2025-04-28 21:21:58,495 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 195 to 143.
[2025-04-28 21:21:58,496 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 143 states, 12 states have (on average 7.083333333333333) internal successors, (85), 82 states have internal predecessors, (85), 128 states have call successors, (128), 6 states have call predecessors, (128), 6 states have return successors, (345), 55 states have call predecessors, (345), 128 states have call successors, (345)
[2025-04-28 21:21:58,503 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 143 states to 143 states and 558 transitions.
[2025-04-28 21:21:58,503 INFO  L79                 Accepts]: Start accepts. Automaton has 143 states and 558 transitions. Word has length 15
[2025-04-28 21:21:58,504 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,504 INFO  L485      AbstractCegarLoop]: Abstraction has 143 states and 558 transitions.
[2025-04-28 21:21:58,504 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:58,504 INFO  L278                IsEmpty]: Start isEmpty. Operand 143 states and 558 transitions.
[2025-04-28 21:21:58,523 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:58,523 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,523 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:58,529 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:58,727 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,728 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,728 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,728 INFO  L85        PathProgramCache]: Analyzing trace with hash 1662835682, now seen corresponding path program 1 times
[2025-04-28 21:21:58,728 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,728 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1499159091]
[2025-04-28 21:21:58,729 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,729 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,733 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:58,737 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:58,737 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,737 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,775 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:58,775 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,775 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1499159091]
[2025-04-28 21:21:58,775 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1499159091] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:58,775 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:58,775 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:58,775 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [481528763]
[2025-04-28 21:21:58,775 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,776 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:58,776 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,776 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:58,776 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:58,777 INFO  L87              Difference]: Start difference. First operand 143 states and 558 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:59,209 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,209 INFO  L93              Difference]: Finished difference Result 245 states and 1331 transitions.
[2025-04-28 21:21:59,210 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:59,210 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:59,210 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,243 INFO  L225             Difference]: With dead ends: 245
[2025-04-28 21:21:59,243 INFO  L226             Difference]: Without dead ends: 245
[2025-04-28 21:21:59,243 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:59,244 INFO  L437           NwaCegarLoop]: 159 mSDtfsCounter, 11 mSDsluCounter, 164 mSDsCounter, 0 mSdLazyCounter, 244 mSolverCounterSat, 48 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 38 SdHoareTripleChecker+Valid, 323 SdHoareTripleChecker+Invalid, 292 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 48 IncrementalHoareTripleChecker+Valid, 244 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,245 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [38 Valid, 323 Invalid, 292 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [48 Valid, 244 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:59,246 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 245 states.
[2025-04-28 21:21:59,419 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 245 to 243.
[2025-04-28 21:21:59,420 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 243 states, 20 states have (on average 7.95) internal successors, (159), 126 states have internal predecessors, (159), 220 states have call successors, (220), 10 states have call predecessors, (220), 10 states have return successors, (950), 107 states have call predecessors, (950), 220 states have call successors, (950)
[2025-04-28 21:21:59,439 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 243 states to 243 states and 1329 transitions.
[2025-04-28 21:21:59,439 INFO  L79                 Accepts]: Start accepts. Automaton has 243 states and 1329 transitions. Word has length 16
[2025-04-28 21:21:59,439 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,439 INFO  L485      AbstractCegarLoop]: Abstraction has 243 states and 1329 transitions.
[2025-04-28 21:21:59,440 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:59,440 INFO  L278                IsEmpty]: Start isEmpty. Operand 243 states and 1329 transitions.
[2025-04-28 21:21:59,468 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:59,468 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,468 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:59,469 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:59,469 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,471 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,471 INFO  L85        PathProgramCache]: Analyzing trace with hash -383387905, now seen corresponding path program 1 times
[2025-04-28 21:21:59,471 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,471 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [720701553]
[2025-04-28 21:21:59,471 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,471 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,479 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:59,487 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:59,487 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,487 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,557 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:59,557 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,557 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [720701553]
[2025-04-28 21:21:59,557 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [720701553] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,557 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:59,557 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:59,557 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1408958816]
[2025-04-28 21:21:59,557 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,558 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:59,558 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,558 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:59,558 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:59,559 INFO  L87              Difference]: Start difference. First operand 243 states and 1329 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:59,977 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,978 INFO  L93              Difference]: Finished difference Result 297 states and 2041 transitions.
[2025-04-28 21:21:59,979 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:59,979 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:21:59,979 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,028 INFO  L225             Difference]: With dead ends: 297
[2025-04-28 21:22:00,029 INFO  L226             Difference]: Without dead ends: 297
[2025-04-28 21:22:00,029 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:22:00,031 INFO  L437           NwaCegarLoop]: 157 mSDtfsCounter, 11 mSDsluCounter, 174 mSDsCounter, 0 mSdLazyCounter, 247 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 331 SdHoareTripleChecker+Invalid, 281 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 247 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,032 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 331 Invalid, 281 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 247 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:00,033 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 297 states.
[2025-04-28 21:22:00,243 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 297 to 293.
[2025-04-28 21:22:00,245 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 293 states, 24 states have (on average 7.625) internal successors, (183), 148 states have internal predecessors, (183), 266 states have call successors, (266), 12 states have call predecessors, (266), 12 states have return successors, (1335), 133 states have call predecessors, (1335), 266 states have call successors, (1335)
[2025-04-28 21:22:00,267 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 293 states to 293 states and 1784 transitions.
[2025-04-28 21:22:00,267 INFO  L79                 Accepts]: Start accepts. Automaton has 293 states and 1784 transitions. Word has length 16
[2025-04-28 21:22:00,267 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,267 INFO  L485      AbstractCegarLoop]: Abstraction has 293 states and 1784 transitions.
[2025-04-28 21:22:00,267 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:22:00,268 INFO  L278                IsEmpty]: Start isEmpty. Operand 293 states and 1784 transitions.
[2025-04-28 21:22:00,298 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:22:00,298 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,298 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,298 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:22:00,298 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,299 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,299 INFO  L85        PathProgramCache]: Analyzing trace with hash 153743642, now seen corresponding path program 1 times
[2025-04-28 21:22:00,299 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,299 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [175725312]
[2025-04-28 21:22:00,299 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,299 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,303 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:22:00,307 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:22:00,307 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,307 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,349 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:00,349 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,349 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [175725312]
[2025-04-28 21:22:00,349 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [175725312] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:00,349 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:00,349 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:00,350 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1387742338]
[2025-04-28 21:22:00,350 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,350 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:00,350 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,350 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:00,350 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:00,350 INFO  L87              Difference]: Start difference. First operand 293 states and 1784 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:00,820 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,821 INFO  L93              Difference]: Finished difference Result 393 states and 2879 transitions.
[2025-04-28 21:22:00,821 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:00,821 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:22:00,822 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,879 INFO  L225             Difference]: With dead ends: 393
[2025-04-28 21:22:00,881 INFO  L226             Difference]: Without dead ends: 393
[2025-04-28 21:22:00,882 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:22:00,882 INFO  L437           NwaCegarLoop]: 156 mSDtfsCounter, 11 mSDsluCounter, 177 mSDsCounter, 0 mSdLazyCounter, 227 mSolverCounterSat, 47 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 30 SdHoareTripleChecker+Valid, 333 SdHoareTripleChecker+Invalid, 274 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 47 IncrementalHoareTripleChecker+Valid, 227 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,883 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [30 Valid, 333 Invalid, 274 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [47 Valid, 227 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:00,884 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 393 states.
[2025-04-28 21:22:01,230 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 393 to 393.
[2025-04-28 21:22:01,233 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 393 states, 32 states have (on average 7.46875) internal successors, (239), 192 states have internal predecessors, (239), 358 states have call successors, (358), 16 states have call predecessors, (358), 16 states have return successors, (2282), 185 states have call predecessors, (2282), 358 states have call successors, (2282)
[2025-04-28 21:22:01,278 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 393 states to 393 states and 2879 transitions.
[2025-04-28 21:22:01,278 INFO  L79                 Accepts]: Start accepts. Automaton has 393 states and 2879 transitions. Word has length 16
[2025-04-28 21:22:01,278 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,278 INFO  L485      AbstractCegarLoop]: Abstraction has 393 states and 2879 transitions.
[2025-04-28 21:22:01,278 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:01,279 INFO  L278                IsEmpty]: Start isEmpty. Operand 393 states and 2879 transitions.
[2025-04-28 21:22:01,320 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:22:01,320 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,320 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,320 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:22:01,321 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,321 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,321 INFO  L85        PathProgramCache]: Analyzing trace with hash 796855091, now seen corresponding path program 1 times
[2025-04-28 21:22:01,321 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,322 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [132024957]
[2025-04-28 21:22:01,322 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,322 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,328 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:22:01,332 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:22:01,333 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,333 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,390 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:01,391 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,391 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [132024957]
[2025-04-28 21:22:01,391 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [132024957] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:01,391 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:01,391 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:01,391 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [910529211]
[2025-04-28 21:22:01,391 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,391 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:01,391 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,392 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:01,392 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:01,392 INFO  L87              Difference]: Start difference. First operand 393 states and 2879 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:01,885 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,886 INFO  L93              Difference]: Finished difference Result 493 states and 4248 transitions.
[2025-04-28 21:22:01,886 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:01,886 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:22:01,886 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,989 INFO  L225             Difference]: With dead ends: 493
[2025-04-28 21:22:01,989 INFO  L226             Difference]: Without dead ends: 493
[2025-04-28 21:22:01,989 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:22:01,990 INFO  L437           NwaCegarLoop]: 154 mSDtfsCounter, 11 mSDsluCounter, 164 mSDsCounter, 0 mSdLazyCounter, 232 mSolverCounterSat, 47 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 318 SdHoareTripleChecker+Invalid, 279 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 47 IncrementalHoareTripleChecker+Valid, 232 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,990 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 318 Invalid, 279 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [47 Valid, 232 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:01,992 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 493 states.
[2025-04-28 21:22:02,407 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 493 to 493.
[2025-04-28 21:22:02,411 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 493 states, 40 states have (on average 7.625) internal successors, (305), 236 states have internal predecessors, (305), 450 states have call successors, (450), 20 states have call predecessors, (450), 20 states have return successors, (3493), 237 states have call predecessors, (3493), 450 states have call successors, (3493)
[2025-04-28 21:22:02,472 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 493 states to 493 states and 4248 transitions.
[2025-04-28 21:22:02,472 INFO  L79                 Accepts]: Start accepts. Automaton has 493 states and 4248 transitions. Word has length 16
[2025-04-28 21:22:02,473 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:02,473 INFO  L485      AbstractCegarLoop]: Abstraction has 493 states and 4248 transitions.
[2025-04-28 21:22:02,473 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:02,473 INFO  L278                IsEmpty]: Start isEmpty. Operand 493 states and 4248 transitions.
[2025-04-28 21:22:02,521 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:22:02,521 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:02,521 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:02,521 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:22:02,522 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,523 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,523 INFO  L85        PathProgramCache]: Analyzing trace with hash 1075821200, now seen corresponding path program 1 times
[2025-04-28 21:22:02,523 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,523 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [755242855]
[2025-04-28 21:22:02,524 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:02,524 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,529 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:22:02,532 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:22:02,535 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,535 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,587 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:02,587 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,588 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [755242855]
[2025-04-28 21:22:02,588 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [755242855] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:02,588 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:02,588 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:02,589 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [121498964]
[2025-04-28 21:22:02,589 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:02,589 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:02,589 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:02,589 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:02,590 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:02,590 INFO  L87              Difference]: Start difference. First operand 493 states and 4248 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:03,113 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,113 INFO  L93              Difference]: Finished difference Result 593 states and 5887 transitions.
[2025-04-28 21:22:03,114 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:03,114 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:22:03,114 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,251 INFO  L225             Difference]: With dead ends: 593
[2025-04-28 21:22:03,251 INFO  L226             Difference]: Without dead ends: 593
[2025-04-28 21:22:03,251 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:22:03,252 INFO  L437           NwaCegarLoop]: 150 mSDtfsCounter, 11 mSDsluCounter, 154 mSDsCounter, 0 mSdLazyCounter, 233 mSolverCounterSat, 47 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 39 SdHoareTripleChecker+Valid, 304 SdHoareTripleChecker+Invalid, 280 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 47 IncrementalHoareTripleChecker+Valid, 233 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,252 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [39 Valid, 304 Invalid, 280 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [47 Valid, 233 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:03,253 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 593 states.
[2025-04-28 21:22:03,877 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 593 to 593.
[2025-04-28 21:22:03,882 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 593 states, 48 states have (on average 7.854166666666667) internal successors, (377), 280 states have internal predecessors, (377), 542 states have call successors, (542), 24 states have call predecessors, (542), 24 states have return successors, (4968), 289 states have call predecessors, (4968), 542 states have call successors, (4968)
[2025-04-28 21:22:03,971 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 593 states to 593 states and 5887 transitions.
[2025-04-28 21:22:03,971 INFO  L79                 Accepts]: Start accepts. Automaton has 593 states and 5887 transitions. Word has length 16
[2025-04-28 21:22:03,971 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,971 INFO  L485      AbstractCegarLoop]: Abstraction has 593 states and 5887 transitions.
[2025-04-28 21:22:03,972 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:03,972 INFO  L278                IsEmpty]: Start isEmpty. Operand 593 states and 5887 transitions.
[2025-04-28 21:22:04,008 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:22:04,008 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,009 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:04,009 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:22:04,009 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,009 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,009 INFO  L85        PathProgramCache]: Analyzing trace with hash -1584648638, now seen corresponding path program 1 times
[2025-04-28 21:22:04,009 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,010 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1652812811]
[2025-04-28 21:22:04,010 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:04,010 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,012 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:22:04,014 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:22:04,015 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,015 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,053 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:04,054 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,054 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1652812811]
[2025-04-28 21:22:04,054 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1652812811] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:04,054 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:04,054 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:04,054 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1401852408]
[2025-04-28 21:22:04,054 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:04,054 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:04,054 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:04,055 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:04,055 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:04,055 INFO  L87              Difference]: Start difference. First operand 593 states and 5887 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:04,619 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,620 INFO  L93              Difference]: Finished difference Result 695 states and 7448 transitions.
[2025-04-28 21:22:04,620 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:04,620 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:22:04,620 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,793 INFO  L225             Difference]: With dead ends: 695
[2025-04-28 21:22:04,793 INFO  L226             Difference]: Without dead ends: 695
[2025-04-28 21:22:04,794 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:22:04,794 INFO  L437           NwaCegarLoop]: 117 mSDtfsCounter, 11 mSDsluCounter, 135 mSDsCounter, 0 mSdLazyCounter, 236 mSolverCounterSat, 48 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 252 SdHoareTripleChecker+Invalid, 284 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 48 IncrementalHoareTripleChecker+Valid, 236 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,795 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 252 Invalid, 284 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [48 Valid, 236 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:04,796 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 695 states.
[2025-04-28 21:22:05,564 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 695 to 693.
[2025-04-28 21:22:05,571 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 693 states, 56 states have (on average 7.625) internal successors, (427), 324 states have internal predecessors, (427), 634 states have call successors, (634), 28 states have call predecessors, (634), 28 states have return successors, (6385), 341 states have call predecessors, (6385), 634 states have call successors, (6385)
[2025-04-28 21:22:05,691 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 693 states to 693 states and 7446 transitions.
[2025-04-28 21:22:05,691 INFO  L79                 Accepts]: Start accepts. Automaton has 693 states and 7446 transitions. Word has length 16
[2025-04-28 21:22:05,691 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:05,691 INFO  L485      AbstractCegarLoop]: Abstraction has 693 states and 7446 transitions.
[2025-04-28 21:22:05,691 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:05,692 INFO  L278                IsEmpty]: Start isEmpty. Operand 693 states and 7446 transitions.
[2025-04-28 21:22:05,729 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:22:05,729 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:05,729 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:05,730 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:22:05,731 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:05,731 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:05,731 INFO  L85        PathProgramCache]: Analyzing trace with hash 461574949, now seen corresponding path program 1 times
[2025-04-28 21:22:05,731 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:05,731 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2020685430]
[2025-04-28 21:22:05,732 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:05,732 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:05,739 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:22:05,741 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:22:05,745 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:05,745 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:05,793 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:05,793 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:05,794 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2020685430]
[2025-04-28 21:22:05,794 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2020685430] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:05,794 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:05,794 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:05,794 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1581865585]
[2025-04-28 21:22:05,794 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,794 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:05,794 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,795 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:05,796 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:05,796 INFO  L87              Difference]: Start difference. First operand 693 states and 7446 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:22:06,344 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,344 INFO  L93              Difference]: Finished difference Result 705 states and 8833 transitions.
[2025-04-28 21:22:06,344 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:06,345 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:22:06,345 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,584 INFO  L225             Difference]: With dead ends: 705
[2025-04-28 21:22:06,584 INFO  L226             Difference]: Without dead ends: 705
[2025-04-28 21:22:06,584 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:22:06,585 INFO  L437           NwaCegarLoop]: 167 mSDtfsCounter, 11 mSDsluCounter, 184 mSDsCounter, 0 mSdLazyCounter, 241 mSolverCounterSat, 40 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 32 SdHoareTripleChecker+Valid, 351 SdHoareTripleChecker+Invalid, 281 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 40 IncrementalHoareTripleChecker+Valid, 241 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,585 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [32 Valid, 351 Invalid, 281 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [40 Valid, 241 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:06,586 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 705 states.
[2025-04-28 21:22:07,413 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 705 to 693.
[2025-04-28 21:22:07,419 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 693 states, 56 states have (on average 7.625) internal successors, (427), 324 states have internal predecessors, (427), 634 states have call successors, (634), 28 states have call predecessors, (634), 28 states have return successors, (6373), 341 states have call predecessors, (6373), 634 states have call successors, (6373)
[2025-04-28 21:22:07,537 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 693 states to 693 states and 7434 transitions.
[2025-04-28 21:22:07,537 INFO  L79                 Accepts]: Start accepts. Automaton has 693 states and 7434 transitions. Word has length 16
[2025-04-28 21:22:07,537 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,537 INFO  L485      AbstractCegarLoop]: Abstraction has 693 states and 7434 transitions.
[2025-04-28 21:22:07,537 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:22:07,538 INFO  L278                IsEmpty]: Start isEmpty. Operand 693 states and 7434 transitions.
[2025-04-28 21:22:07,653 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:22:07,653 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,654 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:07,654 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:22:07,654 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,654 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,655 INFO  L85        PathProgramCache]: Analyzing trace with hash -1535449708, now seen corresponding path program 1 times
[2025-04-28 21:22:07,655 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,655 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [847882963]
[2025-04-28 21:22:07,655 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,655 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,659 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:22:07,661 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:22:07,661 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,661 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,698 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:07,698 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,698 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [847882963]
[2025-04-28 21:22:07,698 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [847882963] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,698 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [285517038]
[2025-04-28 21:22:07,699 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,699 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,701 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:07,703 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:22:07,706 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,742 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:22:07,759 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:22:07,759 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,759 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,763 INFO  L256         TraceCheckSpWp]: Trace formula consists of 99 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,764 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:07,791 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:07,791 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:08,009 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:08,009 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [285517038] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,010 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,010 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-04-28 21:22:08,010 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1757686665]
[2025-04-28 21:22:08,010 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,010 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:08,010 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,011 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:08,011 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:08,011 INFO  L87              Difference]: Start difference. First operand 693 states and 7434 transitions. Second operand  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:10,596 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:10,596 INFO  L93              Difference]: Finished difference Result 757 states and 9687 transitions.
[2025-04-28 21:22:10,597 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:10,597 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6) Word has length 19
[2025-04-28 21:22:10,597 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:10,753 INFO  L225             Difference]: With dead ends: 757
[2025-04-28 21:22:10,753 INFO  L226             Difference]: Without dead ends: 757
[2025-04-28 21:22:10,754 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 48 GetRequests, 37 SyntacticMatches, 2 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=36, Invalid=74, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:22:10,754 INFO  L437           NwaCegarLoop]: 212 mSDtfsCounter, 42 mSDsluCounter, 223 mSDsCounter, 0 mSdLazyCounter, 1142 mSolverCounterSat, 287 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 155 SdHoareTripleChecker+Valid, 435 SdHoareTripleChecker+Invalid, 1429 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 287 IncrementalHoareTripleChecker+Valid, 1142 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:10,754 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [155 Valid, 435 Invalid, 1429 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [287 Valid, 1142 Invalid, 0 Unknown, 0 Unchecked, 2.3s Time]
[2025-04-28 21:22:10,756 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 757 states.
[2025-04-28 21:22:11,522 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 757 to 731.
[2025-04-28 21:22:11,527 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 731 states, 75 states have (on average 5.946666666666666) internal successors, (446), 343 states have internal predecessors, (446), 634 states have call successors, (634), 28 states have call predecessors, (634), 47 states have return successors, (5862), 360 states have call predecessors, (5862), 634 states have call successors, (5862)
[2025-04-28 21:22:11,633 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 731 states to 731 states and 6942 transitions.
[2025-04-28 21:22:11,633 INFO  L79                 Accepts]: Start accepts. Automaton has 731 states and 6942 transitions. Word has length 19
[2025-04-28 21:22:11,633 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:11,633 INFO  L485      AbstractCegarLoop]: Abstraction has 731 states and 6942 transitions.
[2025-04-28 21:22:11,634 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:11,634 INFO  L278                IsEmpty]: Start isEmpty. Operand 731 states and 6942 transitions.
[2025-04-28 21:22:11,675 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:22:11,675 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:11,675 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:11,680 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:22:11,879 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:11,879 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:11,882 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:11,883 INFO  L85        PathProgramCache]: Analyzing trace with hash -592731759, now seen corresponding path program 1 times
[2025-04-28 21:22:11,883 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:11,883 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [802840574]
[2025-04-28 21:22:11,883 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:11,883 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:11,889 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:22:11,892 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:22:11,896 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:11,896 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:11,949 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:11,949 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:11,949 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [802840574]
[2025-04-28 21:22:11,949 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [802840574] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:11,949 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:11,949 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:11,950 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1314800355]
[2025-04-28 21:22:11,950 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:11,950 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:11,950 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:11,950 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:11,951 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:11,951 INFO  L87              Difference]: Start difference. First operand 731 states and 6942 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:22:12,580 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,580 INFO  L93              Difference]: Finished difference Result 783 states and 12016 transitions.
[2025-04-28 21:22:12,580 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:12,581 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5) Word has length 20
[2025-04-28 21:22:12,581 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,892 INFO  L225             Difference]: With dead ends: 783
[2025-04-28 21:22:12,893 INFO  L226             Difference]: Without dead ends: 783
[2025-04-28 21:22:12,893 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:12,893 INFO  L437           NwaCegarLoop]: 183 mSDtfsCounter, 11 mSDsluCounter, 230 mSDsCounter, 0 mSdLazyCounter, 252 mSolverCounterSat, 39 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 31 SdHoareTripleChecker+Valid, 413 SdHoareTripleChecker+Invalid, 291 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 39 IncrementalHoareTripleChecker+Valid, 252 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,893 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [31 Valid, 413 Invalid, 291 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [39 Valid, 252 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:12,895 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 783 states.
[2025-04-28 21:22:13,625 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 783 to 731.
[2025-04-28 21:22:13,630 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 731 states, 75 states have (on average 5.946666666666666) internal successors, (446), 343 states have internal predecessors, (446), 634 states have call successors, (634), 28 states have call predecessors, (634), 47 states have return successors, (5817), 360 states have call predecessors, (5817), 634 states have call successors, (5817)
[2025-04-28 21:22:13,711 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 731 states to 731 states and 6897 transitions.
[2025-04-28 21:22:13,712 INFO  L79                 Accepts]: Start accepts. Automaton has 731 states and 6897 transitions. Word has length 20
[2025-04-28 21:22:13,712 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,712 INFO  L485      AbstractCegarLoop]: Abstraction has 731 states and 6897 transitions.
[2025-04-28 21:22:13,712 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:22:13,712 INFO  L278                IsEmpty]: Start isEmpty. Operand 731 states and 6897 transitions.
[2025-04-28 21:22:13,749 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:22:13,749 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,749 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:13,749 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:22:13,749 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,750 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,750 INFO  L85        PathProgramCache]: Analyzing trace with hash 2104148321, now seen corresponding path program 1 times
[2025-04-28 21:22:13,750 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,750 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [152391629]
[2025-04-28 21:22:13,750 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,750 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,754 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:22:13,756 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:22:13,756 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,756 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,785 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:13,786 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,786 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [152391629]
[2025-04-28 21:22:13,786 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [152391629] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:13,786 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:13,786 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:13,786 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1723630535]
[2025-04-28 21:22:13,786 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:13,786 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:13,786 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:13,787 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:13,787 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:13,787 INFO  L87              Difference]: Start difference. First operand 731 states and 6897 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:22:14,526 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:14,526 INFO  L93              Difference]: Finished difference Result 847 states and 9165 transitions.
[2025-04-28 21:22:14,526 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:14,530 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:22:14,530 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:14,792 INFO  L225             Difference]: With dead ends: 847
[2025-04-28 21:22:14,793 INFO  L226             Difference]: Without dead ends: 847
[2025-04-28 21:22:14,793 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:14,794 INFO  L437           NwaCegarLoop]: 132 mSDtfsCounter, 12 mSDsluCounter, 137 mSDsCounter, 0 mSdLazyCounter, 389 mSolverCounterSat, 52 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 27 SdHoareTripleChecker+Valid, 269 SdHoareTripleChecker+Invalid, 441 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 52 IncrementalHoareTripleChecker+Valid, 389 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:14,795 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [27 Valid, 269 Invalid, 441 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [52 Valid, 389 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:22:14,797 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 847 states.
[2025-04-28 21:22:15,518 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 847 to 839.
[2025-04-28 21:22:15,530 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 839 states, 87 states have (on average 5.402298850574713) internal successors, (470), 391 states have internal predecessors, (470), 726 states have call successors, (726), 32 states have call predecessors, (726), 55 states have return successors, (6989), 416 states have call predecessors, (6989), 726 states have call successors, (6989)
[2025-04-28 21:22:15,664 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 839 states to 839 states and 8185 transitions.
[2025-04-28 21:22:15,664 INFO  L79                 Accepts]: Start accepts. Automaton has 839 states and 8185 transitions. Word has length 20
[2025-04-28 21:22:15,664 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:15,664 INFO  L485      AbstractCegarLoop]: Abstraction has 839 states and 8185 transitions.
[2025-04-28 21:22:15,665 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:22:15,666 INFO  L278                IsEmpty]: Start isEmpty. Operand 839 states and 8185 transitions.
[2025-04-28 21:22:15,719 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:22:15,719 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:15,719 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:15,719 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:22:15,719 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:15,720 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:15,720 INFO  L85        PathProgramCache]: Analyzing trace with hash 760538503, now seen corresponding path program 1 times
[2025-04-28 21:22:15,720 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:15,720 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [822720993]
[2025-04-28 21:22:15,720 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:15,721 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:15,725 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:22:15,731 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:22:15,731 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:15,732 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:15,773 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:15,774 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:15,775 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [822720993]
[2025-04-28 21:22:15,775 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [822720993] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:15,775 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:15,775 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:15,776 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [251713880]
[2025-04-28 21:22:15,776 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:15,776 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:15,776 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:15,776 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:15,776 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:15,777 INFO  L87              Difference]: Start difference. First operand 839 states and 8185 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:22:16,444 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:16,444 INFO  L93              Difference]: Finished difference Result 851 states and 9543 transitions.
[2025-04-28 21:22:16,445 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:16,445 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:22:16,445 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:16,667 INFO  L225             Difference]: With dead ends: 851
[2025-04-28 21:22:16,667 INFO  L226             Difference]: Without dead ends: 851
[2025-04-28 21:22:16,668 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:16,668 INFO  L437           NwaCegarLoop]: 153 mSDtfsCounter, 11 mSDsluCounter, 156 mSDsCounter, 0 mSdLazyCounter, 362 mSolverCounterSat, 47 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 28 SdHoareTripleChecker+Valid, 309 SdHoareTripleChecker+Invalid, 409 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 47 IncrementalHoareTripleChecker+Valid, 362 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:16,668 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [28 Valid, 309 Invalid, 409 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [47 Valid, 362 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:22:16,670 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 851 states.
[2025-04-28 21:22:17,173 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 851 to 839.
[2025-04-28 21:22:17,179 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 839 states, 87 states have (on average 5.402298850574713) internal successors, (470), 391 states have internal predecessors, (470), 726 states have call successors, (726), 32 states have call predecessors, (726), 55 states have return successors, (6953), 416 states have call predecessors, (6953), 726 states have call successors, (6953)
[2025-04-28 21:22:17,299 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 839 states to 839 states and 8149 transitions.
[2025-04-28 21:22:17,299 INFO  L79                 Accepts]: Start accepts. Automaton has 839 states and 8149 transitions. Word has length 20
[2025-04-28 21:22:17,299 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:17,299 INFO  L485      AbstractCegarLoop]: Abstraction has 839 states and 8149 transitions.
[2025-04-28 21:22:17,300 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:22:17,300 INFO  L278                IsEmpty]: Start isEmpty. Operand 839 states and 8149 transitions.
[2025-04-28 21:22:17,366 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:22:17,366 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:17,366 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:17,366 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:22:17,367 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:17,367 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:17,367 INFO  L85        PathProgramCache]: Analyzing trace with hash 341906452, now seen corresponding path program 1 times
[2025-04-28 21:22:17,367 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:17,368 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1144596292]
[2025-04-28 21:22:17,368 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:17,368 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:17,372 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:22:17,374 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:22:17,375 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:17,375 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:17,407 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:17,407 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:17,407 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1144596292]
[2025-04-28 21:22:17,407 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1144596292] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:17,407 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:17,407 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:17,408 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1829790295]
[2025-04-28 21:22:17,408 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:17,408 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:17,408 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:17,408 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:17,409 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:17,409 INFO  L87              Difference]: Start difference. First operand 839 states and 8149 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:22:18,223 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:18,223 INFO  L93              Difference]: Finished difference Result 851 states and 9183 transitions.
[2025-04-28 21:22:18,224 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:18,224 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:22:18,224 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:18,403 INFO  L225             Difference]: With dead ends: 851
[2025-04-28 21:22:18,403 INFO  L226             Difference]: Without dead ends: 851
[2025-04-28 21:22:18,403 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:18,404 INFO  L437           NwaCegarLoop]: 153 mSDtfsCounter, 11 mSDsluCounter, 142 mSDsCounter, 0 mSdLazyCounter, 350 mSolverCounterSat, 62 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 42 SdHoareTripleChecker+Valid, 295 SdHoareTripleChecker+Invalid, 412 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 62 IncrementalHoareTripleChecker+Valid, 350 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:18,404 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [42 Valid, 295 Invalid, 412 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [62 Valid, 350 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:18,406 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 851 states.
[2025-04-28 21:22:19,014 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 851 to 839.
[2025-04-28 21:22:19,020 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 839 states, 87 states have (on average 5.126436781609195) internal successors, (446), 391 states have internal predecessors, (446), 726 states have call successors, (726), 32 states have call predecessors, (726), 55 states have return successors, (6717), 416 states have call predecessors, (6717), 726 states have call successors, (6717)
[2025-04-28 21:22:19,111 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 839 states to 839 states and 7889 transitions.
[2025-04-28 21:22:19,111 INFO  L79                 Accepts]: Start accepts. Automaton has 839 states and 7889 transitions. Word has length 20
[2025-04-28 21:22:19,111 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:19,111 INFO  L485      AbstractCegarLoop]: Abstraction has 839 states and 7889 transitions.
[2025-04-28 21:22:19,112 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:22:19,112 INFO  L278                IsEmpty]: Start isEmpty. Operand 839 states and 7889 transitions.
[2025-04-28 21:22:19,154 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-04-28 21:22:19,154 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:19,154 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:19,154 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:22:19,154 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:19,154 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:19,155 INFO  L85        PathProgramCache]: Analyzing trace with hash -2029766728, now seen corresponding path program 1 times
[2025-04-28 21:22:19,155 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:19,155 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [914579912]
[2025-04-28 21:22:19,155 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:19,155 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:19,159 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:22:19,163 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:22:19,163 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:19,163 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:19,204 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 8 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:19,205 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:19,205 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [914579912]
[2025-04-28 21:22:19,205 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [914579912] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:19,205 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2086328338]
[2025-04-28 21:22:19,205 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:19,205 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:19,208 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:19,210 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:19,215 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:22:19,250 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:22:19,268 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:22:19,269 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:19,269 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:19,270 INFO  L256         TraceCheckSpWp]: Trace formula consists of 131 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:19,271 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:19,292 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 8 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:19,293 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:19,542 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 8 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:19,542 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2086328338] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:19,543 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:19,543 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-04-28 21:22:19,543 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [280062925]
[2025-04-28 21:22:19,543 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:19,543 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:19,543 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:19,544 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:19,544 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:19,544 INFO  L87              Difference]: Start difference. First operand 839 states and 7889 transitions. Second operand  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:22:22,060 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:22,060 INFO  L93              Difference]: Finished difference Result 959 states and 16816 transitions.
[2025-04-28 21:22:22,060 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:22,060 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7) Word has length 23
[2025-04-28 21:22:22,061 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:22,387 INFO  L225             Difference]: With dead ends: 959
[2025-04-28 21:22:22,387 INFO  L226             Difference]: Without dead ends: 959
[2025-04-28 21:22:22,387 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 45 SyntacticMatches, 2 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 19 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=54, Invalid=102, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:22:22,388 INFO  L437           NwaCegarLoop]: 214 mSDtfsCounter, 40 mSDsluCounter, 356 mSDsCounter, 0 mSdLazyCounter, 1314 mSolverCounterSat, 194 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 96 SdHoareTripleChecker+Valid, 570 SdHoareTripleChecker+Invalid, 1508 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 194 IncrementalHoareTripleChecker+Valid, 1314 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:22,388 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [96 Valid, 570 Invalid, 1508 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [194 Valid, 1314 Invalid, 0 Unknown, 0 Unchecked, 2.1s Time]
[2025-04-28 21:22:22,389 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 959 states.
