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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:40,171 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:40,286 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e3d57506-5002-4d75-bb94-18f73a279f2e/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:40,295 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:40,299 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:40,334 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:40,338 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:40,338 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:40,339 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:40,340 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:40,341 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:40,341 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:40,341 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:40,341 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:40,341 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:40,343 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:40,343 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:40,343 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:40,344 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,344 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:40,344 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:40,344 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:40,344 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:40,344 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:40,344 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:40,345 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:40,346 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:40,677 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:40,688 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:40,690 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:40,692 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:40,692 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:40,695 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e3d57506-5002-4d75-bb94-18f73a279f2e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-122.smt2
[2025-04-28 21:21:40,697 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:40,704 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:41,004 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e3d57506-5002-4d75-bb94-18f73a279f2e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-122.smt2
[2025-04-28 21:21:41,007 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:41,008 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:41,009 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:41,009 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:41,009 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:41,015 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,052 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41 Unit
[2025-04-28 21:21:41,052 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:41,053 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,054 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:41,054 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:41,072 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,072 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,104 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,105 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,108 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,113 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,116 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,117 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,118 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,133 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,134 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:41,135 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:41,135 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:41,137 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,140 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,154 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,174 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:41,179 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:41,200 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:41,200 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:41,200 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:41,200 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:41,200 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:41,200 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:41,200 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Inv given in one single declaration
[2025-04-28 21:21:41,201 INFO  L130     BoogieDeclarations]: Found specification of procedure Inv
[2025-04-28 21:21:41,201 INFO  L138     BoogieDeclarations]: Found implementation of procedure Inv
[2025-04-28 21:21:41,201 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:41,201 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:41,201 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:41,262 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:41,266 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:41,626 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:41,626 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:41,645 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:41,646 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:41,646 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41 BoogieIcfgContainer
[2025-04-28 21:21:41,647 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:41,654 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:41,654 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:41,658 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:41,658 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/3) ...
[2025-04-28 21:21:41,659 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@b010584 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,659 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (2/3) ...
[2025-04-28 21:21:41,660 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@b010584 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,660 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41" (3/3) ...
[2025-04-28 21:21:41,664 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:41,682 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:41,686 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 39 locations, 113 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:41,746 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:41,769 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;@20547dc4, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:41,769 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:41,774 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 39 states, 8 states have (on average 3.625) internal successors, (29), 29 states have internal predecessors, (29), 28 states have call successors, (28), 3 states have call predecessors, (28), 3 states have return successors, (28), 8 states have call predecessors, (28), 28 states have call successors, (28)
[2025-04-28 21:21:41,807 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-04-28 21:21:41,808 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,808 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-04-28 21:21:41,809 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,819 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,820 INFO  L85        PathProgramCache]: Analyzing trace with hash 192775405, now seen corresponding path program 1 times
[2025-04-28 21:21:41,830 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,831 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1163830376]
[2025-04-28 21:21:41,831 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,833 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,863 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-04-28 21:21:41,866 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-04-28 21:21:41,866 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,866 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,906 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:41,907 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,907 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1163830376]
[2025-04-28 21:21:41,908 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1163830376] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,908 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,914 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-04-28 21:21:41,916 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [384436505]
[2025-04-28 21:21:41,916 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,921 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-04-28 21:21:41,922 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,961 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-04-28 21:21:41,963 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:41,965 INFO  L87              Difference]: Start difference. First operand  has 39 states, 8 states have (on average 3.625) internal successors, (29), 29 states have internal predecessors, (29), 28 states have call successors, (28), 3 states have call predecessors, (28), 3 states have return successors, (28), 8 states have call predecessors, (28), 28 states have call successors, (28) Second operand  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:42,008 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,012 INFO  L93              Difference]: Finished difference Result 37 states and 82 transitions.
[2025-04-28 21:21:42,013 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-04-28 21:21:42,015 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1) Word has length 5
[2025-04-28 21:21:42,015 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,029 INFO  L225             Difference]: With dead ends: 37
[2025-04-28 21:21:42,031 INFO  L226             Difference]: Without dead ends: 37
[2025-04-28 21:21:42,033 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:42,037 INFO  L437           NwaCegarLoop]: 82 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 82 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,039 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 82 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:42,063 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 37 states.
[2025-04-28 21:21:42,105 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 37 to 37.
[2025-04-28 21:21:42,107 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 37 states, 6 states have (on average 4.333333333333333) internal successors, (26), 26 states have internal predecessors, (26), 28 states have call successors, (28), 3 states have call predecessors, (28), 3 states have return successors, (28), 8 states have call predecessors, (28), 28 states have call successors, (28)
[2025-04-28 21:21:42,117 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 37 states to 37 states and 82 transitions.
[2025-04-28 21:21:42,121 INFO  L79                 Accepts]: Start accepts. Automaton has 37 states and 82 transitions. Word has length 5
[2025-04-28 21:21:42,122 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,122 INFO  L485      AbstractCegarLoop]: Abstraction has 37 states and 82 transitions.
[2025-04-28 21:21:42,122 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:42,123 INFO  L278                IsEmpty]: Start isEmpty. Operand 37 states and 82 transitions.
[2025-04-28 21:21:42,138 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:42,139 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,139 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,142 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:42,142 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,143 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,143 INFO  L85        PathProgramCache]: Analyzing trace with hash -1670096426, now seen corresponding path program 1 times
[2025-04-28 21:21:42,143 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,143 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1044577691]
[2025-04-28 21:21:42,144 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,144 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,156 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:42,178 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:42,178 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,178 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,323 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:42,326 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,326 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1044577691]
[2025-04-28 21:21:42,326 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1044577691] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,326 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,326 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:42,326 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1753643572]
[2025-04-28 21:21:42,327 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,328 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:42,329 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,329 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:42,330 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:42,330 INFO  L87              Difference]: Start difference. First operand 37 states and 82 transitions. Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:42,878 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,878 INFO  L93              Difference]: Finished difference Result 49 states and 136 transitions.
[2025-04-28 21:21:42,879 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:42,880 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:42,880 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,886 INFO  L225             Difference]: With dead ends: 49
[2025-04-28 21:21:42,886 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:21:42,886 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:42,889 INFO  L437           NwaCegarLoop]: 73 mSDtfsCounter, 6 mSDsluCounter, 84 mSDsCounter, 0 mSdLazyCounter, 134 mSolverCounterSat, 30 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 157 SdHoareTripleChecker+Invalid, 164 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 30 IncrementalHoareTripleChecker+Valid, 134 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,889 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 157 Invalid, 164 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [30 Valid, 134 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:42,890 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:21:42,914 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 49.
[2025-04-28 21:21:42,916 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 49 states, 8 states have (on average 4.125) internal successors, (33), 32 states have internal predecessors, (33), 38 states have call successors, (38), 4 states have call predecessors, (38), 4 states have return successors, (65), 13 states have call predecessors, (65), 38 states have call successors, (65)
[2025-04-28 21:21:42,919 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 49 states to 49 states and 136 transitions.
[2025-04-28 21:21:42,922 INFO  L79                 Accepts]: Start accepts. Automaton has 49 states and 136 transitions. Word has length 12
[2025-04-28 21:21:42,923 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,923 INFO  L485      AbstractCegarLoop]: Abstraction has 49 states and 136 transitions.
[2025-04-28 21:21:42,924 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:42,924 INFO  L278                IsEmpty]: Start isEmpty. Operand 49 states and 136 transitions.
[2025-04-28 21:21:42,930 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:42,932 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,933 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,933 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:42,933 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,934 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,934 INFO  L85        PathProgramCache]: Analyzing trace with hash -1253618975, now seen corresponding path program 1 times
[2025-04-28 21:21:42,934 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,934 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1909756984]
[2025-04-28 21:21:42,934 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,935 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,947 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:42,960 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:42,960 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,960 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,079 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:43,080 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,080 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1909756984]
[2025-04-28 21:21:43,080 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1909756984] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,080 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1271028211]
[2025-04-28 21:21:43,081 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,081 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,085 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,089 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:43,093 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,149 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:43,182 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:43,182 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,182 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,186 INFO  L256         TraceCheckSpWp]: Trace formula consists of 69 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,198 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,299 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:43,300 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,572 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:43,572 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1271028211] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,572 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,573 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-04-28 21:21:43,573 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1871749171]
[2025-04-28 21:21:43,573 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,573 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:43,573 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,576 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:43,576 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:43,576 INFO  L87              Difference]: Start difference. First operand 49 states and 136 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:44,579 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,579 INFO  L93              Difference]: Finished difference Result 101 states and 470 transitions.
[2025-04-28 21:21:44,580 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:44,580 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 15
[2025-04-28 21:21:44,580 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,594 INFO  L225             Difference]: With dead ends: 101
[2025-04-28 21:21:44,594 INFO  L226             Difference]: Without dead ends: 101
[2025-04-28 21:21:44,594 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 35 GetRequests, 28 SyntacticMatches, 2 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:44,595 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 26 mSDsluCounter, 139 mSDsCounter, 0 mSdLazyCounter, 328 mSolverCounterSat, 124 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 46 SdHoareTripleChecker+Valid, 248 SdHoareTripleChecker+Invalid, 452 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 124 IncrementalHoareTripleChecker+Valid, 328 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,596 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [46 Valid, 248 Invalid, 452 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [124 Valid, 328 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:44,597 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-04-28 21:21:44,663 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 81.
[2025-04-28 21:21:44,664 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 81 states, 11 states have (on average 5.0) internal successors, (55), 53 states have internal predecessors, (55), 66 states have call successors, (66), 5 states have call predecessors, (66), 6 states have return successors, (186), 23 states have call predecessors, (186), 66 states have call successors, (186)
[2025-04-28 21:21:44,669 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 81 states to 81 states and 307 transitions.
[2025-04-28 21:21:44,669 INFO  L79                 Accepts]: Start accepts. Automaton has 81 states and 307 transitions. Word has length 15
[2025-04-28 21:21:44,670 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,670 INFO  L485      AbstractCegarLoop]: Abstraction has 81 states and 307 transitions.
[2025-04-28 21:21:44,670 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:44,670 INFO  L278                IsEmpty]: Start isEmpty. Operand 81 states and 307 transitions.
[2025-04-28 21:21:44,678 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:44,678 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,679 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,685 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:44,883 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,883 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,884 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,885 INFO  L85        PathProgramCache]: Analyzing trace with hash -60398406, now seen corresponding path program 1 times
[2025-04-28 21:21:44,885 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,885 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1193642487]
[2025-04-28 21:21:44,885 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,885 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,892 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:44,898 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:44,898 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,898 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,938 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:44,938 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,938 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1193642487]
[2025-04-28 21:21:44,938 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1193642487] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,938 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,938 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:44,939 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [933515297]
[2025-04-28 21:21:44,939 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,939 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:44,939 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,939 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:44,940 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:44,940 INFO  L87              Difference]: Start difference. First operand 81 states and 307 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:45,306 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,306 INFO  L93              Difference]: Finished difference Result 117 states and 632 transitions.
[2025-04-28 21:21:45,307 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:45,307 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:45,307 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,321 INFO  L225             Difference]: With dead ends: 117
[2025-04-28 21:21:45,322 INFO  L226             Difference]: Without dead ends: 117
[2025-04-28 21:21:45,322 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:45,323 INFO  L437           NwaCegarLoop]: 98 mSDtfsCounter, 6 mSDsluCounter, 106 mSDsCounter, 0 mSdLazyCounter, 148 mSolverCounterSat, 30 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 204 SdHoareTripleChecker+Invalid, 178 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 30 IncrementalHoareTripleChecker+Valid, 148 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,323 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 204 Invalid, 178 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [30 Valid, 148 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:45,324 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-04-28 21:21:45,427 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 117.
[2025-04-28 21:21:45,429 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 117 states, 17 states have (on average 4.588235294117647) internal successors, (78), 67 states have internal predecessors, (78), 94 states have call successors, (94), 7 states have call predecessors, (94), 10 states have return successors, (460), 43 states have call predecessors, (460), 94 states have call successors, (460)
[2025-04-28 21:21:45,446 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 117 states to 117 states and 632 transitions.
[2025-04-28 21:21:45,446 INFO  L79                 Accepts]: Start accepts. Automaton has 117 states and 632 transitions. Word has length 16
[2025-04-28 21:21:45,447 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,447 INFO  L485      AbstractCegarLoop]: Abstraction has 117 states and 632 transitions.
[2025-04-28 21:21:45,447 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:45,447 INFO  L278                IsEmpty]: Start isEmpty. Operand 117 states and 632 transitions.
[2025-04-28 21:21:45,460 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:45,460 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,460 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,460 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:45,460 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,461 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,462 INFO  L85        PathProgramCache]: Analyzing trace with hash 955248509, now seen corresponding path program 1 times
[2025-04-28 21:21:45,462 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,462 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1560277787]
[2025-04-28 21:21:45,462 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,462 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,470 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:45,476 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:45,476 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,477 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,532 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:45,532 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,532 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1560277787]
[2025-04-28 21:21:45,532 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1560277787] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,532 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,533 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:45,533 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [634493464]
[2025-04-28 21:21:45,533 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,535 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:45,535 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,536 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:45,536 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:45,536 INFO  L87              Difference]: Start difference. First operand 117 states and 632 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:45,871 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,872 INFO  L93              Difference]: Finished difference Result 155 states and 1060 transitions.
[2025-04-28 21:21:45,873 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:45,873 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:45,874 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,893 INFO  L225             Difference]: With dead ends: 155
[2025-04-28 21:21:45,893 INFO  L226             Difference]: Without dead ends: 155
[2025-04-28 21:21:45,893 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:45,895 INFO  L437           NwaCegarLoop]: 96 mSDtfsCounter, 6 mSDsluCounter, 100 mSDsCounter, 0 mSdLazyCounter, 151 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 196 SdHoareTripleChecker+Invalid, 179 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 151 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,897 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 196 Invalid, 179 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 151 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:45,898 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 155 states.
[2025-04-28 21:21:46,015 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 155 to 153.
[2025-04-28 21:21:46,018 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 153 states, 23 states have (on average 4.521739130434782) internal successors, (104), 81 states have internal predecessors, (104), 122 states have call successors, (122), 9 states have call predecessors, (122), 14 states have return successors, (832), 63 states have call predecessors, (832), 122 states have call successors, (832)
[2025-04-28 21:21:46,029 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 153 states to 153 states and 1058 transitions.
[2025-04-28 21:21:46,030 INFO  L79                 Accepts]: Start accepts. Automaton has 153 states and 1058 transitions. Word has length 16
[2025-04-28 21:21:46,030 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,030 INFO  L485      AbstractCegarLoop]: Abstraction has 153 states and 1058 transitions.
[2025-04-28 21:21:46,030 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:46,031 INFO  L278                IsEmpty]: Start isEmpty. Operand 153 states and 1058 transitions.
[2025-04-28 21:21:46,047 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:46,047 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,047 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,047 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:46,047 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,048 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,051 INFO  L85        PathProgramCache]: Analyzing trace with hash -1090975078, now seen corresponding path program 1 times
[2025-04-28 21:21:46,052 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,052 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1018095145]
[2025-04-28 21:21:46,052 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,052 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,060 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:46,063 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:46,067 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,067 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,137 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:46,137 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,137 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1018095145]
[2025-04-28 21:21:46,137 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1018095145] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,137 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,137 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:46,137 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1226562666]
[2025-04-28 21:21:46,138 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,138 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:46,138 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,139 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:46,139 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,139 INFO  L87              Difference]: Start difference. First operand 153 states and 1058 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:46,447 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,447 INFO  L93              Difference]: Finished difference Result 153 states and 1056 transitions.
[2025-04-28 21:21:46,448 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:46,448 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:46,451 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,472 INFO  L225             Difference]: With dead ends: 153
[2025-04-28 21:21:46,475 INFO  L226             Difference]: Without dead ends: 153
[2025-04-28 21:21:46,475 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:46,476 INFO  L437           NwaCegarLoop]: 94 mSDtfsCounter, 6 mSDsluCounter, 96 mSDsCounter, 0 mSdLazyCounter, 147 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 190 SdHoareTripleChecker+Invalid, 173 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 147 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,476 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 190 Invalid, 173 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 147 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:46,477 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-04-28 21:21:46,587 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 153.
[2025-04-28 21:21:46,589 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 153 states, 23 states have (on average 4.521739130434782) internal successors, (104), 81 states have internal predecessors, (104), 122 states have call successors, (122), 9 states have call predecessors, (122), 14 states have return successors, (830), 63 states have call predecessors, (830), 122 states have call successors, (830)
[2025-04-28 21:21:46,598 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 153 states to 153 states and 1056 transitions.
[2025-04-28 21:21:46,599 INFO  L79                 Accepts]: Start accepts. Automaton has 153 states and 1056 transitions. Word has length 16
[2025-04-28 21:21:46,599 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,599 INFO  L485      AbstractCegarLoop]: Abstraction has 153 states and 1056 transitions.
[2025-04-28 21:21:46,599 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:46,600 INFO  L278                IsEmpty]: Start isEmpty. Operand 153 states and 1056 transitions.
[2025-04-28 21:21:46,611 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:46,612 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,612 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,612 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:46,612 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,613 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,613 INFO  L85        PathProgramCache]: Analyzing trace with hash 1636392532, now seen corresponding path program 1 times
[2025-04-28 21:21:46,613 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,613 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1075614154]
[2025-04-28 21:21:46,613 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,613 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,619 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:46,627 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:46,627 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,627 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,689 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:46,689 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,689 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1075614154]
[2025-04-28 21:21:46,689 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1075614154] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,689 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,689 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:46,690 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [319600614]
[2025-04-28 21:21:46,690 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,690 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:46,690 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,690 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:46,690 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,691 INFO  L87              Difference]: Start difference. First operand 153 states and 1056 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:46,978 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,978 INFO  L93              Difference]: Finished difference Result 179 states and 1544 transitions.
[2025-04-28 21:21:46,978 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:46,978 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:21:46,979 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,012 INFO  L225             Difference]: With dead ends: 179
[2025-04-28 21:21:47,012 INFO  L226             Difference]: Without dead ends: 179
[2025-04-28 21:21:47,013 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:47,014 INFO  L437           NwaCegarLoop]: 104 mSDtfsCounter, 6 mSDsluCounter, 117 mSDsCounter, 0 mSdLazyCounter, 146 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 221 SdHoareTripleChecker+Invalid, 164 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 146 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,014 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 221 Invalid, 164 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 146 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:47,017 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 179 states.
[2025-04-28 21:21:47,148 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 179 to 171.
[2025-04-28 21:21:47,150 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 171 states, 26 states have (on average 4.3076923076923075) internal successors, (112), 88 states have internal predecessors, (112), 136 states have call successors, (136), 10 states have call predecessors, (136), 16 states have return successors, (1018), 73 states have call predecessors, (1018), 136 states have call successors, (1018)
[2025-04-28 21:21:47,160 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 171 states to 171 states and 1266 transitions.
[2025-04-28 21:21:47,160 INFO  L79                 Accepts]: Start accepts. Automaton has 171 states and 1266 transitions. Word has length 16
[2025-04-28 21:21:47,161 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,161 INFO  L485      AbstractCegarLoop]: Abstraction has 171 states and 1266 transitions.
[2025-04-28 21:21:47,161 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:47,161 INFO  L278                IsEmpty]: Start isEmpty. Operand 171 states and 1266 transitions.
[2025-04-28 21:21:47,179 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:47,179 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,180 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,181 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:47,181 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,182 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,183 INFO  L85        PathProgramCache]: Analyzing trace with hash 911562087, now seen corresponding path program 1 times
[2025-04-28 21:21:47,183 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,183 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [402414055]
[2025-04-28 21:21:47,184 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,184 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,191 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:47,197 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:47,198 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,198 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,259 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:47,259 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,259 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [402414055]
[2025-04-28 21:21:47,259 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [402414055] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,260 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,260 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:47,260 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1161423516]
[2025-04-28 21:21:47,260 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,260 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:47,260 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,261 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:47,261 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:47,261 INFO  L87              Difference]: Start difference. First operand 171 states and 1266 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:47,555 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,555 INFO  L93              Difference]: Finished difference Result 179 states and 1538 transitions.
[2025-04-28 21:21:47,556 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:47,556 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:21:47,556 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,585 INFO  L225             Difference]: With dead ends: 179
[2025-04-28 21:21:47,585 INFO  L226             Difference]: Without dead ends: 179
[2025-04-28 21:21:47,586 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:47,586 INFO  L437           NwaCegarLoop]: 106 mSDtfsCounter, 6 mSDsluCounter, 117 mSDsCounter, 0 mSdLazyCounter, 142 mSolverCounterSat, 19 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 223 SdHoareTripleChecker+Invalid, 161 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 19 IncrementalHoareTripleChecker+Valid, 142 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,587 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 223 Invalid, 161 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [19 Valid, 142 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:47,588 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 179 states.
[2025-04-28 21:21:47,724 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 179 to 171.
[2025-04-28 21:21:47,726 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 171 states, 26 states have (on average 4.3076923076923075) internal successors, (112), 88 states have internal predecessors, (112), 136 states have call successors, (136), 10 states have call predecessors, (136), 16 states have return successors, (1012), 73 states have call predecessors, (1012), 136 states have call successors, (1012)
[2025-04-28 21:21:47,738 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 171 states to 171 states and 1260 transitions.
[2025-04-28 21:21:47,738 INFO  L79                 Accepts]: Start accepts. Automaton has 171 states and 1260 transitions. Word has length 16
[2025-04-28 21:21:47,738 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,738 INFO  L485      AbstractCegarLoop]: Abstraction has 171 states and 1260 transitions.
[2025-04-28 21:21:47,738 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:47,739 INFO  L278                IsEmpty]: Start isEmpty. Operand 171 states and 1260 transitions.
[2025-04-28 21:21:47,755 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:47,755 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,755 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,756 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:47,756 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,756 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,756 INFO  L85        PathProgramCache]: Analyzing trace with hash 153974509, now seen corresponding path program 1 times
[2025-04-28 21:21:47,757 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,757 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [860481584]
[2025-04-28 21:21:47,757 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,757 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,767 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:47,771 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:47,773 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,773 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,858 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:47,858 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,858 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [860481584]
[2025-04-28 21:21:47,859 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [860481584] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,859 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [610177503]
[2025-04-28 21:21:47,859 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,861 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,865 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,868 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:47,873 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,917 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:47,936 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:47,936 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,936 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,939 INFO  L256         TraceCheckSpWp]: Trace formula consists of 98 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,940 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,969 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:47,972 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,215 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:48,215 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [610177503] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,215 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,215 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-04-28 21:21:48,216 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [183769375]
[2025-04-28 21:21:48,216 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,216 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:48,216 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,216 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:48,217 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:48,217 INFO  L87              Difference]: Start difference. First operand 171 states and 1260 transitions. Second operand  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:49,705 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,705 INFO  L93              Difference]: Finished difference Result 207 states and 1766 transitions.
[2025-04-28 21:21:49,706 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:49,706 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6) Word has length 19
[2025-04-28 21:21:49,706 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,744 INFO  L225             Difference]: With dead ends: 207
[2025-04-28 21:21:49,744 INFO  L226             Difference]: Without dead ends: 207
[2025-04-28 21:21:49,744 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 47 GetRequests, 36 SyntacticMatches, 2 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=36, Invalid=74, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:49,745 INFO  L437           NwaCegarLoop]: 116 mSDtfsCounter, 30 mSDsluCounter, 136 mSDsCounter, 0 mSdLazyCounter, 634 mSolverCounterSat, 183 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 135 SdHoareTripleChecker+Valid, 252 SdHoareTripleChecker+Invalid, 817 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 183 IncrementalHoareTripleChecker+Valid, 634 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,745 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [135 Valid, 252 Invalid, 817 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [183 Valid, 634 Invalid, 0 Unknown, 0 Unchecked, 1.4s Time]
[2025-04-28 21:21:49,746 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 207 states.
[2025-04-28 21:21:49,902 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 207 to 189.
[2025-04-28 21:21:49,904 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 189 states, 35 states have (on average 3.4571428571428573) internal successors, (121), 97 states have internal predecessors, (121), 136 states have call successors, (136), 10 states have call predecessors, (136), 25 states have return successors, (952), 82 states have call predecessors, (952), 136 states have call successors, (952)
[2025-04-28 21:21:49,916 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 189 states to 189 states and 1209 transitions.
[2025-04-28 21:21:49,916 INFO  L79                 Accepts]: Start accepts. Automaton has 189 states and 1209 transitions. Word has length 19
[2025-04-28 21:21:49,916 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,916 INFO  L485      AbstractCegarLoop]: Abstraction has 189 states and 1209 transitions.
[2025-04-28 21:21:49,916 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:49,916 INFO  L278                IsEmpty]: Start isEmpty. Operand 189 states and 1209 transitions.
[2025-04-28 21:21:49,929 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:49,929 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,929 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,935 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:50,133 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,134 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,135 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,135 INFO  L85        PathProgramCache]: Analyzing trace with hash -1845094754, now seen corresponding path program 1 times
[2025-04-28 21:21:50,135 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,135 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [503193280]
[2025-04-28 21:21:50,135 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,135 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,141 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:50,144 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:50,145 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,145 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,192 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:50,192 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,192 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [503193280]
[2025-04-28 21:21:50,193 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [503193280] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,193 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,193 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,193 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1780866539]
[2025-04-28 21:21:50,193 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,193 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,193 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,194 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,195 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,196 INFO  L87              Difference]: Start difference. First operand 189 states and 1209 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:50,461 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,462 INFO  L93              Difference]: Finished difference Result 227 states and 1709 transitions.
[2025-04-28 21:21:50,462 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:50,462 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:50,463 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,486 INFO  L225             Difference]: With dead ends: 227
[2025-04-28 21:21:50,486 INFO  L226             Difference]: Without dead ends: 227
[2025-04-28 21:21:50,487 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:50,488 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 6 mSDsluCounter, 92 mSDsCounter, 0 mSdLazyCounter, 148 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 182 SdHoareTripleChecker+Invalid, 176 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 148 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,488 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 182 Invalid, 176 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 148 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:50,490 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 227 states.
[2025-04-28 21:21:50,612 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 227 to 225.
[2025-04-28 21:21:50,614 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 225 states, 41 states have (on average 3.6097560975609757) internal successors, (148), 111 states have internal predecessors, (148), 164 states have call successors, (164), 12 states have call predecessors, (164), 29 states have return successors, (1395), 102 states have call predecessors, (1395), 164 states have call successors, (1395)
[2025-04-28 21:21:50,629 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 225 states to 225 states and 1707 transitions.
[2025-04-28 21:21:50,629 INFO  L79                 Accepts]: Start accepts. Automaton has 225 states and 1707 transitions. Word has length 20
[2025-04-28 21:21:50,630 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,630 INFO  L485      AbstractCegarLoop]: Abstraction has 225 states and 1707 transitions.
[2025-04-28 21:21:50,630 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:50,630 INFO  L278                IsEmpty]: Start isEmpty. Operand 225 states and 1707 transitions.
[2025-04-28 21:21:50,643 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:50,644 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,644 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,644 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:50,644 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,645 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,645 INFO  L85        PathProgramCache]: Analyzing trace with hash -2072434117, now seen corresponding path program 1 times
[2025-04-28 21:21:50,645 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,645 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [116184389]
[2025-04-28 21:21:50,645 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,645 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,653 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:50,655 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:50,657 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,658 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,727 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:50,727 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,728 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [116184389]
[2025-04-28 21:21:50,728 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [116184389] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,728 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,728 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,728 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2060253452]
[2025-04-28 21:21:50,729 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,729 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,729 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,729 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,729 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,730 INFO  L87              Difference]: Start difference. First operand 225 states and 1707 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:51,175 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,176 INFO  L93              Difference]: Finished difference Result 313 states and 3226 transitions.
[2025-04-28 21:21:51,176 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:51,177 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:51,177 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,227 INFO  L225             Difference]: With dead ends: 313
[2025-04-28 21:21:51,227 INFO  L226             Difference]: Without dead ends: 313
[2025-04-28 21:21:51,227 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:51,228 INFO  L437           NwaCegarLoop]: 97 mSDtfsCounter, 6 mSDsluCounter, 98 mSDsCounter, 0 mSdLazyCounter, 230 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 195 SdHoareTripleChecker+Invalid, 264 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 230 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,228 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 195 Invalid, 264 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 230 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:51,230 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 313 states.
[2025-04-28 21:21:51,514 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 313 to 305.
[2025-04-28 21:21:51,518 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 305 states, 57 states have (on average 3.0701754385964914) internal successors, (175), 143 states have internal predecessors, (175), 220 states have call successors, (220), 16 states have call predecessors, (220), 41 states have return successors, (2450), 146 states have call predecessors, (2450), 220 states have call successors, (2450)
[2025-04-28 21:21:51,595 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 305 states to 305 states and 2845 transitions.
[2025-04-28 21:21:51,595 INFO  L79                 Accepts]: Start accepts. Automaton has 305 states and 2845 transitions. Word has length 20
[2025-04-28 21:21:51,596 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,596 INFO  L485      AbstractCegarLoop]: Abstraction has 305 states and 2845 transitions.
[2025-04-28 21:21:51,596 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:51,596 INFO  L278                IsEmpty]: Start isEmpty. Operand 305 states and 2845 transitions.
[2025-04-28 21:21:51,610 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:51,611 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,611 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,611 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:51,611 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,612 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,612 INFO  L85        PathProgramCache]: Analyzing trace with hash 1015143374, now seen corresponding path program 1 times
[2025-04-28 21:21:51,612 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,612 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [560504999]
[2025-04-28 21:21:51,612 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,612 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,617 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:51,620 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:51,620 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,620 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,668 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:51,668 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,668 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [560504999]
[2025-04-28 21:21:51,669 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [560504999] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,669 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,669 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:51,669 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [244752689]
[2025-04-28 21:21:51,669 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,669 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:51,669 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,670 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:51,670 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:51,670 INFO  L87              Difference]: Start difference. First operand 305 states and 2845 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:52,046 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,046 INFO  L93              Difference]: Finished difference Result 317 states and 3369 transitions.
[2025-04-28 21:21:52,046 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:52,047 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:52,047 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,095 INFO  L225             Difference]: With dead ends: 317
[2025-04-28 21:21:52,095 INFO  L226             Difference]: Without dead ends: 317
[2025-04-28 21:21:52,096 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:52,096 INFO  L437           NwaCegarLoop]: 105 mSDtfsCounter, 6 mSDsluCounter, 110 mSDsCounter, 0 mSdLazyCounter, 212 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 215 SdHoareTripleChecker+Invalid, 238 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 212 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,096 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 215 Invalid, 238 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 212 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:52,097 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 317 states.
[2025-04-28 21:21:52,342 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 317 to 305.
[2025-04-28 21:21:52,345 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 305 states, 57 states have (on average 3.0701754385964914) internal successors, (175), 143 states have internal predecessors, (175), 220 states have call successors, (220), 16 states have call predecessors, (220), 41 states have return successors, (2432), 146 states have call predecessors, (2432), 220 states have call successors, (2432)
[2025-04-28 21:21:52,374 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 305 states to 305 states and 2827 transitions.
[2025-04-28 21:21:52,374 INFO  L79                 Accepts]: Start accepts. Automaton has 305 states and 2827 transitions. Word has length 20
[2025-04-28 21:21:52,374 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,375 INFO  L485      AbstractCegarLoop]: Abstraction has 305 states and 2827 transitions.
[2025-04-28 21:21:52,375 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:52,375 INFO  L278                IsEmpty]: Start isEmpty. Operand 305 states and 2827 transitions.
[2025-04-28 21:21:52,392 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:52,392 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,392 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,392 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:52,393 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,393 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,393 INFO  L85        PathProgramCache]: Analyzing trace with hash 2043951889, now seen corresponding path program 1 times
[2025-04-28 21:21:52,393 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,394 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [180011188]
[2025-04-28 21:21:52,394 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,394 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,398 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:52,400 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:52,401 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,401 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,436 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:52,436 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,436 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [180011188]
[2025-04-28 21:21:52,436 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [180011188] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,436 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,436 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:52,436 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1198175568]
[2025-04-28 21:21:52,436 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,437 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:52,437 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,437 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:52,437 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:52,437 INFO  L87              Difference]: Start difference. First operand 305 states and 2827 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:52,850 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,851 INFO  L93              Difference]: Finished difference Result 379 states and 4268 transitions.
[2025-04-28 21:21:52,851 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:52,851 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:52,852 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,924 INFO  L225             Difference]: With dead ends: 379
[2025-04-28 21:21:52,924 INFO  L226             Difference]: Without dead ends: 379
[2025-04-28 21:21:52,925 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:52,925 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 7 mSDsluCounter, 94 mSDsCounter, 0 mSdLazyCounter, 94 mSolverCounterSat, 71 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 44 SdHoareTripleChecker+Valid, 203 SdHoareTripleChecker+Invalid, 165 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 71 IncrementalHoareTripleChecker+Valid, 94 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,925 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [44 Valid, 203 Invalid, 165 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [71 Valid, 94 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:52,926 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 379 states.
[2025-04-28 21:21:53,256 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 379 to 365.
[2025-04-28 21:21:53,260 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 365 states, 75 states have (on average 2.7066666666666666) internal successors, (203), 169 states have internal predecessors, (203), 248 states have call successors, (248), 18 states have call predecessors, (248), 57 states have return successors, (3164), 178 states have call predecessors, (3164), 248 states have call successors, (3164)
[2025-04-28 21:21:53,299 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 365 states to 365 states and 3615 transitions.
[2025-04-28 21:21:53,300 INFO  L79                 Accepts]: Start accepts. Automaton has 365 states and 3615 transitions. Word has length 20
[2025-04-28 21:21:53,300 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,301 INFO  L485      AbstractCegarLoop]: Abstraction has 365 states and 3615 transitions.
[2025-04-28 21:21:53,301 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:53,301 INFO  L278                IsEmpty]: Start isEmpty. Operand 365 states and 3615 transitions.
[2025-04-28 21:21:53,325 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:53,326 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,326 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,326 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:53,326 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,327 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,327 INFO  L85        PathProgramCache]: Analyzing trace with hash -1696903296, now seen corresponding path program 1 times
[2025-04-28 21:21:53,327 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,327 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [687597116]
[2025-04-28 21:21:53,327 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,327 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,341 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:53,343 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:53,343 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,343 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,387 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:53,387 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,387 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [687597116]
[2025-04-28 21:21:53,387 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [687597116] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,387 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,387 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:53,389 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [59829400]
[2025-04-28 21:21:53,389 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,389 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:53,389 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,390 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:53,390 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:53,390 INFO  L87              Difference]: Start difference. First operand 365 states and 3615 transitions. Second operand  has 4 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 4 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:53,831 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,831 INFO  L93              Difference]: Finished difference Result 421 states and 4917 transitions.
[2025-04-28 21:21:53,832 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:53,832 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 4 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:53,832 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,910 INFO  L225             Difference]: With dead ends: 421
[2025-04-28 21:21:53,910 INFO  L226             Difference]: Without dead ends: 421
[2025-04-28 21:21:53,910 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:53,912 INFO  L437           NwaCegarLoop]: 99 mSDtfsCounter, 6 mSDsluCounter, 90 mSDsCounter, 0 mSdLazyCounter, 225 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 189 SdHoareTripleChecker+Invalid, 259 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 225 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,913 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 189 Invalid, 259 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 225 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:53,914 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 421 states.
[2025-04-28 21:21:54,250 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 421 to 409.
[2025-04-28 21:21:54,253 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 409 states, 85 states have (on average 2.588235294117647) internal successors, (220), 187 states have internal predecessors, (220), 276 states have call successors, (276), 20 states have call predecessors, (276), 65 states have return successors, (3811), 202 states have call predecessors, (3811), 276 states have call successors, (3811)
[2025-04-28 21:21:54,325 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 409 states to 409 states and 4307 transitions.
[2025-04-28 21:21:54,326 INFO  L79                 Accepts]: Start accepts. Automaton has 409 states and 4307 transitions. Word has length 24
[2025-04-28 21:21:54,326 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,326 INFO  L485      AbstractCegarLoop]: Abstraction has 409 states and 4307 transitions.
[2025-04-28 21:21:54,326 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 4 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:54,326 INFO  L278                IsEmpty]: Start isEmpty. Operand 409 states and 4307 transitions.
[2025-04-28 21:21:54,354 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:54,356 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,356 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,356 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:54,356 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,357 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,357 INFO  L85        PathProgramCache]: Analyzing trace with hash -1530490640, now seen corresponding path program 1 times
[2025-04-28 21:21:54,357 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,357 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1647856364]
[2025-04-28 21:21:54,357 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,357 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,363 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:54,366 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:54,366 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,366 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,414 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:54,414 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,414 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1647856364]
[2025-04-28 21:21:54,414 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1647856364] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,414 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,414 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:54,415 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1440465908]
[2025-04-28 21:21:54,415 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,415 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:54,415 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,415 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:54,415 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:54,416 INFO  L87              Difference]: Start difference. First operand 409 states and 4307 transitions. Second operand  has 4 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 4 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:54,894 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,894 INFO  L93              Difference]: Finished difference Result 469 states and 5990 transitions.
[2025-04-28 21:21:54,895 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:54,895 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 4 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:54,895 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,011 INFO  L225             Difference]: With dead ends: 469
[2025-04-28 21:21:55,011 INFO  L226             Difference]: Without dead ends: 469
[2025-04-28 21:21:55,011 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:55,012 INFO  L437           NwaCegarLoop]: 101 mSDtfsCounter, 6 mSDsluCounter, 91 mSDsCounter, 0 mSdLazyCounter, 210 mSolverCounterSat, 32 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 192 SdHoareTripleChecker+Invalid, 242 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 32 IncrementalHoareTripleChecker+Valid, 210 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,012 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 192 Invalid, 242 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [32 Valid, 210 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:55,013 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 469 states.
[2025-04-28 21:21:55,481 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 469 to 453.
[2025-04-28 21:21:55,486 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 453 states, 95 states have (on average 2.526315789473684) internal successors, (240), 205 states have internal predecessors, (240), 304 states have call successors, (304), 22 states have call predecessors, (304), 73 states have return successors, (4579), 226 states have call predecessors, (4579), 304 states have call successors, (4579)
[2025-04-28 21:21:55,534 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 453 states to 453 states and 5123 transitions.
[2025-04-28 21:21:55,534 INFO  L79                 Accepts]: Start accepts. Automaton has 453 states and 5123 transitions. Word has length 24
[2025-04-28 21:21:55,534 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,534 INFO  L485      AbstractCegarLoop]: Abstraction has 453 states and 5123 transitions.
[2025-04-28 21:21:55,534 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 4 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:55,534 INFO  L278                IsEmpty]: Start isEmpty. Operand 453 states and 5123 transitions.
[2025-04-28 21:21:55,559 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 23
[2025-04-28 21:21:55,559 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,559 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,559 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:21:55,560 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,561 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,561 INFO  L85        PathProgramCache]: Analyzing trace with hash -1936866231, now seen corresponding path program 1 times
[2025-04-28 21:21:55,562 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,562 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [926035220]
[2025-04-28 21:21:55,562 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,562 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,567 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 22 statements into 1 equivalence classes.
[2025-04-28 21:21:55,573 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 22 of 22 statements.
[2025-04-28 21:21:55,573 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,573 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,615 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:55,615 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,615 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [926035220]
[2025-04-28 21:21:55,615 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [926035220] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,616 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,616 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:55,616 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1649213891]
[2025-04-28 21:21:55,616 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,616 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:55,616 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,616 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:55,616 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:55,617 INFO  L87              Difference]: Start difference. First operand 453 states and 5123 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:56,403 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,403 INFO  L93              Difference]: Finished difference Result 985 states and 24519 transitions.
[2025-04-28 21:21:56,404 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:56,404 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5) Word has length 22
[2025-04-28 21:21:56,404 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,792 INFO  L225             Difference]: With dead ends: 985
[2025-04-28 21:21:56,792 INFO  L226             Difference]: Without dead ends: 985
[2025-04-28 21:21:56,792 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:56,793 INFO  L437           NwaCegarLoop]: 119 mSDtfsCounter, 17 mSDsluCounter, 122 mSDsCounter, 0 mSdLazyCounter, 236 mSolverCounterSat, 52 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 27 SdHoareTripleChecker+Valid, 241 SdHoareTripleChecker+Invalid, 288 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 52 IncrementalHoareTripleChecker+Valid, 236 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,793 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [27 Valid, 241 Invalid, 288 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [52 Valid, 236 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:56,795 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 985 states.
[2025-04-28 21:21:58,486 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 985 to 833.
[2025-04-28 21:21:58,496 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 833 states, 186 states have (on average 2.1989247311827955) internal successors, (409), 342 states have internal predecessors, (409), 542 states have call successors, (542), 42 states have call predecessors, (542), 144 states have return successors, (12214), 449 states have call predecessors, (12214), 542 states have call successors, (12214)
[2025-04-28 21:21:58,679 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 833 states to 833 states and 13165 transitions.
[2025-04-28 21:21:58,679 INFO  L79                 Accepts]: Start accepts. Automaton has 833 states and 13165 transitions. Word has length 22
[2025-04-28 21:21:58,679 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,679 INFO  L485      AbstractCegarLoop]: Abstraction has 833 states and 13165 transitions.
[2025-04-28 21:21:58,680 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:58,680 INFO  L278                IsEmpty]: Start isEmpty. Operand 833 states and 13165 transitions.
[2025-04-28 21:21:58,708 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 23
[2025-04-28 21:21:58,708 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,709 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,709 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:21:58,709 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,709 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,710 INFO  L85        PathProgramCache]: Analyzing trace with hash -317984900, now seen corresponding path program 1 times
[2025-04-28 21:21:58,710 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,710 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1818034450]
[2025-04-28 21:21:58,710 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,710 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,714 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 22 statements into 1 equivalence classes.
[2025-04-28 21:21:58,717 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 22 of 22 statements.
[2025-04-28 21:21:58,718 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,718 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,759 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:58,759 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,759 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1818034450]
[2025-04-28 21:21:58,759 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1818034450] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:58,760 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:58,760 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:58,760 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [72370057]
[2025-04-28 21:21:58,760 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,760 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:58,760 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,760 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:58,761 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:58,761 INFO  L87              Difference]: Start difference. First operand 833 states and 13165 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:59,338 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,339 INFO  L93              Difference]: Finished difference Result 985 states and 24159 transitions.
[2025-04-28 21:21:59,339 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:59,339 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5) Word has length 22
[2025-04-28 21:21:59,340 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,725 INFO  L225             Difference]: With dead ends: 985
[2025-04-28 21:21:59,725 INFO  L226             Difference]: Without dead ends: 985
[2025-04-28 21:21:59,726 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:59,726 INFO  L437           NwaCegarLoop]: 116 mSDtfsCounter, 6 mSDsluCounter, 154 mSDsCounter, 0 mSdLazyCounter, 130 mSolverCounterSat, 17 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 270 SdHoareTripleChecker+Invalid, 147 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 17 IncrementalHoareTripleChecker+Valid, 130 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,726 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 270 Invalid, 147 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [17 Valid, 130 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:59,728 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 985 states.
[2025-04-28 21:22:01,109 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 985 to 833.
[2025-04-28 21:22:01,128 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 833 states, 186 states have (on average 2.1989247311827955) internal successors, (409), 342 states have internal predecessors, (409), 542 states have call successors, (542), 42 states have call predecessors, (542), 144 states have return successors, (12034), 449 states have call predecessors, (12034), 542 states have call successors, (12034)
[2025-04-28 21:22:01,310 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 833 states to 833 states and 12985 transitions.
[2025-04-28 21:22:01,310 INFO  L79                 Accepts]: Start accepts. Automaton has 833 states and 12985 transitions. Word has length 22
[2025-04-28 21:22:01,310 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,310 INFO  L485      AbstractCegarLoop]: Abstraction has 833 states and 12985 transitions.
[2025-04-28 21:22:01,310 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:22:01,310 INFO  L278                IsEmpty]: Start isEmpty. Operand 833 states and 12985 transitions.
[2025-04-28 21:22:01,359 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:22:01,359 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,359 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,360 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:22:01,360 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,360 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,360 INFO  L85        PathProgramCache]: Analyzing trace with hash -1224664771, now seen corresponding path program 1 times
[2025-04-28 21:22:01,361 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,361 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1789475606]
[2025-04-28 21:22:01,361 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,361 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,369 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:22:01,376 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:01,376 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,376 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,444 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:01,445 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,445 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1789475606]
[2025-04-28 21:22:01,445 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1789475606] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:01,445 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [827919102]
[2025-04-28 21:22:01,445 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,445 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,448 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:01,451 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:01,454 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:22:01,497 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:22:01,521 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:01,521 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,521 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,522 INFO  L256         TraceCheckSpWp]: Trace formula consists of 149 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:01,524 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:01,556 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:01,560 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,952 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:01,953 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [827919102] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,953 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,953 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-04-28 21:22:01,953 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1316272809]
[2025-04-28 21:22:01,953 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,954 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:01,954 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,954 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:01,954 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:01,954 INFO  L87              Difference]: Start difference. First operand 833 states and 12985 transitions. Second operand  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:22:03,656 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,657 INFO  L93              Difference]: Finished difference Result 1554 states and 36553 transitions.
[2025-04-28 21:22:03,657 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:22:03,657 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8) Word has length 25
[2025-04-28 21:22:03,657 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,496 INFO  L225             Difference]: With dead ends: 1554
[2025-04-28 21:22:04,496 INFO  L226             Difference]: Without dead ends: 1554
[2025-04-28 21:22:04,496 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 57 GetRequests, 49 SyntacticMatches, 3 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:22:04,497 INFO  L437           NwaCegarLoop]: 144 mSDtfsCounter, 26 mSDsluCounter, 303 mSDsCounter, 0 mSdLazyCounter, 741 mSolverCounterSat, 77 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 38 SdHoareTripleChecker+Valid, 447 SdHoareTripleChecker+Invalid, 818 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 77 IncrementalHoareTripleChecker+Valid, 741 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,497 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [38 Valid, 447 Invalid, 818 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [77 Valid, 741 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:22:04,499 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1554 states.
[2025-04-28 21:22:06,501 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1554 to 1552.
[2025-04-28 21:22:06,538 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1552 states, 352 states have (on average 1.8465909090909092) internal successors, (650), 575 states have internal predecessors, (650), 961 states have call successors, (961), 58 states have call predecessors, (961), 294 states have return successors, (34940), 919 states have call predecessors, (34940), 961 states have call successors, (34940)
[2025-04-28 21:22:07,237 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1552 states to 1552 states and 36551 transitions.
[2025-04-28 21:22:07,238 INFO  L79                 Accepts]: Start accepts. Automaton has 1552 states and 36551 transitions. Word has length 25
[2025-04-28 21:22:07,238 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,238 INFO  L485      AbstractCegarLoop]: Abstraction has 1552 states and 36551 transitions.
[2025-04-28 21:22:07,239 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:22:07,239 INFO  L278                IsEmpty]: Start isEmpty. Operand 1552 states and 36551 transitions.
[2025-04-28 21:22:07,306 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 27
[2025-04-28 21:22:07,307 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,307 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:07,312 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:07,511 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,511 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,512 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,512 INFO  L85        PathProgramCache]: Analyzing trace with hash -700935470, now seen corresponding path program 1 times
[2025-04-28 21:22:07,513 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,513 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1254998659]
[2025-04-28 21:22:07,513 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,513 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,517 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:22:07,520 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:22:07,521 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,521 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,562 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:07,562 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,563 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1254998659]
[2025-04-28 21:22:07,563 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1254998659] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,563 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [300598801]
[2025-04-28 21:22:07,563 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,563 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,565 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:07,567 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:22:07,574 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,609 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:22:07,631 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:22:07,631 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,631 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,634 INFO  L256         TraceCheckSpWp]: Trace formula consists of 155 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,635 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:07,662 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:07,662 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:08,003 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:08,004 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [300598801] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,004 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,004 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 5
[2025-04-28 21:22:08,004 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2006308712]
[2025-04-28 21:22:08,004 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,005 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:08,005 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,005 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:08,005 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:08,005 INFO  L87              Difference]: Start difference. First operand 1552 states and 36551 transitions. Second operand  has 5 states, 4 states have (on average 2.5) internal successors, (10), 5 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 4 states have call predecessors, (7), 3 states have call successors, (7)
