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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:26,524 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:26,582 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ac31059d-0ed9-40bb-8b84-e2172749aa0e/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:26,587 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:26,587 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:26,626 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:26,627 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:26,627 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:26,627 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:26,627 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:26,628 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:26,628 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:26,628 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:26,628 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:26,628 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:26,629 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:26,629 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:26,629 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:26,629 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:26,629 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:26,629 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:26,629 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:26,630 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:26,630 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:26,630 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:26,631 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:26,631 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:26,943 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:26,954 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:26,957 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:26,959 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:26,960 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:26,961 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ac31059d-0ed9-40bb-8b84-e2172749aa0e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-023.smt2
[2025-04-28 21:21:26,963 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:26,970 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:27,225 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ac31059d-0ed9-40bb-8b84-e2172749aa0e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-023.smt2
[2025-04-28 21:21:27,228 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:27,230 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:27,233 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:27,233 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:27,233 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:27,237 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,272 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27 Unit
[2025-04-28 21:21:27,273 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:27,274 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:27,275 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:27,275 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:27,290 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,290 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,317 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,318 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,321 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,323 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,328 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,329 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,329 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,347 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:27,349 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:27,349 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:27,349 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:27,350 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,353 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:27,369 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,386 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:27,392 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:27,409 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:27,410 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:27,410 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:27,410 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:27,410 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:27,410 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:27,410 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:27,410 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:27,410 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:27,410 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibonacci given in one single declaration
[2025-04-28 21:21:27,411 INFO  L130     BoogieDeclarations]: Found specification of procedure fibonacci
[2025-04-28 21:21:27,411 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibonacci
[2025-04-28 21:21:27,411 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibonacci.AT.split given in one single declaration
[2025-04-28 21:21:27,411 INFO  L130     BoogieDeclarations]: Found specification of procedure fibonacci.AT.split
[2025-04-28 21:21:27,411 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibonacci.AT.split
[2025-04-28 21:21:27,411 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibonacci.AT_call given in one single declaration
[2025-04-28 21:21:27,411 INFO  L130     BoogieDeclarations]: Found specification of procedure fibonacci.AT_call
[2025-04-28 21:21:27,411 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibonacci.AT_call
[2025-04-28 21:21:27,411 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:27,411 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:27,411 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:27,473 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:27,476 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:27,613 INFO  L?                        ?]: Removed 20 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:27,613 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:27,624 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:27,624 INFO  L312             CfgBuilder]: Removed 3 assume(true) statements.
[2025-04-28 21:21:27,624 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:27 BoogieIcfgContainer
[2025-04-28 21:21:27,624 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:27,627 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:27,627 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:27,630 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:27,630 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:27" (1/3) ...
[2025-04-28 21:21:27,631 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3dddc5f8 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:27, skipping insertion in model container
[2025-04-28 21:21:27,631 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (2/3) ...
[2025-04-28 21:21:27,631 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3dddc5f8 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:27, skipping insertion in model container
[2025-04-28 21:21:27,632 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:27" (3/3) ...
[2025-04-28 21:21:27,633 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:27,652 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:27,655 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 27 locations, 39 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:27,693 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:27,711 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;@72174845, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:27,711 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:27,715 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 27 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 6 states have call predecessors, (8), 6 states have return successors, (8), 8 states have call predecessors, (8), 8 states have call successors, (8)
[2025-04-28 21:21:27,725 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:27,725 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,726 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,726 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,732 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,732 INFO  L85        PathProgramCache]: Analyzing trace with hash 1798046636, now seen corresponding path program 1 times
[2025-04-28 21:21:27,739 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,740 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1076588476]
[2025-04-28 21:21:27,740 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,741 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,769 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:27,783 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:27,784 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,784 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,928 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:27,928 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,928 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1076588476]
[2025-04-28 21:21:27,929 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1076588476] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,929 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,932 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:27,933 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [742580765]
[2025-04-28 21:21:27,934 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,937 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:27,937 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,967 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:27,967 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:27,969 INFO  L87              Difference]: Start difference. First operand  has 27 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 6 states have call predecessors, (8), 6 states have return successors, (8), 8 states have call predecessors, (8), 8 states have call successors, (8) Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:28,052 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,055 INFO  L93              Difference]: Finished difference Result 27 states and 32 transitions.
[2025-04-28 21:21:28,057 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:28,058 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4) Word has length 15
[2025-04-28 21:21:28,058 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,066 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:28,066 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:28,069 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:28,073 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 1 mSDsluCounter, 43 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 70 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,074 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 70 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:28,088 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:28,135 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:28,137 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 13 states have internal predecessors, (14), 8 states have call successors, (8), 6 states have call predecessors, (8), 7 states have return successors, (10), 8 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:28,140 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:28,141 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:28,142 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,142 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:28,142 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:28,142 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:28,146 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:28,146 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,146 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,146 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:28,146 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,147 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,147 INFO  L85        PathProgramCache]: Analyzing trace with hash 395917480, now seen corresponding path program 1 times
[2025-04-28 21:21:28,147 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,147 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [914764717]
[2025-04-28 21:21:28,148 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,148 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,153 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:28,157 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:28,157 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,157 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,262 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:28,263 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,263 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [914764717]
[2025-04-28 21:21:28,263 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [914764717] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,263 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,263 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:28,263 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [567032892]
[2025-04-28 21:21:28,263 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,264 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:28,264 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,265 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:28,265 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,267 INFO  L87              Difference]: Start difference. First operand 27 states and 32 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:28,308 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,308 INFO  L93              Difference]: Finished difference Result 31 states and 38 transitions.
[2025-04-28 21:21:28,309 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:28,309 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4) Word has length 15
[2025-04-28 21:21:28,309 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,310 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:28,310 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:28,310 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:28,311 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 1 mSDsluCounter, 43 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 70 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,312 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 70 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:28,313 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:28,317 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 27.
[2025-04-28 21:21:28,317 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 12 states have internal predecessors, (14), 8 states have call successors, (8), 6 states have call predecessors, (8), 7 states have return successors, (10), 8 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:28,318 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:28,318 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:28,318 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,318 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:28,319 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:28,319 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:28,320 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:28,320 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,320 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,320 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:28,320 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,321 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,321 INFO  L85        PathProgramCache]: Analyzing trace with hash -910996012, now seen corresponding path program 1 times
[2025-04-28 21:21:28,321 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,321 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [943605656]
[2025-04-28 21:21:28,321 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,322 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,339 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:28,353 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:28,353 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,353 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,487 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:28,487 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,488 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [943605656]
[2025-04-28 21:21:28,488 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [943605656] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,488 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [737150076]
[2025-04-28 21:21:28,488 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,488 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,492 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,497 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:28,500 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,564 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:28,599 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:28,599 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,599 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,601 INFO  L256         TraceCheckSpWp]: Trace formula consists of 113 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,608 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,698 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:28,698 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:28,698 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [737150076] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,698 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:28,698 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 5
[2025-04-28 21:21:28,699 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [591573475]
[2025-04-28 21:21:28,699 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,699 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:28,699 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,702 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:28,702 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:28,702 INFO  L87              Difference]: Start difference. First operand 27 states and 32 transitions. Second operand  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:28,733 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,733 INFO  L93              Difference]: Finished difference Result 29 states and 34 transitions.
[2025-04-28 21:21:28,735 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:28,736 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:28,736 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,737 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:28,737 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:21:28,738 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 30 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:28,739 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 1 mSDsluCounter, 45 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 73 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,739 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 73 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:28,744 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:21:28,750 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:21:28,751 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 12 states have (on average 1.25) internal successors, (15), 14 states have internal predecessors, (15), 8 states have call successors, (8), 6 states have call predecessors, (8), 8 states have return successors, (11), 8 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:28,751 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 34 transitions.
[2025-04-28 21:21:28,752 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 34 transitions. Word has length 30
[2025-04-28 21:21:28,752 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,752 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 34 transitions.
[2025-04-28 21:21:28,752 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:28,752 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 34 transitions.
[2025-04-28 21:21:28,753 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:28,753 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,753 INFO  L218           NwaCegarLoop]: trace histogram [3, 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, 1]
[2025-04-28 21:21:28,761 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:28,954 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:28,954 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,955 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,955 INFO  L85        PathProgramCache]: Analyzing trace with hash -1524351780, now seen corresponding path program 1 times
[2025-04-28 21:21:28,955 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,955 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1087001536]
[2025-04-28 21:21:28,955 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,955 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,963 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:28,971 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:28,971 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,971 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,023 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:29,023 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,023 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1087001536]
[2025-04-28 21:21:29,023 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1087001536] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,023 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [497840208]
[2025-04-28 21:21:29,023 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,024 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,027 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,029 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:29,033 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,090 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:29,132 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:29,132 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,132 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,134 INFO  L256         TraceCheckSpWp]: Trace formula consists of 113 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,139 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,153 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:29,155 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:29,156 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [497840208] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,156 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:29,156 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 4
[2025-04-28 21:21:29,156 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [508627316]
[2025-04-28 21:21:29,156 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,158 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:29,158 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,159 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:29,159 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:29,159 INFO  L87              Difference]: Start difference. First operand 29 states and 34 transitions. Second operand  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 2 states have call predecessors, (8), 2 states have return successors, (8), 1 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:29,178 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,179 INFO  L93              Difference]: Finished difference Result 29 states and 33 transitions.
[2025-04-28 21:21:29,180 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:29,180 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 2 states have call predecessors, (8), 2 states have return successors, (8), 1 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:29,180 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,182 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:29,182 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:29,182 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 31 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:29,184 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 1 mSDsluCounter, 46 mSDsCounter, 0 mSdLazyCounter, 5 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 75 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 5 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,185 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 75 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 5 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:29,187 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:29,192 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:29,195 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 8 states have call successors, (8), 6 states have call predecessors, (8), 7 states have return successors, (10), 8 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:29,196 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 30 transitions.
[2025-04-28 21:21:29,196 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 30 transitions. Word has length 30
[2025-04-28 21:21:29,196 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,196 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 30 transitions.
[2025-04-28 21:21:29,196 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 2 states have call predecessors, (8), 2 states have return successors, (8), 1 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:29,197 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 30 transitions.
[2025-04-28 21:21:29,197 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:29,197 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,197 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:29,203 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:29,398 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:29,398 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,399 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,399 INFO  L85        PathProgramCache]: Analyzing trace with hash 1895196644, now seen corresponding path program 1 times
[2025-04-28 21:21:29,399 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,399 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1924283494]
[2025-04-28 21:21:29,399 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,399 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,412 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:29,434 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:29,434 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,434 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,774 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:29,776 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,776 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1924283494]
[2025-04-28 21:21:29,776 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1924283494] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,776 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [776984041]
[2025-04-28 21:21:29,776 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,777 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,779 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,782 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:29,786 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,829 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:29,854 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:29,854 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,854 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,856 INFO  L256         TraceCheckSpWp]: Trace formula consists of 113 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,858 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,156 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:30,157 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:32,324 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:32,324 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [776984041] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:32,324 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:32,324 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 9
[2025-04-28 21:21:32,324 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1238537733]
[2025-04-28 21:21:32,325 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,325 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:32,325 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,326 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:32,326 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=53, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:32,326 INFO  L87              Difference]: Start difference. First operand 27 states and 30 transitions. Second operand  has 9 states, 5 states have (on average 3.4) internal successors, (17), 9 states have internal predecessors, (17), 7 states have call successors, (11), 2 states have call predecessors, (11), 5 states have return successors, (11), 3 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:32,407 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,407 INFO  L93              Difference]: Finished difference Result 33 states and 41 transitions.
[2025-04-28 21:21:32,409 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:32,409 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 3.4) internal successors, (17), 9 states have internal predecessors, (17), 7 states have call successors, (11), 2 states have call predecessors, (11), 5 states have return successors, (11), 3 states have call predecessors, (11), 7 states have call successors, (11) Word has length 30
[2025-04-28 21:21:32,410 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,410 INFO  L225             Difference]: With dead ends: 33
[2025-04-28 21:21:32,410 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:21:32,410 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 56 SyntacticMatches, 3 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=53, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:32,411 INFO  L437           NwaCegarLoop]: 25 mSDtfsCounter, 2 mSDsluCounter, 104 mSDsCounter, 0 mSdLazyCounter, 38 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 129 SdHoareTripleChecker+Invalid, 39 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 38 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,411 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 129 Invalid, 39 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 38 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:32,412 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:21:32,418 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 33.
[2025-04-28 21:21:32,418 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 10 states have call successors, (10), 6 states have call predecessors, (10), 9 states have return successors, (17), 12 states have call predecessors, (17), 10 states have call successors, (17)
[2025-04-28 21:21:32,423 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 41 transitions.
[2025-04-28 21:21:32,423 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 41 transitions. Word has length 30
[2025-04-28 21:21:32,423 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,423 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 41 transitions.
[2025-04-28 21:21:32,423 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 3.4) internal successors, (17), 9 states have internal predecessors, (17), 7 states have call successors, (11), 2 states have call predecessors, (11), 5 states have return successors, (11), 3 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:32,424 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 41 transitions.
[2025-04-28 21:21:32,425 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 61
[2025-04-28 21:21:32,425 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,425 INFO  L218           NwaCegarLoop]: trace histogram [7, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,431 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:32,625 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:32,626 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,626 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,626 INFO  L85        PathProgramCache]: Analyzing trace with hash 1369193224, now seen corresponding path program 2 times
[2025-04-28 21:21:32,626 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,626 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [794092107]
[2025-04-28 21:21:32,627 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:32,627 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,638 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:32,664 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:32,664 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:32,664 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,150 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 14 proven. 33 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:33,150 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,150 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [794092107]
[2025-04-28 21:21:33,150 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [794092107] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,150 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [279621107]
[2025-04-28 21:21:33,151 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:33,151 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,154 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,156 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:33,163 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,230 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:33,275 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:33,275 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:33,275 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,281 INFO  L256         TraceCheckSpWp]: Trace formula consists of 251 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,285 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,555 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 32 proven. 21 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:33,555 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,717 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 32 proven. 21 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:38,718 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [279621107] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,718 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,718 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 12, 12] total 20
[2025-04-28 21:21:38,718 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [357448724]
[2025-04-28 21:21:38,718 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,719 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:38,719 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,720 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:38,720 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=62, Invalid=318, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:38,720 INFO  L87              Difference]: Start difference. First operand 33 states and 41 transitions. Second operand  has 20 states, 11 states have (on average 2.6363636363636362) internal successors, (29), 18 states have internal predecessors, (29), 15 states have call successors, (24), 2 states have call predecessors, (24), 11 states have return successors, (29), 13 states have call predecessors, (29), 15 states have call successors, (29)
[2025-04-28 21:21:39,217 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,218 INFO  L93              Difference]: Finished difference Result 60 states and 91 transitions.
[2025-04-28 21:21:39,219 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:21:39,219 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 11 states have (on average 2.6363636363636362) internal successors, (29), 18 states have internal predecessors, (29), 15 states have call successors, (24), 2 states have call predecessors, (24), 11 states have return successors, (29), 13 states have call predecessors, (29), 15 states have call successors, (29) Word has length 60
[2025-04-28 21:21:39,219 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,221 INFO  L225             Difference]: With dead ends: 60
[2025-04-28 21:21:39,223 INFO  L226             Difference]: Without dead ends: 60
[2025-04-28 21:21:39,224 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 139 GetRequests, 107 SyntacticMatches, 5 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 164 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=147, Invalid=665, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:21:39,224 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 21 mSDsluCounter, 348 mSDsCounter, 0 mSdLazyCounter, 172 mSolverCounterSat, 72 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 382 SdHoareTripleChecker+Invalid, 244 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 72 IncrementalHoareTripleChecker+Valid, 172 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,226 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 382 Invalid, 244 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [72 Valid, 172 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:39,227 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 60 states.
[2025-04-28 21:21:39,236 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 60 to 57.
[2025-04-28 21:21:39,236 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 22 states have (on average 1.0909090909090908) internal successors, (24), 24 states have internal predecessors, (24), 18 states have call successors, (18), 8 states have call predecessors, (18), 16 states have return successors, (44), 24 states have call predecessors, (44), 18 states have call successors, (44)
[2025-04-28 21:21:39,237 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 86 transitions.
[2025-04-28 21:21:39,238 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 86 transitions. Word has length 60
[2025-04-28 21:21:39,238 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,238 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 86 transitions.
[2025-04-28 21:21:39,238 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 11 states have (on average 2.6363636363636362) internal successors, (29), 18 states have internal predecessors, (29), 15 states have call successors, (24), 2 states have call predecessors, (24), 11 states have return successors, (29), 13 states have call predecessors, (29), 15 states have call successors, (29)
[2025-04-28 21:21:39,239 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 86 transitions.
[2025-04-28 21:21:39,244 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 241
[2025-04-28 21:21:39,245 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,245 INFO  L218           NwaCegarLoop]: trace histogram [31, 16, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,249 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:39,446 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:39,446 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,447 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,447 INFO  L85        PathProgramCache]: Analyzing trace with hash 341954696, now seen corresponding path program 3 times
[2025-04-28 21:21:39,447 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,447 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [472376950]
[2025-04-28 21:21:39,447 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:39,447 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,480 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 240 statements into 19 equivalence classes.
[2025-04-28 21:21:39,606 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 135 of 240 statements.
[2025-04-28 21:21:39,606 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:39,606 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,240 INFO  L134       CoverageAnalysis]: Checked inductivity of 2340 backedges. 601 proven. 132 refuted. 0 times theorem prover too weak. 1607 trivial. 0 not checked.
[2025-04-28 21:21:41,241 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,242 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [472376950]
[2025-04-28 21:21:41,242 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [472376950] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,242 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [327937434]
[2025-04-28 21:21:41,242 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:41,243 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,245 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,248 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:41,252 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,409 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 240 statements into 19 equivalence classes.
[2025-04-28 21:21:41,518 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 135 of 240 statements.
[2025-04-28 21:21:41,519 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:41,519 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,523 INFO  L256         TraceCheckSpWp]: Trace formula consists of 627 conjuncts, 45 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,533 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,146 INFO  L134       CoverageAnalysis]: Checked inductivity of 2340 backedges. 653 proven. 132 refuted. 0 times theorem prover too weak. 1555 trivial. 0 not checked.
[2025-04-28 21:21:42,146 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,838 INFO  L134       CoverageAnalysis]: Checked inductivity of 2340 backedges. 602 proven. 133 refuted. 0 times theorem prover too weak. 1605 trivial. 0 not checked.
[2025-04-28 21:21:51,838 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [327937434] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,838 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,838 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 16, 17] total 29
[2025-04-28 21:21:51,838 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [209202211]
[2025-04-28 21:21:51,839 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,840 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 29 states
[2025-04-28 21:21:51,840 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,841 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 29 interpolants.
[2025-04-28 21:21:51,841 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=96, Invalid=716, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:21:51,842 INFO  L87              Difference]: Start difference. First operand 57 states and 86 transitions. Second operand  has 29 states, 14 states have (on average 2.857142857142857) internal successors, (40), 25 states have internal predecessors, (40), 23 states have call successors, (36), 2 states have call predecessors, (36), 14 states have return successors, (43), 20 states have call predecessors, (43), 23 states have call successors, (43)
[2025-04-28 21:21:52,432 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,432 INFO  L93              Difference]: Finished difference Result 64 states and 80 transitions.
[2025-04-28 21:21:52,439 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:21:52,439 INFO  L79                 Accepts]: Start accepts. Automaton has  has 29 states, 14 states have (on average 2.857142857142857) internal successors, (40), 25 states have internal predecessors, (40), 23 states have call successors, (36), 2 states have call predecessors, (36), 14 states have return successors, (43), 20 states have call predecessors, (43), 23 states have call successors, (43) Word has length 240
[2025-04-28 21:21:52,440 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,441 INFO  L225             Difference]: With dead ends: 64
[2025-04-28 21:21:52,441 INFO  L226             Difference]: Without dead ends: 64
[2025-04-28 21:21:52,442 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 508 GetRequests, 463 SyntacticMatches, 7 SemanticMatches, 38 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 417 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=252, Invalid=1308, Unknown=0, NotChecked=0, Total=1560
[2025-04-28 21:21:52,446 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 42 mSDsluCounter, 461 mSDsCounter, 0 mSdLazyCounter, 256 mSolverCounterSat, 132 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 42 SdHoareTripleChecker+Valid, 501 SdHoareTripleChecker+Invalid, 388 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 132 IncrementalHoareTripleChecker+Valid, 256 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,446 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [42 Valid, 501 Invalid, 388 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [132 Valid, 256 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:52,447 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 64 states.
[2025-04-28 21:21:52,452 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 64 to 61.
[2025-04-28 21:21:52,454 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 61 states, 25 states have (on average 1.04) internal successors, (26), 24 states have internal predecessors, (26), 20 states have call successors, (20), 12 states have call predecessors, (20), 15 states have return successors, (30), 24 states have call predecessors, (30), 20 states have call successors, (30)
[2025-04-28 21:21:52,455 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 61 states to 61 states and 76 transitions.
[2025-04-28 21:21:52,455 INFO  L79                 Accepts]: Start accepts. Automaton has 61 states and 76 transitions. Word has length 240
[2025-04-28 21:21:52,456 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,456 INFO  L485      AbstractCegarLoop]: Abstraction has 61 states and 76 transitions.
[2025-04-28 21:21:52,456 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 29 states, 14 states have (on average 2.857142857142857) internal successors, (40), 25 states have internal predecessors, (40), 23 states have call successors, (36), 2 states have call predecessors, (36), 14 states have return successors, (43), 20 states have call predecessors, (43), 23 states have call successors, (43)
[2025-04-28 21:21:52,456 INFO  L278                IsEmpty]: Start isEmpty. Operand 61 states and 76 transitions.
[2025-04-28 21:21:52,458 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 151
[2025-04-28 21:21:52,458 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,459 INFO  L218           NwaCegarLoop]: trace histogram [19, 10, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,465 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:52,659 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,659 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,660 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,660 INFO  L85        PathProgramCache]: Analyzing trace with hash 1540848684, now seen corresponding path program 4 times
[2025-04-28 21:21:52,660 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,660 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [139313103]
[2025-04-28 21:21:52,660 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:52,660 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,678 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 150 statements into 2 equivalence classes.
[2025-04-28 21:21:52,702 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 150 of 150 statements.
[2025-04-28 21:21:52,702 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:52,702 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,670 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 82 proven. 223 refuted. 0 times theorem prover too weak. 532 trivial. 0 not checked.
[2025-04-28 21:21:53,673 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,673 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [139313103]
[2025-04-28 21:21:53,674 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [139313103] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,674 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1832389629]
[2025-04-28 21:21:53,674 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:53,674 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,680 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,682 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:53,691 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,886 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 150 statements into 2 equivalence classes.
[2025-04-28 21:21:53,979 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 150 of 150 statements.
[2025-04-28 21:21:53,979 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:53,979 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,983 INFO  L256         TraceCheckSpWp]: Trace formula consists of 665 conjuncts, 24 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,987 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,232 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 203 proven. 76 refuted. 0 times theorem prover too weak. 558 trivial. 0 not checked.
[2025-04-28 21:21:54,232 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
