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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:23,305 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:23,382 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b304d392-c8cf-4cb3-bb99-acc2b80a39d5/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:23,387 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:23,387 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:23,426 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:23,428 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:23,428 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:23,429 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:23,430 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:23,430 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:23,431 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:23,431 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:23,431 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:23,431 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:23,431 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:23,433 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:23,433 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:23,433 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:23,433 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:23,433 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:23,433 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:23,433 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:23,434 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:23,434 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:23,434 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:23,435 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:23,815 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:23,827 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:23,831 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:23,834 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:23,834 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:23,837 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b304d392-c8cf-4cb3-bb99-acc2b80a39d5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-114.smt2
[2025-04-28 21:21:23,838 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:23,842 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:24,052 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b304d392-c8cf-4cb3-bb99-acc2b80a39d5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-114.smt2
[2025-04-28 21:21:24,056 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:24,057 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:24,059 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:24,059 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:24,060 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:24,064 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,087 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24 Unit
[2025-04-28 21:21:24,088 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:24,089 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:24,090 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:24,090 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:24,106 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,106 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,136 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,136 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,139 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,140 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,143 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,144 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,144 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,159 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:24,164 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:24,164 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:24,164 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:24,165 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,169 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:24,187 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:24,202 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:24,206 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:24,218 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:24,218 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:24,218 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:24,218 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure SAD given in one single declaration
[2025-04-28 21:21:24,218 INFO  L130     BoogieDeclarations]: Found specification of procedure SAD
[2025-04-28 21:21:24,218 INFO  L138     BoogieDeclarations]: Found implementation of procedure SAD
[2025-04-28 21:21:24,219 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure FUN given in one single declaration
[2025-04-28 21:21:24,219 INFO  L130     BoogieDeclarations]: Found specification of procedure FUN
[2025-04-28 21:21:24,219 INFO  L138     BoogieDeclarations]: Found implementation of procedure FUN
[2025-04-28 21:21:24,219 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:24,219 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:24,219 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:24,279 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:24,282 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:24,392 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:24,392 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:24,411 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:24,411 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:24,412 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:24 BoogieIcfgContainer
[2025-04-28 21:21:24,412 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:24,418 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:24,418 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:24,424 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:24,424 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:24" (1/3) ...
[2025-04-28 21:21:24,425 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@10d8ef79 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:24, skipping insertion in model container
[2025-04-28 21:21:24,425 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (2/3) ...
[2025-04-28 21:21:24,425 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@10d8ef79 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:24, skipping insertion in model container
[2025-04-28 21:21:24,425 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:24" (3/3) ...
[2025-04-28 21:21:24,427 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:24,445 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:24,448 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 18 locations, 26 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:24,498 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:24,524 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;@5c51facd, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:24,526 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:24,530 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 18 states, 8 states have (on average 1.375) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 3 states have return successors, (5), 4 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:24,540 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:24,540 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,541 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:24,541 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,547 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,549 INFO  L85        PathProgramCache]: Analyzing trace with hash -528632176, now seen corresponding path program 1 times
[2025-04-28 21:21:24,557 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,558 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2128365947]
[2025-04-28 21:21:24,558 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,559 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,600 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:24,624 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:24,624 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,626 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,759 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:24,759 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,760 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2128365947]
[2025-04-28 21:21:24,760 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2128365947] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:24,761 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:24,765 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:24,768 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1116524727]
[2025-04-28 21:21:24,769 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:24,775 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:24,778 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:24,813 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:24,814 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:24,816 INFO  L87              Difference]: Start difference. First operand  has 18 states, 8 states have (on average 1.375) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 3 states have return successors, (5), 4 states have call predecessors, (5), 5 states have call successors, (5) Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 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:24,882 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:24,883 INFO  L93              Difference]: Finished difference Result 20 states and 24 transitions.
[2025-04-28 21:21:24,885 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:24,887 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 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 13
[2025-04-28 21:21:24,888 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:24,895 INFO  L225             Difference]: With dead ends: 20
[2025-04-28 21:21:24,896 INFO  L226             Difference]: Without dead ends: 20
[2025-04-28 21:21:24,898 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:24,902 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 1 mSDsluCounter, 29 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 47 SdHoareTripleChecker+Invalid, 7 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:24,903 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 47 Invalid, 7 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:24,919 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 20 states.
[2025-04-28 21:21:24,946 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 20 to 18.
[2025-04-28 21:21:24,947 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 18 states, 8 states have (on average 1.25) internal successors, (10), 10 states have internal predecessors, (10), 5 states have call successors, (5), 3 states have call predecessors, (5), 4 states have return successors, (6), 4 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:24,954 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 18 states to 18 states and 21 transitions.
[2025-04-28 21:21:24,955 INFO  L79                 Accepts]: Start accepts. Automaton has 18 states and 21 transitions. Word has length 13
[2025-04-28 21:21:24,956 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:24,956 INFO  L485      AbstractCegarLoop]: Abstraction has 18 states and 21 transitions.
[2025-04-28 21:21:24,956 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 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:24,956 INFO  L278                IsEmpty]: Start isEmpty. Operand 18 states and 21 transitions.
[2025-04-28 21:21:24,958 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:24,958 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,958 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:24,959 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:24,959 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,960 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,960 INFO  L85        PathProgramCache]: Analyzing trace with hash 1056419826, now seen corresponding path program 1 times
[2025-04-28 21:21:24,960 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,960 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1455835773]
[2025-04-28 21:21:24,960 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,961 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,976 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:24,994 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:24,994 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,994 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,281 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:25,283 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,284 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1455835773]
[2025-04-28 21:21:25,284 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1455835773] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:25,284 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [783411743]
[2025-04-28 21:21:25,284 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,284 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,291 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:25,298 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:25,300 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:25,331 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:25,342 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:25,343 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,343 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,349 INFO  L256         TraceCheckSpWp]: Trace formula consists of 47 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:25,356 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:25,522 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:25,522 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:26,340 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:26,340 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [783411743] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:26,340 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:26,340 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:26,345 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2099846247]
[2025-04-28 21:21:26,345 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,346 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:26,346 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,347 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:26,347 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:26,347 INFO  L87              Difference]: Start difference. First operand 18 states and 21 transitions. Second operand  has 12 states, 5 states have (on average 2.6) internal successors, (13), 11 states have internal predecessors, (13), 8 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 3 states have call predecessors, (8), 8 states have call successors, (8)
[2025-04-28 21:21:26,507 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,507 INFO  L93              Difference]: Finished difference Result 24 states and 29 transitions.
[2025-04-28 21:21:26,508 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:26,509 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 5 states have (on average 2.6) internal successors, (13), 11 states have internal predecessors, (13), 8 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 3 states have call predecessors, (8), 8 states have call successors, (8) Word has length 17
[2025-04-28 21:21:26,509 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,510 INFO  L225             Difference]: With dead ends: 24
[2025-04-28 21:21:26,510 INFO  L226             Difference]: Without dead ends: 24
[2025-04-28 21:21:26,512 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 44 GetRequests, 28 SyntacticMatches, 3 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 21 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=44, Invalid=166, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:26,513 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 5 mSDsluCounter, 98 mSDsCounter, 0 mSdLazyCounter, 59 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 115 SdHoareTripleChecker+Invalid, 60 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 59 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,513 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 115 Invalid, 60 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 59 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:26,514 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 24 states.
[2025-04-28 21:21:26,521 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 24 to 22.
[2025-04-28 21:21:26,521 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 10 states have (on average 1.2) internal successors, (12), 12 states have internal predecessors, (12), 5 states have call successors, (5), 3 states have call predecessors, (5), 6 states have return successors, (9), 6 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:26,522 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 26 transitions.
[2025-04-28 21:21:26,523 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 26 transitions. Word has length 17
[2025-04-28 21:21:26,523 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,523 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 26 transitions.
[2025-04-28 21:21:26,523 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 5 states have (on average 2.6) internal successors, (13), 11 states have internal predecessors, (13), 8 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 3 states have call predecessors, (8), 8 states have call successors, (8)
[2025-04-28 21:21:26,523 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 26 transitions.
[2025-04-28 21:21:26,524 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:26,524 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,524 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,530 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:26,725 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:26,725 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,726 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,726 INFO  L85        PathProgramCache]: Analyzing trace with hash 1561869207, now seen corresponding path program 1 times
[2025-04-28 21:21:26,726 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,726 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1479023178]
[2025-04-28 21:21:26,726 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,726 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,731 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:26,748 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:26,748 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,748 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,045 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:27,045 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,045 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1479023178]
[2025-04-28 21:21:27,045 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1479023178] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,045 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1361676728]
[2025-04-28 21:21:27,045 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,045 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,049 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,051 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:27,055 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:27,098 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:27,117 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:27,117 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,117 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,118 INFO  L256         TraceCheckSpWp]: Trace formula consists of 60 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:27,120 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,315 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:27,315 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:28,227 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:28,228 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1361676728] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:28,228 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:28,228 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 20
[2025-04-28 21:21:28,228 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [244719274]
[2025-04-28 21:21:28,228 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,229 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:28,229 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,230 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:28,230 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=47, Invalid=333, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:28,230 INFO  L87              Difference]: Start difference. First operand 22 states and 26 transitions. Second operand  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (12), 7 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:21:28,604 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,605 INFO  L93              Difference]: Finished difference Result 26 states and 31 transitions.
[2025-04-28 21:21:28,605 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:28,605 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (12), 7 states have call predecessors, (12), 11 states have call successors, (12) Word has length 21
[2025-04-28 21:21:28,606 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,606 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:28,606 INFO  L226             Difference]: Without dead ends: 22
[2025-04-28 21:21:28,607 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 28 SyntacticMatches, 5 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 40 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=103, Invalid=599, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:28,608 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 19 mSDsluCounter, 190 mSDsCounter, 0 mSdLazyCounter, 172 mSolverCounterSat, 36 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 207 SdHoareTripleChecker+Invalid, 208 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 36 IncrementalHoareTripleChecker+Valid, 172 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,608 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 207 Invalid, 208 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [36 Valid, 172 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:28,609 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 22 states.
[2025-04-28 21:21:28,612 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 22 to 20.
[2025-04-28 21:21:28,612 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 20 states, 9 states have (on average 1.2222222222222223) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 5 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:28,613 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 23 transitions.
[2025-04-28 21:21:28,613 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 23 transitions. Word has length 21
[2025-04-28 21:21:28,613 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,613 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 23 transitions.
[2025-04-28 21:21:28,614 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (12), 7 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:21:28,614 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 23 transitions.
[2025-04-28 21:21:28,614 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:28,614 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,615 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,620 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:28,819 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,819 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,819 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,820 INFO  L85        PathProgramCache]: Analyzing trace with hash 721441492, now seen corresponding path program 2 times
[2025-04-28 21:21:28,820 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,820 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1263355548]
[2025-04-28 21:21:28,820 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:28,820 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,826 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:21:28,831 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:28,831 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:28,831 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,992 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:28,992 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,992 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1263355548]
[2025-04-28 21:21:28,992 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1263355548] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,992 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1898805185]
[2025-04-28 21:21:28,992 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:28,992 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,995 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,997 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:21:29,000 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,037 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:21:29,048 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:29,048 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:29,048 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,049 INFO  L256         TraceCheckSpWp]: Trace formula consists of 59 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,052 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,234 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 3 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:29,234 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:30,728 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:30,729 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1898805185] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:30,729 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:30,729 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 21
[2025-04-28 21:21:30,729 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1012727943]
[2025-04-28 21:21:30,729 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,729 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:30,730 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,730 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:30,731 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=60, Invalid=360, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:30,731 INFO  L87              Difference]: Start difference. First operand 20 states and 23 transitions. Second operand  has 21 states, 11 states have (on average 2.090909090909091) internal successors, (23), 20 states have internal predecessors, (23), 11 states have call successors, (11), 1 states have call predecessors, (11), 10 states have return successors, (13), 8 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:21:30,884 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,884 INFO  L93              Difference]: Finished difference Result 22 states and 25 transitions.
[2025-04-28 21:21:30,885 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:30,885 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 11 states have (on average 2.090909090909091) internal successors, (23), 20 states have internal predecessors, (23), 11 states have call successors, (11), 1 states have call predecessors, (11), 10 states have return successors, (13), 8 states have call predecessors, (13), 11 states have call successors, (13) Word has length 21
[2025-04-28 21:21:30,885 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,886 INFO  L225             Difference]: With dead ends: 22
[2025-04-28 21:21:30,886 INFO  L226             Difference]: Without dead ends: 22
[2025-04-28 21:21:30,886 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 55 GetRequests, 30 SyntacticMatches, 2 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 70 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=100, Invalid=500, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:30,887 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 7 mSDsluCounter, 166 mSDsCounter, 0 mSdLazyCounter, 93 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 184 SdHoareTripleChecker+Invalid, 98 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 93 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,887 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 184 Invalid, 98 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 93 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:30,888 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 22 states.
[2025-04-28 21:21:30,891 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 22 to 22.
[2025-04-28 21:21:30,891 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 10 states have (on average 1.2) internal successors, (12), 12 states have internal predecessors, (12), 5 states have call successors, (5), 3 states have call predecessors, (5), 6 states have return successors, (8), 6 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:30,892 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 25 transitions.
[2025-04-28 21:21:30,892 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 25 transitions. Word has length 21
[2025-04-28 21:21:30,892 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,892 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 25 transitions.
[2025-04-28 21:21:30,892 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 11 states have (on average 2.090909090909091) internal successors, (23), 20 states have internal predecessors, (23), 11 states have call successors, (11), 1 states have call predecessors, (11), 10 states have return successors, (13), 8 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:21:30,892 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 25 transitions.
[2025-04-28 21:21:30,893 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:30,893 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,893 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,899 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:31,093 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,094 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,094 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,095 INFO  L85        PathProgramCache]: Analyzing trace with hash 702223097, now seen corresponding path program 2 times
[2025-04-28 21:21:31,095 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,095 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1371991942]
[2025-04-28 21:21:31,095 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:31,095 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,100 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:31,108 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:31,108 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:31,108 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,331 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:31,331 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,331 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1371991942]
[2025-04-28 21:21:31,331 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1371991942] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,331 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [676944638]
[2025-04-28 21:21:31,331 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:31,332 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,334 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,338 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:31,341 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,389 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:31,403 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:31,403 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:31,403 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,404 INFO  L256         TraceCheckSpWp]: Trace formula consists of 72 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,405 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,639 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:31,641 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,527 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:33,527 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [676944638] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,527 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,528 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 25
[2025-04-28 21:21:33,528 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1725955396]
[2025-04-28 21:21:33,528 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,529 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:21:33,529 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,530 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:21:33,531 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=65, Invalid=535, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:33,531 INFO  L87              Difference]: Start difference. First operand 22 states and 25 transitions. Second operand  has 25 states, 12 states have (on average 2.25) internal successors, (27), 24 states have internal predecessors, (27), 14 states have call successors, (14), 1 states have call predecessors, (14), 11 states have return successors, (16), 9 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:21:33,959 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,959 INFO  L93              Difference]: Finished difference Result 34 states and 39 transitions.
[2025-04-28 21:21:33,962 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:33,962 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 12 states have (on average 2.25) internal successors, (27), 24 states have internal predecessors, (27), 14 states have call successors, (14), 1 states have call predecessors, (14), 11 states have return successors, (16), 9 states have call predecessors, (16), 14 states have call successors, (16) Word has length 25
[2025-04-28 21:21:33,967 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,967 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:33,968 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:33,968 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 71 GetRequests, 33 SyntacticMatches, 5 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 164 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=156, Invalid=1034, Unknown=0, NotChecked=0, Total=1190
[2025-04-28 21:21:33,969 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 28 mSDsluCounter, 206 mSDsCounter, 0 mSdLazyCounter, 169 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 35 SdHoareTripleChecker+Valid, 224 SdHoareTripleChecker+Invalid, 203 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 169 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,969 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [35 Valid, 224 Invalid, 203 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 169 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:33,970 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:33,974 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 28.
[2025-04-28 21:21:33,974 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 13 states have (on average 1.1538461538461537) internal successors, (15), 15 states have internal predecessors, (15), 5 states have call successors, (5), 3 states have call predecessors, (5), 9 states have return successors, (13), 9 states have call predecessors, (13), 5 states have call successors, (13)
[2025-04-28 21:21:33,975 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 33 transitions.
[2025-04-28 21:21:33,975 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 33 transitions. Word has length 25
[2025-04-28 21:21:33,975 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,975 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 33 transitions.
[2025-04-28 21:21:33,976 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 12 states have (on average 2.25) internal successors, (27), 24 states have internal predecessors, (27), 14 states have call successors, (14), 1 states have call predecessors, (14), 11 states have return successors, (16), 9 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:21:33,976 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 33 transitions.
[2025-04-28 21:21:33,976 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:33,977 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,977 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,982 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:34,181 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:21:34,181 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,181 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,181 INFO  L85        PathProgramCache]: Analyzing trace with hash 690176734, now seen corresponding path program 3 times
[2025-04-28 21:21:34,182 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,182 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1780725083]
[2025-04-28 21:21:34,182 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:34,182 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,187 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 29 statements into 3 equivalence classes.
[2025-04-28 21:21:34,193 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:34,193 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:34,193 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,411 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 2 proven. 11 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:34,411 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,411 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1780725083]
[2025-04-28 21:21:34,411 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1780725083] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,411 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2025705788]
[2025-04-28 21:21:34,411 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:34,411 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,415 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,417 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:34,420 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,478 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 29 statements into 3 equivalence classes.
[2025-04-28 21:21:34,491 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:34,491 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:34,491 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,492 INFO  L256         TraceCheckSpWp]: Trace formula consists of 85 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,494 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,540 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 2 proven. 11 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:34,540 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:36,071 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 2 proven. 12 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:36,075 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2025705788] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:36,076 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:36,076 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 14] total 18
[2025-04-28 21:21:36,076 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [362311127]
[2025-04-28 21:21:36,076 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,076 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:36,077 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,077 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:36,077 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=252, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:36,078 INFO  L87              Difference]: Start difference. First operand 28 states and 33 transitions. Second operand  has 18 states, 8 states have (on average 2.375) internal successors, (19), 17 states have internal predecessors, (19), 11 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (12), 6 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:21:36,261 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,261 INFO  L93              Difference]: Finished difference Result 36 states and 41 transitions.
[2025-04-28 21:21:36,262 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:36,262 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 8 states have (on average 2.375) internal successors, (19), 17 states have internal predecessors, (19), 11 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (12), 6 states have call predecessors, (12), 11 states have call successors, (12) Word has length 29
[2025-04-28 21:21:36,262 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,263 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:36,263 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:36,263 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 77 GetRequests, 48 SyntacticMatches, 7 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 86 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=107, Invalid=445, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:36,264 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 14 mSDsluCounter, 109 mSDsCounter, 0 mSdLazyCounter, 91 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 127 SdHoareTripleChecker+Invalid, 103 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 91 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,264 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 127 Invalid, 103 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 91 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,265 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:36,268 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 28.
[2025-04-28 21:21:36,268 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 13 states have (on average 1.1538461538461537) internal successors, (15), 15 states have internal predecessors, (15), 5 states have call successors, (5), 3 states have call predecessors, (5), 9 states have return successors, (12), 9 states have call predecessors, (12), 5 states have call successors, (12)
[2025-04-28 21:21:36,269 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 32 transitions.
[2025-04-28 21:21:36,269 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 32 transitions. Word has length 29
[2025-04-28 21:21:36,269 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,269 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 32 transitions.
[2025-04-28 21:21:36,269 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 8 states have (on average 2.375) internal successors, (19), 17 states have internal predecessors, (19), 11 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (12), 6 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:21:36,269 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 32 transitions.
[2025-04-28 21:21:36,270 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:36,270 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,270 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,275 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:36,474 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,474 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,474 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,474 INFO  L85        PathProgramCache]: Analyzing trace with hash 1334982720, now seen corresponding path program 4 times
[2025-04-28 21:21:36,474 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,475 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1670567418]
[2025-04-28 21:21:36,475 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:36,475 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,479 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 33 statements into 2 equivalence classes.
[2025-04-28 21:21:36,485 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:36,485 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:36,485 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,784 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 22 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:36,784 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,784 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1670567418]
[2025-04-28 21:21:36,784 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1670567418] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,784 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1998987885]
[2025-04-28 21:21:36,784 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:36,784 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,787 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,789 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:36,792 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,867 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 33 statements into 2 equivalence classes.
[2025-04-28 21:21:36,881 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:36,881 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:36,881 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,882 INFO  L256         TraceCheckSpWp]: Trace formula consists of 97 conjuncts, 26 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,884 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,208 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 21 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:37,208 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:41,476 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 22 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:41,476 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1998987885] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:41,476 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:41,476 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 15, 16] total 33
[2025-04-28 21:21:41,477 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1442194255]
[2025-04-28 21:21:41,477 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,477 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 33 states
[2025-04-28 21:21:41,477 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,478 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 33 interpolants.
[2025-04-28 21:21:41,478 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=91, Invalid=965, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:41,479 INFO  L87              Difference]: Start difference. First operand 28 states and 32 transitions. Second operand  has 33 states, 15 states have (on average 2.3333333333333335) internal successors, (35), 32 states have internal predecessors, (35), 19 states have call successors, (19), 1 states have call predecessors, (19), 14 states have return successors, (22), 12 states have call predecessors, (22), 19 states have call successors, (22)
[2025-04-28 21:21:42,181 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,181 INFO  L93              Difference]: Finished difference Result 42 states and 47 transitions.
[2025-04-28 21:21:42,182 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:21:42,182 INFO  L79                 Accepts]: Start accepts. Automaton has  has 33 states, 15 states have (on average 2.3333333333333335) internal successors, (35), 32 states have internal predecessors, (35), 19 states have call successors, (19), 1 states have call predecessors, (19), 14 states have return successors, (22), 12 states have call predecessors, (22), 19 states have call successors, (22) Word has length 33
[2025-04-28 21:21:42,182 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,183 INFO  L225             Difference]: With dead ends: 42
[2025-04-28 21:21:42,183 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:21:42,184 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 96 GetRequests, 43 SyntacticMatches, 7 SemanticMatches, 46 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 323 ImplicationChecksByTransitivity, 1.2s TimeCoverageRelationStatistics Valid=266, Invalid=1990, Unknown=0, NotChecked=0, Total=2256
[2025-04-28 21:21:42,185 INFO  L437           NwaCegarLoop]: 20 mSDtfsCounter, 65 mSDsluCounter, 280 mSDsCounter, 0 mSdLazyCounter, 244 mSolverCounterSat, 93 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 66 SdHoareTripleChecker+Valid, 300 SdHoareTripleChecker+Invalid, 337 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 93 IncrementalHoareTripleChecker+Valid, 244 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,185 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [66 Valid, 300 Invalid, 337 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [93 Valid, 244 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:42,186 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:21:42,190 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 34.
[2025-04-28 21:21:42,190 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 16 states have (on average 1.125) internal successors, (18), 18 states have internal predecessors, (18), 5 states have call successors, (5), 3 states have call predecessors, (5), 12 states have return successors, (16), 12 states have call predecessors, (16), 5 states have call successors, (16)
[2025-04-28 21:21:42,191 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 39 transitions.
[2025-04-28 21:21:42,191 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 39 transitions. Word has length 33
[2025-04-28 21:21:42,195 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,195 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 39 transitions.
[2025-04-28 21:21:42,195 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 33 states, 15 states have (on average 2.3333333333333335) internal successors, (35), 32 states have internal predecessors, (35), 19 states have call successors, (19), 1 states have call predecessors, (19), 14 states have return successors, (22), 12 states have call predecessors, (22), 19 states have call successors, (22)
[2025-04-28 21:21:42,195 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 39 transitions.
[2025-04-28 21:21:42,196 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:42,196 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,196 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,202 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:42,396 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,397 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,397 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,397 INFO  L85        PathProgramCache]: Analyzing trace with hash 1962709535, now seen corresponding path program 5 times
[2025-04-28 21:21:42,397 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,397 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [489760592]
[2025-04-28 21:21:42,397 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:42,397 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,402 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 37 statements into 6 equivalence classes.
[2025-04-28 21:21:42,411 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:42,411 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:42,411 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,809 INFO  L134       CoverageAnalysis]: Checked inductivity of 58 backedges. 0 proven. 42 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:42,810 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,810 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [489760592]
[2025-04-28 21:21:42,810 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [489760592] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,810 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [638023990]
[2025-04-28 21:21:42,810 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:42,810 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,813 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,815 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:42,818 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,935 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 37 statements into 6 equivalence classes.
[2025-04-28 21:21:42,958 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:42,958 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:42,958 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,959 INFO  L256         TraceCheckSpWp]: Trace formula consists of 108 conjuncts, 30 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,961 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,180 INFO  L134       CoverageAnalysis]: Checked inductivity of 58 backedges. 18 proven. 21 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:43,180 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,046 INFO  L134       CoverageAnalysis]: Checked inductivity of 58 backedges. 12 proven. 30 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:51,046 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [638023990] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,046 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,046 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 16, 18] total 35
[2025-04-28 21:21:51,046 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [809861033]
[2025-04-28 21:21:51,046 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,047 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 35 states
[2025-04-28 21:21:51,047 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,048 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 35 interpolants.
[2025-04-28 21:21:51,048 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=137, Invalid=1053, Unknown=0, NotChecked=0, Total=1190
[2025-04-28 21:21:51,048 INFO  L87              Difference]: Start difference. First operand 34 states and 39 transitions. Second operand  has 35 states, 17 states have (on average 2.176470588235294) internal successors, (37), 34 states have internal predecessors, (37), 19 states have call successors, (19), 1 states have call predecessors, (19), 16 states have return successors, (22), 14 states have call predecessors, (22), 19 states have call successors, (22)
[2025-04-28 21:21:51,429 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,429 INFO  L93              Difference]: Finished difference Result 38 states and 43 transitions.
[2025-04-28 21:21:51,430 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:51,430 INFO  L79                 Accepts]: Start accepts. Automaton has  has 35 states, 17 states have (on average 2.176470588235294) internal successors, (37), 34 states have internal predecessors, (37), 19 states have call successors, (19), 1 states have call predecessors, (19), 16 states have return successors, (22), 14 states have call predecessors, (22), 19 states have call successors, (22) Word has length 37
[2025-04-28 21:21:51,430 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,432 INFO  L225             Difference]: With dead ends: 38
[2025-04-28 21:21:51,432 INFO  L226             Difference]: Without dead ends: 38
[2025-04-28 21:21:51,433 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 99 GetRequests, 54 SyntacticMatches, 4 SemanticMatches, 41 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 217 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=284, Invalid=1522, Unknown=0, NotChecked=0, Total=1806
[2025-04-28 21:21:51,434 INFO  L437           NwaCegarLoop]: 21 mSDtfsCounter, 10 mSDsluCounter, 247 mSDsCounter, 0 mSdLazyCounter, 242 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 268 SdHoareTripleChecker+Invalid, 253 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 242 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,435 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 268 Invalid, 253 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 242 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:51,436 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 38 states.
[2025-04-28 21:21:51,441 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 38 to 34.
[2025-04-28 21:21:51,441 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 16 states have (on average 1.125) internal successors, (18), 18 states have internal predecessors, (18), 5 states have call successors, (5), 3 states have call predecessors, (5), 12 states have return successors, (16), 12 states have call predecessors, (16), 5 states have call successors, (16)
[2025-04-28 21:21:51,442 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 39 transitions.
[2025-04-28 21:21:51,442 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 39 transitions. Word has length 37
[2025-04-28 21:21:51,442 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,442 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 39 transitions.
[2025-04-28 21:21:51,442 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 35 states, 17 states have (on average 2.176470588235294) internal successors, (37), 34 states have internal predecessors, (37), 19 states have call successors, (19), 1 states have call predecessors, (19), 16 states have return successors, (22), 14 states have call predecessors, (22), 19 states have call successors, (22)
[2025-04-28 21:21:51,442 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 39 transitions.
[2025-04-28 21:21:51,443 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:51,443 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,443 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,451 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:51,648 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable8
[2025-04-28 21:21:51,648 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,648 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,649 INFO  L85        PathProgramCache]: Analyzing trace with hash 1966846026, now seen corresponding path program 6 times
[2025-04-28 21:21:51,649 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,649 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1496498484]
[2025-04-28 21:21:51,649 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:51,649 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,656 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 41 statements into 5 equivalence classes.
[2025-04-28 21:21:51,666 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 5 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:51,666 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 5 check-sat command(s)
[2025-04-28 21:21:51,666 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,024 INFO  L134       CoverageAnalysis]: Checked inductivity of 57 backedges. 12 proven. 25 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-04-28 21:21:52,024 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,024 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1496498484]
[2025-04-28 21:21:52,024 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1496498484] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,024 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [80079919]
[2025-04-28 21:21:52,025 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:52,025 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,027 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,030 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,034 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,235 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 41 statements into 5 equivalence classes.
[2025-04-28 21:21:52,257 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 5 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:52,257 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 5 check-sat command(s)
[2025-04-28 21:21:52,258 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,259 INFO  L256         TraceCheckSpWp]: Trace formula consists of 123 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,261 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,329 INFO  L134       CoverageAnalysis]: Checked inductivity of 57 backedges. 12 proven. 23 refuted. 0 times theorem prover too weak. 22 trivial. 0 not checked.
[2025-04-28 21:21:52,329 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,617 INFO  L134       CoverageAnalysis]: Checked inductivity of 57 backedges. 12 proven. 29 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:56,618 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [80079919] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,619 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,619 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [17, 16, 20] total 26
[2025-04-28 21:21:56,621 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [167405833]
[2025-04-28 21:21:56,621 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,622 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:56,622 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,622 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:56,623 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=99, Invalid=551, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:56,623 INFO  L87              Difference]: Start difference. First operand 34 states and 39 transitions. Second operand  has 26 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 25 states have internal predecessors, (27), 16 states have call successors, (16), 1 states have call predecessors, (16), 10 states have return successors, (20), 9 states have call predecessors, (20), 16 states have call successors, (20)
[2025-04-28 21:21:56,982 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,982 INFO  L93              Difference]: Finished difference Result 46 states and 51 transitions.
[2025-04-28 21:21:56,985 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:56,985 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 25 states have internal predecessors, (27), 16 states have call successors, (16), 1 states have call predecessors, (16), 10 states have return successors, (20), 9 states have call predecessors, (20), 16 states have call successors, (20) Word has length 41
[2025-04-28 21:21:56,985 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,986 INFO  L225             Difference]: With dead ends: 46
[2025-04-28 21:21:56,986 INFO  L226             Difference]: Without dead ends: 36
[2025-04-28 21:21:56,987 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 111 GetRequests, 68 SyntacticMatches, 9 SemanticMatches, 34 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 277 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=226, Invalid=1034, Unknown=0, NotChecked=0, Total=1260
[2025-04-28 21:21:56,987 INFO  L437           NwaCegarLoop]: 20 mSDtfsCounter, 13 mSDsluCounter, 244 mSDsCounter, 0 mSdLazyCounter, 198 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 264 SdHoareTripleChecker+Invalid, 209 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 198 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,988 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 264 Invalid, 209 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 198 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:56,991 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 36 states.
[2025-04-28 21:21:56,999 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 36 to 34.
[2025-04-28 21:21:57,000 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 16 states have (on average 1.125) internal successors, (18), 18 states have internal predecessors, (18), 5 states have call successors, (5), 3 states have call predecessors, (5), 12 states have return successors, (15), 12 states have call predecessors, (15), 5 states have call successors, (15)
[2025-04-28 21:21:57,000 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 38 transitions.
[2025-04-28 21:21:57,000 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 38 transitions. Word has length 41
[2025-04-28 21:21:57,001 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,001 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 38 transitions.
[2025-04-28 21:21:57,001 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 25 states have internal predecessors, (27), 16 states have call successors, (16), 1 states have call predecessors, (16), 10 states have return successors, (20), 9 states have call predecessors, (20), 16 states have call successors, (20)
[2025-04-28 21:21:57,001 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 38 transitions.
[2025-04-28 21:21:57,004 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:57,005 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,005 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,012 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:57,205 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:21:57,205 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,206 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,206 INFO  L85        PathProgramCache]: Analyzing trace with hash -1990639740, now seen corresponding path program 7 times
[2025-04-28 21:21:57,206 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,206 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [690769356]
[2025-04-28 21:21:57,206 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:57,206 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,211 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-04-28 21:21:57,222 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:57,222 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,222 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,709 INFO  L134       CoverageAnalysis]: Checked inductivity of 65 backedges. 0 proven. 47 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:57,709 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,709 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [690769356]
[2025-04-28 21:21:57,709 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [690769356] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,709 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [433498509]
[2025-04-28 21:21:57,709 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:57,710 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,712 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,714 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:57,718 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
