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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:32,210 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:32,272 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4df6a42c-277e-470c-ba40-1356a717fb82/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:32,276 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:32,277 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:32,300 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:32,300 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:32,300 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:32,301 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:32,301 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:32,301 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:32,301 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:32,301 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:32,301 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:32,302 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:32,302 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:32,302 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:32,302 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:32,302 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:32,302 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:32,303 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:32,303 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:32,303 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:32,303 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:32,303 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:32,304 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:32,304 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:32,640 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:32,653 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:32,656 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:32,660 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:32,660 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:32,661 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4df6a42c-277e-470c-ba40-1356a717fb82/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-153.smt2
[2025-04-28 21:21:32,664 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:32,671 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:33,020 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4df6a42c-277e-470c-ba40-1356a717fb82/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-153.smt2
[2025-04-28 21:21:33,028 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:33,029 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:33,030 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:33,030 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:33,030 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:33,033 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,065 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33 Unit
[2025-04-28 21:21:33,065 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:33,066 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:33,066 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:33,067 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:33,082 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,082 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,110 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,110 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,125 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,126 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,131 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,133 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,138 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,168 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:33,172 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:33,172 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:33,173 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:33,175 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (1/1) ...
[2025-04-28 21:21:33,178 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:33,195 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,210 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:33,215 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:33,236 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:33,237 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:33,237 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:33,237 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:33,238 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:33,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:33,238 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_0 given in one single declaration
[2025-04-28 21:21:33,238 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_0
[2025-04-28 21:21:33,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_0
[2025-04-28 21:21:33,239 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:33,239 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:33,239 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:33,330 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:33,333 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:33,749 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:33,749 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:33,774 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:33,777 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:33,777 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:33 BoogieIcfgContainer
[2025-04-28 21:21:33,777 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:33,780 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:33,782 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:33,788 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:33,788 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:33" (1/3) ...
[2025-04-28 21:21:33,789 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2459ba83 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:33, skipping insertion in model container
[2025-04-28 21:21:33,789 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:33" (2/3) ...
[2025-04-28 21:21:33,789 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2459ba83 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:33, skipping insertion in model container
[2025-04-28 21:21:33,789 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:33" (3/3) ...
[2025-04-28 21:21:33,791 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:33,809 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:33,812 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 44 locations, 115 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:33,878 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:33,892 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;@3fc3a999, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:33,892 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:33,897 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 44 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 19 states have internal predecessors, (19), 32 states have call successors, (32), 3 states have call predecessors, (32), 3 states have return successors, (32), 22 states have call predecessors, (32), 32 states have call successors, (32)
[2025-04-28 21:21:33,916 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:33,917 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,917 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,918 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,923 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,924 INFO  L85        PathProgramCache]: Analyzing trace with hash -1152244794, now seen corresponding path program 1 times
[2025-04-28 21:21:33,932 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,933 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1648091739]
[2025-04-28 21:21:33,933 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,934 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,962 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:33,980 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:33,980 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,980 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,091 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:34,092 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,092 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1648091739]
[2025-04-28 21:21:34,093 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1648091739] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:34,093 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:34,096 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:34,098 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1662020771]
[2025-04-28 21:21:34,098 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,102 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:34,102 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,132 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:34,132 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:34,135 INFO  L87              Difference]: Start difference. First operand  has 44 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 19 states have internal predecessors, (19), 32 states have call successors, (32), 3 states have call predecessors, (32), 3 states have return successors, (32), 22 states have call predecessors, (32), 32 states have call successors, (32) 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:34,504 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,508 INFO  L93              Difference]: Finished difference Result 46 states and 113 transitions.
[2025-04-28 21:21:34,509 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:34,511 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:34,511 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,527 INFO  L225             Difference]: With dead ends: 46
[2025-04-28 21:21:34,529 INFO  L226             Difference]: Without dead ends: 46
[2025-04-28 21:21:34,531 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:34,535 INFO  L437           NwaCegarLoop]: 52 mSDtfsCounter, 1 mSDsluCounter, 60 mSDsCounter, 0 mSdLazyCounter, 128 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 112 SdHoareTripleChecker+Invalid, 128 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 128 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,536 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 112 Invalid, 128 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 128 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:34,552 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 46 states.
[2025-04-28 21:21:34,624 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 46 to 44.
[2025-04-28 21:21:34,626 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 44 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 18 states have internal predecessors, (18), 32 states have call successors, (32), 3 states have call predecessors, (32), 4 states have return successors, (61), 22 states have call predecessors, (61), 32 states have call successors, (61)
[2025-04-28 21:21:34,632 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 44 states to 44 states and 111 transitions.
[2025-04-28 21:21:34,637 INFO  L79                 Accepts]: Start accepts. Automaton has 44 states and 111 transitions. Word has length 12
[2025-04-28 21:21:34,637 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,637 INFO  L485      AbstractCegarLoop]: Abstraction has 44 states and 111 transitions.
[2025-04-28 21:21:34,638 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:34,638 INFO  L278                IsEmpty]: Start isEmpty. Operand 44 states and 111 transitions.
[2025-04-28 21:21:34,653 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:34,654 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,654 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:34,654 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:34,654 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,659 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,659 INFO  L85        PathProgramCache]: Analyzing trace with hash 2128626920, now seen corresponding path program 1 times
[2025-04-28 21:21:34,659 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,659 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [27651554]
[2025-04-28 21:21:34,659 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,659 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,669 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:34,748 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:34,748 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,749 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,917 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:34,917 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,917 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [27651554]
[2025-04-28 21:21:34,917 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [27651554] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:34,917 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:34,917 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:34,917 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1984839709]
[2025-04-28 21:21:34,918 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,919 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:34,919 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,926 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:34,926 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:34,926 INFO  L87              Difference]: Start difference. First operand 44 states and 111 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:35,278 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,279 INFO  L93              Difference]: Finished difference Result 48 states and 142 transitions.
[2025-04-28 21:21:35,279 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:35,280 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:35,280 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,283 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:35,284 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:35,284 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:35,285 INFO  L437           NwaCegarLoop]: 84 mSDtfsCounter, 1 mSDsluCounter, 108 mSDsCounter, 0 mSdLazyCounter, 119 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 192 SdHoareTripleChecker+Invalid, 123 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 119 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,285 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 192 Invalid, 123 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 119 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:35,286 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:35,327 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 46.
[2025-04-28 21:21:35,327 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 8 states have (on average 2.375) internal successors, (19), 19 states have internal predecessors, (19), 32 states have call successors, (32), 3 states have call predecessors, (32), 5 states have return successors, (89), 23 states have call predecessors, (89), 32 states have call successors, (89)
[2025-04-28 21:21:35,331 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 140 transitions.
[2025-04-28 21:21:35,331 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 140 transitions. Word has length 16
[2025-04-28 21:21:35,331 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,331 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 140 transitions.
[2025-04-28 21:21:35,332 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:35,332 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 140 transitions.
[2025-04-28 21:21:35,336 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:35,337 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,337 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,337 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:35,337 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,338 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,338 INFO  L85        PathProgramCache]: Analyzing trace with hash -1448355107, now seen corresponding path program 1 times
[2025-04-28 21:21:35,338 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,338 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1794048701]
[2025-04-28 21:21:35,338 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,339 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,345 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:35,350 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:35,350 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,350 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,397 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:35,398 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,398 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1794048701]
[2025-04-28 21:21:35,398 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1794048701] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:35,398 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [785218600]
[2025-04-28 21:21:35,398 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,398 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:35,401 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,403 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:35,409 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:35,468 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:35,488 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:35,488 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,488 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,490 INFO  L256         TraceCheckSpWp]: Trace formula consists of 89 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:35,494 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:35,559 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:35,561 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:35,561 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [785218600] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,561 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:35,561 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 5
[2025-04-28 21:21:35,561 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [439987961]
[2025-04-28 21:21:35,562 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,562 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:35,562 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,563 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:35,563 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:35,563 INFO  L87              Difference]: Start difference. First operand 46 states and 140 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), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:35,836 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,836 INFO  L93              Difference]: Finished difference Result 48 states and 141 transitions.
[2025-04-28 21:21:35,837 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:35,837 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), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:21:35,838 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,845 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:35,845 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:35,845 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 19 GetRequests, 16 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:35,846 INFO  L437           NwaCegarLoop]: 53 mSDtfsCounter, 1 mSDsluCounter, 62 mSDsCounter, 0 mSdLazyCounter, 121 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 115 SdHoareTripleChecker+Invalid, 122 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 121 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,846 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 115 Invalid, 122 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 121 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:35,847 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:35,881 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 46.
[2025-04-28 21:21:35,883 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 8 states have (on average 2.375) internal successors, (19), 19 states have internal predecessors, (19), 32 states have call successors, (32), 3 states have call predecessors, (32), 5 states have return successors, (88), 23 states have call predecessors, (88), 32 states have call successors, (88)
[2025-04-28 21:21:35,886 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 139 transitions.
[2025-04-28 21:21:35,886 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 139 transitions. Word has length 16
[2025-04-28 21:21:35,886 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,887 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 139 transitions.
[2025-04-28 21:21:35,887 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), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:35,887 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 139 transitions.
[2025-04-28 21:21:35,892 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:35,894 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,897 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,903 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:36,098 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:36,098 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,099 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,099 INFO  L85        PathProgramCache]: Analyzing trace with hash -671772265, now seen corresponding path program 1 times
[2025-04-28 21:21:36,099 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,099 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [576215726]
[2025-04-28 21:21:36,099 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,099 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,104 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:36,109 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:36,109 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,109 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,158 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:36,158 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,158 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [576215726]
[2025-04-28 21:21:36,158 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [576215726] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,158 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [652643679]
[2025-04-28 21:21:36,158 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,158 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,161 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,163 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:36,166 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,209 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:36,228 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:36,228 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,228 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,229 INFO  L256         TraceCheckSpWp]: Trace formula consists of 89 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,231 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,254 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:36,254 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:36,255 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [652643679] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,255 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:36,255 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 5
[2025-04-28 21:21:36,255 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2042757623]
[2025-04-28 21:21:36,255 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,255 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:36,255 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,256 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:36,256 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:36,256 INFO  L87              Difference]: Start difference. First operand 46 states and 139 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), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:36,492 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,493 INFO  L93              Difference]: Finished difference Result 48 states and 140 transitions.
[2025-04-28 21:21:36,493 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:36,493 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), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:21:36,493 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,495 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:36,496 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:36,496 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 19 GetRequests, 16 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:36,497 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 1 mSDsluCounter, 67 mSDsCounter, 0 mSdLazyCounter, 121 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 123 SdHoareTripleChecker+Invalid, 121 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 121 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,497 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 123 Invalid, 121 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 121 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:36,498 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:36,523 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 46.
[2025-04-28 21:21:36,523 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 8 states have (on average 2.375) internal successors, (19), 19 states have internal predecessors, (19), 32 states have call successors, (32), 3 states have call predecessors, (32), 5 states have return successors, (87), 23 states have call predecessors, (87), 32 states have call successors, (87)
[2025-04-28 21:21:36,525 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 138 transitions.
[2025-04-28 21:21:36,526 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 138 transitions. Word has length 16
[2025-04-28 21:21:36,527 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,527 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 138 transitions.
[2025-04-28 21:21:36,527 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), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:36,527 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 138 transitions.
[2025-04-28 21:21:36,531 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:36,531 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,532 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,537 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:36,732 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,733 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,733 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,733 INFO  L85        PathProgramCache]: Analyzing trace with hash -495438209, now seen corresponding path program 1 times
[2025-04-28 21:21:36,733 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,733 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1635526534]
[2025-04-28 21:21:36,733 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,734 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,740 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:36,743 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:36,744 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,744 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,814 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:36,814 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,814 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1635526534]
[2025-04-28 21:21:36,814 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1635526534] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,814 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1416239679]
[2025-04-28 21:21:36,815 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,815 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,823 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,826 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:36,829 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,882 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:36,914 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:36,915 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,915 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,916 INFO  L256         TraceCheckSpWp]: Trace formula consists of 133 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,918 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,957 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:36,957 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:36,957 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1416239679] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,957 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:36,957 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:21:36,958 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [764138029]
[2025-04-28 21:21:36,958 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,958 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:36,958 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,959 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:36,959 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:36,959 INFO  L87              Difference]: Start difference. First operand 46 states and 138 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, (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:37,208 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,209 INFO  L93              Difference]: Finished difference Result 48 states and 139 transitions.
[2025-04-28 21:21:37,209 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:37,209 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, (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:37,210 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,211 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:37,211 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:37,212 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 23 GetRequests, 19 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:37,213 INFO  L437           NwaCegarLoop]: 83 mSDtfsCounter, 1 mSDsluCounter, 109 mSDsCounter, 0 mSdLazyCounter, 119 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 192 SdHoareTripleChecker+Invalid, 121 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 119 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,213 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 192 Invalid, 121 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 119 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:37,214 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:37,229 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 46.
[2025-04-28 21:21:37,229 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 8 states have (on average 2.375) internal successors, (19), 19 states have internal predecessors, (19), 32 states have call successors, (32), 3 states have call predecessors, (32), 5 states have return successors, (86), 23 states have call predecessors, (86), 32 states have call successors, (86)
[2025-04-28 21:21:37,231 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 137 transitions.
[2025-04-28 21:21:37,231 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 137 transitions. Word has length 20
[2025-04-28 21:21:37,231 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,231 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 137 transitions.
[2025-04-28 21:21:37,232 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, (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:37,232 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 137 transitions.
[2025-04-28 21:21:37,235 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:37,235 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,235 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,241 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:37,439 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,439 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,440 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,440 INFO  L85        PathProgramCache]: Analyzing trace with hash 149003833, now seen corresponding path program 1 times
[2025-04-28 21:21:37,440 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,440 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1957956915]
[2025-04-28 21:21:37,440 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,440 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,447 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:37,450 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:37,451 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,451 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,541 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:37,542 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,542 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1957956915]
[2025-04-28 21:21:37,542 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1957956915] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,542 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [702588154]
[2025-04-28 21:21:37,542 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,542 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,545 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,547 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:37,550 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,597 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:37,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:37,620 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,620 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,623 INFO  L256         TraceCheckSpWp]: Trace formula consists of 133 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,625 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,660 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:37,663 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:37,663 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [702588154] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,663 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:37,663 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:21:37,663 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1597552726]
[2025-04-28 21:21:37,663 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,664 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:37,664 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,664 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:37,664 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:37,664 INFO  L87              Difference]: Start difference. First operand 46 states and 137 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, (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:37,866 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,866 INFO  L93              Difference]: Finished difference Result 48 states and 137 transitions.
[2025-04-28 21:21:37,867 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:37,867 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, (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:37,867 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,869 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:37,869 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:37,869 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 23 GetRequests, 19 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:37,872 INFO  L437           NwaCegarLoop]: 82 mSDtfsCounter, 1 mSDsluCounter, 106 mSDsCounter, 0 mSdLazyCounter, 112 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 188 SdHoareTripleChecker+Invalid, 116 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 112 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,872 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 188 Invalid, 116 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 112 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:37,873 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:37,889 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 46.
[2025-04-28 21:21:37,889 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 8 states have (on average 2.375) internal successors, (19), 19 states have internal predecessors, (19), 32 states have call successors, (32), 3 states have call predecessors, (32), 5 states have return successors, (84), 23 states have call predecessors, (84), 32 states have call successors, (84)
[2025-04-28 21:21:37,891 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 135 transitions.
[2025-04-28 21:21:37,891 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 135 transitions. Word has length 20
[2025-04-28 21:21:37,891 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,891 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 135 transitions.
[2025-04-28 21:21:37,892 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, (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:37,892 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 135 transitions.
[2025-04-28 21:21:37,895 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:37,895 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,896 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,901 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:38,096 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,096 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,097 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,097 INFO  L85        PathProgramCache]: Analyzing trace with hash 1255465908, now seen corresponding path program 1 times
[2025-04-28 21:21:38,097 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,097 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1395624751]
[2025-04-28 21:21:38,097 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,097 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,109 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:38,131 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:38,131 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,131 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,229 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:38,229 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,229 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1395624751]
[2025-04-28 21:21:38,230 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1395624751] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:38,230 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,230 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:38,230 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [668148578]
[2025-04-28 21:21:38,230 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,230 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:38,230 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,231 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:38,231 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:38,231 INFO  L87              Difference]: Start difference. First operand 46 states and 135 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, (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:38,447 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,447 INFO  L93              Difference]: Finished difference Result 52 states and 193 transitions.
[2025-04-28 21:21:38,448 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:38,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, (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:38,448 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,450 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:38,450 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:38,450 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:38,451 INFO  L437           NwaCegarLoop]: 82 mSDtfsCounter, 1 mSDsluCounter, 104 mSDsCounter, 0 mSdLazyCounter, 121 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 186 SdHoareTripleChecker+Invalid, 124 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 121 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,452 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 186 Invalid, 124 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 121 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:38,452 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:38,480 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 48.
[2025-04-28 21:21:38,481 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 20 states have internal predecessors, (20), 32 states have call successors, (32), 3 states have call predecessors, (32), 6 states have return successors, (113), 24 states have call predecessors, (113), 32 states have call successors, (113)
[2025-04-28 21:21:38,482 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 165 transitions.
[2025-04-28 21:21:38,482 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 165 transitions. Word has length 20
[2025-04-28 21:21:38,483 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,484 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 165 transitions.
[2025-04-28 21:21:38,484 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, (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:38,484 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 165 transitions.
[2025-04-28 21:21:38,488 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:38,488 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,488 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,488 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:38,488 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,489 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,489 INFO  L85        PathProgramCache]: Analyzing trace with hash 1112696965, now seen corresponding path program 1 times
[2025-04-28 21:21:38,489 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,489 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1189295739]
[2025-04-28 21:21:38,489 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,489 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,496 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:38,499 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:38,500 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,500 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,576 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:38,576 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,576 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1189295739]
[2025-04-28 21:21:38,576 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1189295739] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:38,576 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [874572092]
[2025-04-28 21:21:38,577 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,577 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,580 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:38,582 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:38,586 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:38,635 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:38,666 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:38,666 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,666 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,668 INFO  L256         TraceCheckSpWp]: Trace formula consists of 171 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:38,670 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:38,871 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 8 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:38,871 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:39,438 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 8 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:39,438 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [874572092] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:39,438 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:39,439 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [4, 8, 8] total 12
[2025-04-28 21:21:39,439 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [318941943]
[2025-04-28 21:21:39,439 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,439 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:39,439 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,440 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:39,440 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=106, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:39,440 INFO  L87              Difference]: Start difference. First operand 48 states and 165 transitions. Second operand  has 12 states, 6 states have (on average 3.0) internal successors, (18), 11 states have internal predecessors, (18), 9 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:40,565 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,565 INFO  L93              Difference]: Finished difference Result 55 states and 233 transitions.
[2025-04-28 21:21:40,565 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:40,566 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 3.0) internal successors, (18), 11 states have internal predecessors, (18), 9 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12) Word has length 24
[2025-04-28 21:21:40,566 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,568 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:40,568 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:40,569 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 37 SyntacticMatches, 4 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=42, Invalid=168, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:40,569 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 4 mSDsluCounter, 187 mSDsCounter, 0 mSdLazyCounter, 994 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 242 SdHoareTripleChecker+Invalid, 1003 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 994 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,570 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 242 Invalid, 1003 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 994 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:21:40,570 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:40,591 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 48.
[2025-04-28 21:21:40,591 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 20 states have internal predecessors, (20), 32 states have call successors, (32), 3 states have call predecessors, (32), 6 states have return successors, (112), 24 states have call predecessors, (112), 32 states have call successors, (112)
[2025-04-28 21:21:40,593 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 164 transitions.
[2025-04-28 21:21:40,593 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 164 transitions. Word has length 24
[2025-04-28 21:21:40,593 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,593 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 164 transitions.
[2025-04-28 21:21:40,593 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 3.0) internal successors, (18), 11 states have internal predecessors, (18), 9 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:40,593 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 164 transitions.
[2025-04-28 21:21:40,597 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:40,597 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,597 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,603 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:40,798 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,798 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,798 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,798 INFO  L85        PathProgramCache]: Analyzing trace with hash -1928736821, now seen corresponding path program 1 times
[2025-04-28 21:21:40,799 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,799 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1150004873]
[2025-04-28 21:21:40,799 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,799 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,805 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:40,807 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:40,808 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,808 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,853 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:40,853 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,853 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1150004873]
[2025-04-28 21:21:40,853 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1150004873] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,853 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1938148126]
[2025-04-28 21:21:40,853 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,853 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,856 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,858 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:40,864 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,913 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:40,943 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:40,943 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,943 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,947 INFO  L256         TraceCheckSpWp]: Trace formula consists of 171 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,949 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,057 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 8 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:41,057 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:41,571 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 8 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:41,571 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1938148126] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:41,571 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:41,571 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [4, 8, 8] total 12
[2025-04-28 21:21:41,571 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [924022626]
[2025-04-28 21:21:41,571 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,573 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:41,573 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,574 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:41,574 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=106, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:41,575 INFO  L87              Difference]: Start difference. First operand 48 states and 164 transitions. Second operand  has 12 states, 6 states have (on average 3.0) internal successors, (18), 11 states have internal predecessors, (18), 9 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:42,547 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,547 INFO  L93              Difference]: Finished difference Result 55 states and 232 transitions.
[2025-04-28 21:21:42,548 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:42,548 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 3.0) internal successors, (18), 11 states have internal predecessors, (18), 9 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12) Word has length 24
[2025-04-28 21:21:42,548 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,550 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:42,551 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:42,551 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 37 SyntacticMatches, 4 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=42, Invalid=168, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:42,552 INFO  L437           NwaCegarLoop]: 59 mSDtfsCounter, 4 mSDsluCounter, 283 mSDsCounter, 0 mSdLazyCounter, 888 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 342 SdHoareTripleChecker+Invalid, 898 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 888 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,552 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 342 Invalid, 898 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 888 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:42,552 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:42,568 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 48.
[2025-04-28 21:21:42,569 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 20 states have internal predecessors, (20), 32 states have call successors, (32), 3 states have call predecessors, (32), 6 states have return successors, (111), 24 states have call predecessors, (111), 32 states have call successors, (111)
[2025-04-28 21:21:42,570 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 163 transitions.
[2025-04-28 21:21:42,570 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 163 transitions. Word has length 24
[2025-04-28 21:21:42,570 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,571 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 163 transitions.
[2025-04-28 21:21:42,571 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 3.0) internal successors, (18), 11 states have internal predecessors, (18), 9 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:42,571 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 163 transitions.
[2025-04-28 21:21:42,574 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:42,575 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,575 INFO  L218           NwaCegarLoop]: trace histogram [7, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,581 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:42,779 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:21:42,780 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,780 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,780 INFO  L85        PathProgramCache]: Analyzing trace with hash 1150052389, now seen corresponding path program 1 times
[2025-04-28 21:21:42,780 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,780 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1136861998]
[2025-04-28 21:21:42,780 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,781 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,790 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:42,825 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:42,825 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,825 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,066 INFO  L134       CoverageAnalysis]: Checked inductivity of 66 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 42 trivial. 0 not checked.
[2025-04-28 21:21:43,067 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,067 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1136861998]
[2025-04-28 21:21:43,067 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1136861998] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,067 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2099423679]
[2025-04-28 21:21:43,067 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,068 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,073 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,075 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,078 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,137 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:43,188 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:43,189 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,189 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,190 INFO  L256         TraceCheckSpWp]: Trace formula consists of 303 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,192 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,261 INFO  L134       CoverageAnalysis]: Checked inductivity of 66 backedges. 32 proven. 2 refuted. 0 times theorem prover too weak. 32 trivial. 0 not checked.
[2025-04-28 21:21:43,263 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,780 INFO  L134       CoverageAnalysis]: Checked inductivity of 66 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 42 trivial. 0 not checked.
[2025-04-28 21:21:43,781 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2099423679] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,781 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,781 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:43,781 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1392534066]
[2025-04-28 21:21:43,781 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,782 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:43,782 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,782 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:43,782 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:43,783 INFO  L87              Difference]: Start difference. First operand 48 states and 163 transitions. Second operand  has 10 states, 5 states have (on average 4.0) internal successors, (20), 10 states have internal predecessors, (20), 7 states have call successors, (15), 2 states have call predecessors, (15), 5 states have return successors, (15), 4 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:21:44,601 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,602 INFO  L93              Difference]: Finished difference Result 54 states and 216 transitions.
[2025-04-28 21:21:44,602 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:44,602 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 4.0) internal successors, (20), 10 states have internal predecessors, (20), 7 states have call successors, (15), 2 states have call predecessors, (15), 5 states have return successors, (15), 4 states have call predecessors, (15), 7 states have call successors, (15) Word has length 36
[2025-04-28 21:21:44,602 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,605 INFO  L225             Difference]: With dead ends: 54
[2025-04-28 21:21:44,605 INFO  L226             Difference]: Without dead ends: 54
[2025-04-28 21:21:44,606 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 79 GetRequests, 66 SyntacticMatches, 3 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=34, Invalid=98, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:44,606 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 6 mSDsluCounter, 148 mSDsCounter, 0 mSdLazyCounter, 705 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 204 SdHoareTripleChecker+Invalid, 716 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 705 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,607 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 204 Invalid, 716 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 705 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:44,607 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-04-28 21:21:44,627 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 50.
[2025-04-28 21:21:44,627 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 10 states have (on average 2.1) internal successors, (21), 21 states have internal predecessors, (21), 32 states have call successors, (32), 3 states have call predecessors, (32), 7 states have return successors, (135), 25 states have call predecessors, (135), 32 states have call successors, (135)
[2025-04-28 21:21:44,631 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 188 transitions.
[2025-04-28 21:21:44,631 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 188 transitions. Word has length 36
[2025-04-28 21:21:44,631 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,631 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 188 transitions.
[2025-04-28 21:21:44,631 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 4.0) internal successors, (20), 10 states have internal predecessors, (20), 7 states have call successors, (15), 2 states have call predecessors, (15), 5 states have return successors, (15), 4 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:21:44,631 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 188 transitions.
[2025-04-28 21:21:44,636 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:44,636 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,636 INFO  L218           NwaCegarLoop]: trace histogram [11, 5, 3, 3, 3, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,642 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:44,837 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable10
[2025-04-28 21:21:44,837 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,837 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,838 INFO  L85        PathProgramCache]: Analyzing trace with hash 2048293063, now seen corresponding path program 1 times
[2025-04-28 21:21:44,838 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,838 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [389616561]
[2025-04-28 21:21:44,838 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,838 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,854 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:44,885 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:44,886 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,886 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,177 INFO  L134       CoverageAnalysis]: Checked inductivity of 174 backedges. 0 proven. 55 refuted. 0 times theorem prover too weak. 119 trivial. 0 not checked.
[2025-04-28 21:21:45,177 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,177 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [389616561]
[2025-04-28 21:21:45,178 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [389616561] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,178 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2122815487]
[2025-04-28 21:21:45,178 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,178 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,181 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,183 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:45,187 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,253 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:45,324 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:45,324 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,324 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,327 INFO  L256         TraceCheckSpWp]: Trace formula consists of 467 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,330 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:45,525 INFO  L134       CoverageAnalysis]: Checked inductivity of 174 backedges. 76 proven. 5 refuted. 0 times theorem prover too weak. 93 trivial. 0 not checked.
[2025-04-28 21:21:45,526 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,315 INFO  L134       CoverageAnalysis]: Checked inductivity of 174 backedges. 2 proven. 55 refuted. 0 times theorem prover too weak. 117 trivial. 0 not checked.
[2025-04-28 21:21:47,315 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2122815487] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,315 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,315 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 16
[2025-04-28 21:21:47,316 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [63818468]
[2025-04-28 21:21:47,316 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,316 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:47,316 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,317 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:47,317 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=35, Invalid=205, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:47,317 INFO  L87              Difference]: Start difference. First operand 50 states and 188 transitions. Second operand  has 16 states, 7 states have (on average 3.857142857142857) internal successors, (27), 16 states have internal predecessors, (27), 11 states have call successors, (19), 2 states have call predecessors, (19), 7 states have return successors, (19), 6 states have call predecessors, (19), 11 states have call successors, (19)
[2025-04-28 21:21:48,934 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,934 INFO  L93              Difference]: Finished difference Result 56 states and 241 transitions.
[2025-04-28 21:21:48,934 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:48,934 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 7 states have (on average 3.857142857142857) internal successors, (27), 16 states have internal predecessors, (27), 11 states have call successors, (19), 2 states have call predecessors, (19), 7 states have return successors, (19), 6 states have call predecessors, (19), 11 states have call successors, (19) Word has length 52
[2025-04-28 21:21:48,935 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,937 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:48,937 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:48,937 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 116 GetRequests, 96 SyntacticMatches, 1 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=82, Invalid=338, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:48,938 INFO  L437           NwaCegarLoop]: 60 mSDtfsCounter, 10 mSDsluCounter, 351 mSDsCounter, 0 mSdLazyCounter, 1462 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 411 SdHoareTripleChecker+Invalid, 1474 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 1462 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,938 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 411 Invalid, 1474 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 1462 Invalid, 0 Unknown, 0 Unchecked, 1.4s Time]
[2025-04-28 21:21:48,939 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:48,957 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 50.
[2025-04-28 21:21:48,958 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 10 states have (on average 2.1) internal successors, (21), 21 states have internal predecessors, (21), 32 states have call successors, (32), 3 states have call predecessors, (32), 7 states have return successors, (135), 25 states have call predecessors, (135), 32 states have call successors, (135)
[2025-04-28 21:21:48,959 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 188 transitions.
[2025-04-28 21:21:48,959 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 188 transitions. Word has length 52
[2025-04-28 21:21:48,960 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,960 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 188 transitions.
[2025-04-28 21:21:48,960 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 7 states have (on average 3.857142857142857) internal successors, (27), 16 states have internal predecessors, (27), 11 states have call successors, (19), 2 states have call predecessors, (19), 7 states have return successors, (19), 6 states have call predecessors, (19), 11 states have call successors, (19)
[2025-04-28 21:21:48,960 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 188 transitions.
[2025-04-28 21:21:48,964 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:48,964 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,964 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,970 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:49,165 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-04-28 21:21:49,165 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,165 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,165 INFO  L85        PathProgramCache]: Analyzing trace with hash 1913753931, now seen corresponding path program 1 times
[2025-04-28 21:21:49,166 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,166 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1684482243]
[2025-04-28 21:21:49,166 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,166 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,170 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:49,172 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:49,173 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,173 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,226 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:49,226 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,226 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1684482243]
[2025-04-28 21:21:49,226 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1684482243] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:49,226 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [361948652]
[2025-04-28 21:21:49,226 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,226 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,229 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,231 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:49,235 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,293 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:49,322 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:49,322 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,322 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,323 INFO  L256         TraceCheckSpWp]: Trace formula consists of 168 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:49,325 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:49,344 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 9 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:49,344 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:49,344 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [361948652] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,344 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:49,344 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 4
[2025-04-28 21:21:49,344 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1204738117]
[2025-04-28 21:21:49,345 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,345 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:49,345 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,345 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:49,345 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:49,346 INFO  L87              Difference]: Start difference. First operand 50 states and 188 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (6), 2 states have call predecessors, (6), 2 states have return successors, (6), 1 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:49,517 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,517 INFO  L93              Difference]: Finished difference Result 52 states and 189 transitions.
[2025-04-28 21:21:49,517 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:49,517 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (6), 2 states have call predecessors, (6), 2 states have return successors, (6), 1 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:49,518 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,520 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:49,520 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:49,520 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 27 GetRequests, 25 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:49,520 INFO  L437           NwaCegarLoop]: 59 mSDtfsCounter, 1 mSDsluCounter, 73 mSDsCounter, 0 mSdLazyCounter, 110 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 132 SdHoareTripleChecker+Invalid, 110 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 110 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,521 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 132 Invalid, 110 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 110 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:49,521 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:49,537 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 50.
[2025-04-28 21:21:49,537 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 10 states have (on average 2.1) internal successors, (21), 21 states have internal predecessors, (21), 32 states have call successors, (32), 3 states have call predecessors, (32), 7 states have return successors, (134), 25 states have call predecessors, (134), 32 states have call successors, (134)
[2025-04-28 21:21:49,539 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 187 transitions.
[2025-04-28 21:21:49,539 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 187 transitions. Word has length 24
[2025-04-28 21:21:49,539 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,539 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 187 transitions.
[2025-04-28 21:21:49,539 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (6), 2 states have call predecessors, (6), 2 states have return successors, (6), 1 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:49,540 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 187 transitions.
[2025-04-28 21:21:49,543 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:49,543 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,543 INFO  L218           NwaCegarLoop]: trace histogram [6, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,549 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:49,744 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:49,744 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,744 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,744 INFO  L85        PathProgramCache]: Analyzing trace with hash -1921942809, now seen corresponding path program 1 times
[2025-04-28 21:21:49,744 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,744 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [673974118]
[2025-04-28 21:21:49,745 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,745 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,751 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:49,759 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:49,759 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,759 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,896 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 2 proven. 16 refuted. 0 times theorem prover too weak. 27 trivial. 0 not checked.
[2025-04-28 21:21:49,896 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,896 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [673974118]
[2025-04-28 21:21:49,896 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [673974118] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:49,896 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2144487493]
[2025-04-28 21:21:49,896 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,896 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,900 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,902 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:49,906 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,967 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:50,003 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:50,003 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,003 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,004 INFO  L256         TraceCheckSpWp]: Trace formula consists of 253 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,005 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,062 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 29 proven. 4 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:50,062 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,452 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 2 proven. 16 refuted. 0 times theorem prover too weak. 27 trivial. 0 not checked.
[2025-04-28 21:21:50,452 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2144487493] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,452 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,452 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:50,453 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1332329861]
[2025-04-28 21:21:50,453 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,453 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:50,453 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,453 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:50,454 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:50,454 INFO  L87              Difference]: Start difference. First operand 50 states and 187 transitions. Second operand  has 10 states, 5 states have (on average 3.6) internal successors, (18), 10 states have internal predecessors, (18), 9 states have call successors, (15), 2 states have call predecessors, (15), 5 states have return successors, (15), 4 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:21:50,956 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,956 INFO  L93              Difference]: Finished difference Result 57 states and 248 transitions.
[2025-04-28 21:21:50,956 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:50,956 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 3.6) internal successors, (18), 10 states have internal predecessors, (18), 9 states have call successors, (15), 2 states have call predecessors, (15), 5 states have return successors, (15), 4 states have call predecessors, (15), 9 states have call successors, (15) Word has length 32
[2025-04-28 21:21:50,956 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,959 INFO  L225             Difference]: With dead ends: 57
[2025-04-28 21:21:50,959 INFO  L226             Difference]: Without dead ends: 57
[2025-04-28 21:21:50,959 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 73 GetRequests, 60 SyntacticMatches, 3 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=34, Invalid=98, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:50,960 INFO  L437           NwaCegarLoop]: 57 mSDtfsCounter, 7 mSDsluCounter, 120 mSDsCounter, 0 mSdLazyCounter, 485 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 177 SdHoareTripleChecker+Invalid, 513 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 485 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,960 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 177 Invalid, 513 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 485 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:50,961 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 57 states.
[2025-04-28 21:21:50,980 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 57 to 53.
[2025-04-28 21:21:50,980 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 53 states, 11 states have (on average 2.0) internal successors, (22), 22 states have internal predecessors, (22), 33 states have call successors, (33), 3 states have call predecessors, (33), 8 states have return successors, (164), 27 states have call predecessors, (164), 33 states have call successors, (164)
[2025-04-28 21:21:50,982 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 53 states to 53 states and 219 transitions.
[2025-04-28 21:21:50,982 INFO  L79                 Accepts]: Start accepts. Automaton has 53 states and 219 transitions. Word has length 32
[2025-04-28 21:21:50,982 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,982 INFO  L485      AbstractCegarLoop]: Abstraction has 53 states and 219 transitions.
[2025-04-28 21:21:50,983 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 3.6) internal successors, (18), 10 states have internal predecessors, (18), 9 states have call successors, (15), 2 states have call predecessors, (15), 5 states have return successors, (15), 4 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:21:50,983 INFO  L278                IsEmpty]: Start isEmpty. Operand 53 states and 219 transitions.
[2025-04-28 21:21:50,987 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:50,987 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,987 INFO  L218           NwaCegarLoop]: trace histogram [6, 4, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,993 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-04-28 21:21:51,187 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,188 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,188 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,188 INFO  L85        PathProgramCache]: Analyzing trace with hash 90615225, now seen corresponding path program 2 times
[2025-04-28 21:21:51,188 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,188 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1082136691]
[2025-04-28 21:21:51,189 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:51,189 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,195 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:21:51,210 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:51,211 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:51,211 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,261 INFO  L134       CoverageAnalysis]: Checked inductivity of 47 backedges. 12 proven. 0 refuted. 0 times theorem prover too weak. 35 trivial. 0 not checked.
[2025-04-28 21:21:51,261 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,261 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1082136691]
[2025-04-28 21:21:51,262 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1082136691] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,262 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,262 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:51,262 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [176398138]
[2025-04-28 21:21:51,262 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,262 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:51,262 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,263 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:51,263 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:51,263 INFO  L87              Difference]: Start difference. First operand 53 states and 219 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, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:51,458 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,458 INFO  L93              Difference]: Finished difference Result 57 states and 246 transitions.
[2025-04-28 21:21:51,459 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:51,459 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, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:21:51,459 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,462 INFO  L225             Difference]: With dead ends: 57
[2025-04-28 21:21:51,462 INFO  L226             Difference]: Without dead ends: 57
[2025-04-28 21:21:51,462 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:51,463 INFO  L437           NwaCegarLoop]: 81 mSDtfsCounter, 1 mSDsluCounter, 106 mSDsCounter, 0 mSdLazyCounter, 116 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 187 SdHoareTripleChecker+Invalid, 120 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 116 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,463 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 187 Invalid, 120 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 116 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:51,464 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 57 states.
[2025-04-28 21:21:51,483 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 57 to 53.
[2025-04-28 21:21:51,484 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 53 states, 11 states have (on average 2.0) internal successors, (22), 22 states have internal predecessors, (22), 33 states have call successors, (33), 3 states have call predecessors, (33), 8 states have return successors, (162), 27 states have call predecessors, (162), 33 states have call successors, (162)
[2025-04-28 21:21:51,486 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 53 states to 53 states and 217 transitions.
[2025-04-28 21:21:51,486 INFO  L79                 Accepts]: Start accepts. Automaton has 53 states and 217 transitions. Word has length 32
[2025-04-28 21:21:51,486 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,486 INFO  L485      AbstractCegarLoop]: Abstraction has 53 states and 217 transitions.
[2025-04-28 21:21:51,486 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, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:51,486 INFO  L278                IsEmpty]: Start isEmpty. Operand 53 states and 217 transitions.
[2025-04-28 21:21:51,490 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:51,490 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,490 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,490 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:51,491 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,491 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,491 INFO  L85        PathProgramCache]: Analyzing trace with hash 396717630, now seen corresponding path program 1 times
[2025-04-28 21:21:51,491 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,491 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1408652022]
[2025-04-28 21:21:51,491 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,492 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,496 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:51,509 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:51,510 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,510 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,921 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 4 proven. 14 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:51,921 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,921 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1408652022]
[2025-04-28 21:21:51,922 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1408652022] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:51,922 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1324296585]
[2025-04-28 21:21:51,922 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,922 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,924 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:51,926 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:51,931 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:21:51,994 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:52,026 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:52,026 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,026 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,028 INFO  L256         TraceCheckSpWp]: Trace formula consists of 208 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,029 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,113 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 18 proven. 2 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:52,113 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,411 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 8 proven. 10 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:52,411 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1324296585] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,411 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,411 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 6, 6] total 12
[2025-04-28 21:21:52,411 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1182452916]
[2025-04-28 21:21:52,411 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,412 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:52,412 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,412 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:52,413 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=106, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:52,413 INFO  L87              Difference]: Start difference. First operand 53 states and 217 transitions. Second operand  has 12 states, 5 states have (on average 3.4) internal successors, (17), 9 states have internal predecessors, (17), 10 states have call successors, (16), 2 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 10 states have call successors, (16)
[2025-04-28 21:21:53,675 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,675 INFO  L93              Difference]: Finished difference Result 62 states and 309 transitions.
[2025-04-28 21:21:53,675 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:53,675 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 5 states have (on average 3.4) internal successors, (17), 9 states have internal predecessors, (17), 10 states have call successors, (16), 2 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 10 states have call successors, (16) Word has length 28
[2025-04-28 21:21:53,676 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,678 INFO  L225             Difference]: With dead ends: 62
[2025-04-28 21:21:53,678 INFO  L226             Difference]: Without dead ends: 62
[2025-04-28 21:21:53,678 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 69 GetRequests, 56 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=44, Invalid=166, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:53,679 INFO  L437           NwaCegarLoop]: 61 mSDtfsCounter, 6 mSDsluCounter, 188 mSDsCounter, 0 mSdLazyCounter, 929 mSolverCounterSat, 36 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 249 SdHoareTripleChecker+Invalid, 965 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 36 IncrementalHoareTripleChecker+Valid, 929 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,679 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 249 Invalid, 965 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [36 Valid, 929 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:21:53,679 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-04-28 21:21:53,707 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 54.
[2025-04-28 21:21:53,709 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 54 states, 11 states have (on average 2.0) internal successors, (22), 22 states have internal predecessors, (22), 34 states have call successors, (34), 3 states have call predecessors, (34), 8 states have return successors, (167), 28 states have call predecessors, (167), 34 states have call successors, (167)
[2025-04-28 21:21:53,710 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 223 transitions.
[2025-04-28 21:21:53,711 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 223 transitions. Word has length 28
[2025-04-28 21:21:53,711 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,711 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 223 transitions.
[2025-04-28 21:21:53,711 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 5 states have (on average 3.4) internal successors, (17), 9 states have internal predecessors, (17), 10 states have call successors, (16), 2 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 10 states have call successors, (16)
[2025-04-28 21:21:53,711 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 223 transitions.
[2025-04-28 21:21:53,716 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:53,716 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,716 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 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,721 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Ended with exit code 0
[2025-04-28 21:21:53,916 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-04-28 21:21:53,917 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,917 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,917 INFO  L85        PathProgramCache]: Analyzing trace with hash 1633851470, now seen corresponding path program 1 times
[2025-04-28 21:21:53,917 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,918 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [891346641]
[2025-04-28 21:21:53,918 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,919 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,924 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:53,946 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:53,951 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,951 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,300 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 8 proven. 6 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:54,300 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,300 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [891346641]
[2025-04-28 21:21:54,300 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [891346641] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,300 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1091780151]
[2025-04-28 21:21:54,300 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,300 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,303 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,305 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:54,309 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,377 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:54,407 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:54,407 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,407 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,409 INFO  L256         TraceCheckSpWp]: Trace formula consists of 208 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,410 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,503 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 18 proven. 2 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:54,504 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,830 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 8 proven. 10 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:54,830 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1091780151] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,830 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,830 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 12
[2025-04-28 21:21:54,831 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [732960764]
[2025-04-28 21:21:54,831 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,831 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:54,832 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,833 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:54,833 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=106, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:54,833 INFO  L87              Difference]: Start difference. First operand 54 states and 223 transitions. Second operand  has 12 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 10 states have internal predecessors, (19), 9 states have call successors, (16), 2 states have call predecessors, (16), 6 states have return successors, (16), 4 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:55,997 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,998 INFO  L93              Difference]: Finished difference Result 68 states and 381 transitions.
[2025-04-28 21:21:55,998 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:55,998 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 10 states have internal predecessors, (19), 9 states have call successors, (16), 2 states have call predecessors, (16), 6 states have return successors, (16), 4 states have call predecessors, (16), 9 states have call successors, (16) Word has length 28
[2025-04-28 21:21:55,998 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,002 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:21:56,002 INFO  L226             Difference]: Without dead ends: 68
[2025-04-28 21:21:56,002 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 68 GetRequests, 54 SyntacticMatches, 0 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 11 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=55, Invalid=185, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:56,003 INFO  L437           NwaCegarLoop]: 59 mSDtfsCounter, 6 mSDsluCounter, 213 mSDsCounter, 0 mSdLazyCounter, 642 mSolverCounterSat, 31 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 272 SdHoareTripleChecker+Invalid, 673 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 31 IncrementalHoareTripleChecker+Valid, 642 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,003 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 272 Invalid, 673 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [31 Valid, 642 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:56,003 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 68 states.
[2025-04-28 21:21:56,031 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 68 to 60.
[2025-04-28 21:21:56,032 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 60 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 23 states have internal predecessors, (23), 38 states have call successors, (38), 3 states have call predecessors, (38), 9 states have return successors, (225), 33 states have call predecessors, (225), 38 states have call successors, (225)
[2025-04-28 21:21:56,034 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 60 states to 60 states and 286 transitions.
[2025-04-28 21:21:56,034 INFO  L79                 Accepts]: Start accepts. Automaton has 60 states and 286 transitions. Word has length 28
[2025-04-28 21:21:56,035 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,035 INFO  L485      AbstractCegarLoop]: Abstraction has 60 states and 286 transitions.
[2025-04-28 21:21:56,035 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 10 states have internal predecessors, (19), 9 states have call successors, (16), 2 states have call predecessors, (16), 6 states have return successors, (16), 4 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:56,035 INFO  L278                IsEmpty]: Start isEmpty. Operand 60 states and 286 transitions.
[2025-04-28 21:21:56,040 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:56,040 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,040 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,046 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Ended with exit code 0
[2025-04-28 21:21:56,245 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 13 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable16
[2025-04-28 21:21:56,245 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,245 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,245 INFO  L85        PathProgramCache]: Analyzing trace with hash -945002003, now seen corresponding path program 1 times
[2025-04-28 21:21:56,246 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,246 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1125005363]
[2025-04-28 21:21:56,246 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,246 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,250 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:56,256 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:56,256 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,256 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,419 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 2 proven. 12 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:56,419 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,419 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1125005363]
[2025-04-28 21:21:56,419 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1125005363] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,419 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1989681412]
[2025-04-28 21:21:56,419 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,419 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,422 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,425 INFO  L229       MonitoredProcess]: Starting monitored process 14 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:56,429 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,497 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:56,532 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:56,532 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,532 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,537 INFO  L256         TraceCheckSpWp]: Trace formula consists of 212 conjuncts, 36 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,538 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,607 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 18 proven. 2 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:56,607 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:57,303 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 0 proven. 14 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:57,303 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1989681412] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:57,303 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:57,303 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:57,303 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1864080666]
[2025-04-28 21:21:57,303 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,304 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:57,304 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,304 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:57,305 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:57,305 INFO  L87              Difference]: Start difference. First operand 60 states and 286 transitions. Second operand  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (11), 2 states have call predecessors, (11), 5 states have return successors, (12), 2 states have call predecessors, (12), 5 states have call successors, (12)
[2025-04-28 21:21:57,935 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,935 INFO  L93              Difference]: Finished difference Result 64 states and 319 transitions.
[2025-04-28 21:21:57,936 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:57,936 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (11), 2 states have call predecessors, (11), 5 states have return successors, (12), 2 states have call predecessors, (12), 5 states have call successors, (12) Word has length 28
[2025-04-28 21:21:57,936 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,939 INFO  L225             Difference]: With dead ends: 64
[2025-04-28 21:21:57,939 INFO  L226             Difference]: Without dead ends: 64
[2025-04-28 21:21:57,939 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 63 GetRequests, 56 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=49, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:57,940 INFO  L437           NwaCegarLoop]: 60 mSDtfsCounter, 3 mSDsluCounter, 136 mSDsCounter, 0 mSdLazyCounter, 526 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 196 SdHoareTripleChecker+Invalid, 526 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 526 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,940 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 196 Invalid, 526 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 526 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:57,941 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 64 states.
[2025-04-28 21:21:57,961 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 64 to 60.
[2025-04-28 21:21:57,962 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 60 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 23 states have internal predecessors, (23), 38 states have call successors, (38), 3 states have call predecessors, (38), 9 states have return successors, (224), 33 states have call predecessors, (224), 38 states have call successors, (224)
[2025-04-28 21:21:57,964 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 60 states to 60 states and 285 transitions.
[2025-04-28 21:21:57,964 INFO  L79                 Accepts]: Start accepts. Automaton has 60 states and 285 transitions. Word has length 28
[2025-04-28 21:21:57,965 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,965 INFO  L485      AbstractCegarLoop]: Abstraction has 60 states and 285 transitions.
[2025-04-28 21:21:57,965 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (11), 2 states have call predecessors, (11), 5 states have return successors, (12), 2 states have call predecessors, (12), 5 states have call successors, (12)
[2025-04-28 21:21:57,965 INFO  L278                IsEmpty]: Start isEmpty. Operand 60 states and 285 transitions.
[2025-04-28 21:21:57,970 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:57,970 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,970 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,976 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Ended with exit code 0
[2025-04-28 21:21:58,174 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 14 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable17
[2025-04-28 21:21:58,174 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,175 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,175 INFO  L85        PathProgramCache]: Analyzing trace with hash 1015284550, now seen corresponding path program 1 times
[2025-04-28 21:21:58,175 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,175 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1502515066]
[2025-04-28 21:21:58,175 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,175 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,183 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:58,206 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:58,206 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,206 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,317 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 6 proven. 6 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:58,317 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,317 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1502515066]
[2025-04-28 21:21:58,317 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1502515066] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,318 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [284977424]
[2025-04-28 21:21:58,318 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,318 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,320 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:58,322 INFO  L229       MonitoredProcess]: Starting monitored process 15 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:58,326 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,394 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:58,425 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:58,425 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,425 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,426 INFO  L256         TraceCheckSpWp]: Trace formula consists of 208 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,428 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,462 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 6 proven. 6 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:58,462 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,739 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 6 proven. 6 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:58,739 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [284977424] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:58,739 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:58,739 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 7
[2025-04-28 21:21:58,739 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [851906953]
[2025-04-28 21:21:58,740 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,740 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:58,740 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,740 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:58,740 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:58,741 INFO  L87              Difference]: Start difference. First operand 60 states and 285 transitions. Second operand  has 7 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 7 states have internal predecessors, (11), 6 states have call successors, (9), 1 states have call predecessors, (9), 3 states have return successors, (9), 2 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:21:59,605 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,605 INFO  L93              Difference]: Finished difference Result 69 states and 390 transitions.
[2025-04-28 21:21:59,606 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:59,606 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 7 states have internal predecessors, (11), 6 states have call successors, (9), 1 states have call predecessors, (9), 3 states have return successors, (9), 2 states have call predecessors, (9), 6 states have call successors, (9) Word has length 28
[2025-04-28 21:21:59,606 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,610 INFO  L225             Difference]: With dead ends: 69
[2025-04-28 21:21:59,610 INFO  L226             Difference]: Without dead ends: 69
[2025-04-28 21:21:59,610 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 65 GetRequests, 58 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=26, Invalid=46, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:59,611 INFO  L437           NwaCegarLoop]: 63 mSDtfsCounter, 3 mSDsluCounter, 132 mSDsCounter, 0 mSdLazyCounter, 642 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 195 SdHoareTripleChecker+Invalid, 658 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 642 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,611 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 195 Invalid, 658 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 642 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:59,611 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 69 states.
[2025-04-28 21:21:59,648 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 69 to 65.
[2025-04-28 21:21:59,648 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 65 states, 13 states have (on average 1.8461538461538463) internal successors, (24), 24 states have internal predecessors, (24), 41 states have call successors, (41), 3 states have call predecessors, (41), 10 states have return successors, (283), 37 states have call predecessors, (283), 41 states have call successors, (283)
[2025-04-28 21:21:59,651 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 65 states to 65 states and 348 transitions.
[2025-04-28 21:21:59,651 INFO  L79                 Accepts]: Start accepts. Automaton has 65 states and 348 transitions. Word has length 28
[2025-04-28 21:21:59,652 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,652 INFO  L485      AbstractCegarLoop]: Abstraction has 65 states and 348 transitions.
[2025-04-28 21:21:59,652 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 3 states have (on average 3.6666666666666665) internal successors, (11), 7 states have internal predecessors, (11), 6 states have call successors, (9), 1 states have call predecessors, (9), 3 states have return successors, (9), 2 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:21:59,652 INFO  L278                IsEmpty]: Start isEmpty. Operand 65 states and 348 transitions.
[2025-04-28 21:21:59,657 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:59,657 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,658 INFO  L218           NwaCegarLoop]: trace histogram [8, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,664 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Ended with exit code 0
[2025-04-28 21:21:59,862 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,15 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,862 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,862 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,862 INFO  L85        PathProgramCache]: Analyzing trace with hash -270069499, now seen corresponding path program 1 times
[2025-04-28 21:21:59,863 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,863 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [302196887]
[2025-04-28 21:21:59,863 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,863 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,869 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:59,879 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:59,879 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,879 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,166 INFO  L134       CoverageAnalysis]: Checked inductivity of 84 backedges. 12 proven. 30 refuted. 0 times theorem prover too weak. 42 trivial. 0 not checked.
[2025-04-28 21:22:00,167 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,167 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [302196887]
[2025-04-28 21:22:00,167 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [302196887] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,167 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1826205898]
[2025-04-28 21:22:00,167 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,167 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,169 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,172 INFO  L229       MonitoredProcess]: Starting monitored process 16 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:00,176 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (16)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,248 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:22:00,302 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:22:00,303 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,303 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,305 INFO  L256         TraceCheckSpWp]: Trace formula consists of 332 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,307 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,439 INFO  L134       CoverageAnalysis]: Checked inductivity of 84 backedges. 14 proven. 28 refuted. 0 times theorem prover too weak. 42 trivial. 0 not checked.
[2025-04-28 21:22:00,439 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,099 INFO  L134       CoverageAnalysis]: Checked inductivity of 84 backedges. 14 proven. 28 refuted. 0 times theorem prover too weak. 42 trivial. 0 not checked.
[2025-04-28 21:22:01,100 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1826205898] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,100 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,100 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 9] total 17
[2025-04-28 21:22:01,100 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1269460113]
[2025-04-28 21:22:01,100 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,100 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:22:01,100 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,101 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:22:01,101 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=226, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:22:01,101 INFO  L87              Difference]: Start difference. First operand 65 states and 348 transitions. Second operand  has 17 states, 7 states have (on average 3.142857142857143) internal successors, (22), 16 states have internal predecessors, (22), 14 states have call successors, (17), 1 states have call predecessors, (17), 7 states have return successors, (17), 5 states have call predecessors, (17), 14 states have call successors, (17)
