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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:24,194 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:24,277 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e448418f-6a93-4474-ae8c-4ade5477619d/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:24,282 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:24,285 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:24,325 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:24,325 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:24,326 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:24,326 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:24,326 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:24,326 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:24,327 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:24,327 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:24,327 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:24,327 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:24,327 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:24,327 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:24,327 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:24,327 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:24,328 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:24,328 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:24,328 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:24,331 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:24,331 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:24,331 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:24,333 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:24,333 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:24,660 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:24,674 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:24,678 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:24,682 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:24,682 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:24,685 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e448418f-6a93-4474-ae8c-4ade5477619d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-027.smt2
[2025-04-28 21:21:24,688 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:24,692 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:24,885 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e448418f-6a93-4474-ae8c-4ade5477619d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-027.smt2
[2025-04-28 21:21:24,888 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:24,889 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:24,890 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:24,890 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:24,891 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:24,899 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,924 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24 Unit
[2025-04-28 21:21:24,924 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:24,928 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:24,928 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:24,929 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:24,945 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,945 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,978 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,978 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,985 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,986 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,992 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,992 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,993 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:25,005 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:25,006 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:25,006 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:25,006 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:25,007 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:25,010 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:25,023 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:25,039 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:25,042 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:25,054 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:25,054 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:25,054 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:25,054 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:25,054 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:25,054 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:25,054 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibo given in one single declaration
[2025-04-28 21:21:25,054 INFO  L130     BoogieDeclarations]: Found specification of procedure fibo
[2025-04-28 21:21:25,055 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibo
[2025-04-28 21:21:25,055 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibo.AT.split given in one single declaration
[2025-04-28 21:21:25,055 INFO  L130     BoogieDeclarations]: Found specification of procedure fibo.AT.split
[2025-04-28 21:21:25,055 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibo.AT.split
[2025-04-28 21:21:25,055 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibo.AT_call given in one single declaration
[2025-04-28 21:21:25,055 INFO  L130     BoogieDeclarations]: Found specification of procedure fibo.AT_call
[2025-04-28 21:21:25,055 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibo.AT_call
[2025-04-28 21:21:25,055 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:25,055 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:25,055 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:25,055 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:25,055 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:25,055 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:25,106 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:25,109 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:25,235 INFO  L?                        ?]: Removed 18 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:25,235 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:25,248 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:25,249 INFO  L312             CfgBuilder]: Removed 3 assume(true) statements.
[2025-04-28 21:21:25,249 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:25 BoogieIcfgContainer
[2025-04-28 21:21:25,250 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:25,253 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:25,253 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:25,257 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:25,257 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:24" (1/3) ...
[2025-04-28 21:21:25,258 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4eb913ec and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:25, skipping insertion in model container
[2025-04-28 21:21:25,258 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (2/3) ...
[2025-04-28 21:21:25,259 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4eb913ec and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:25, skipping insertion in model container
[2025-04-28 21:21:25,259 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:25" (3/3) ...
[2025-04-28 21:21:25,261 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:25,277 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:25,281 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:25,349 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:25,372 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;@6e0abdf6, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:25,376 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:25,381 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:25,393 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:25,393 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,394 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:25,395 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,402 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,403 INFO  L85        PathProgramCache]: Analyzing trace with hash -628591717, now seen corresponding path program 1 times
[2025-04-28 21:21:25,413 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,413 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [867422640]
[2025-04-28 21:21:25,414 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,415 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,458 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:25,479 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:25,481 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,481 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,641 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:25,645 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,646 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [867422640]
[2025-04-28 21:21:25,647 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [867422640] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:25,650 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:25,653 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:25,657 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [12188465]
[2025-04-28 21:21:25,659 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,665 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:25,665 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,701 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:25,702 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:25,705 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), 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:25,776 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,776 INFO  L93              Difference]: Finished difference Result 27 states and 32 transitions.
[2025-04-28 21:21:25,778 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:25,780 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (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 15
[2025-04-28 21:21:25,780 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,788 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:25,788 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:25,791 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:25,798 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, 2 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:25,799 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 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:25,816 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:25,840 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:25,841 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:25,848 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:25,849 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:25,850 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,850 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:25,850 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (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:25,850 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:25,853 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:25,853 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,853 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:25,854 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:25,854 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,856 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,856 INFO  L85        PathProgramCache]: Analyzing trace with hash 2047682327, now seen corresponding path program 1 times
[2025-04-28 21:21:25,856 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,856 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1578317449]
[2025-04-28 21:21:25,856 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,856 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,865 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:25,874 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:25,874 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,875 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,940 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:25,941 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,942 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1578317449]
[2025-04-28 21:21:25,942 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1578317449] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:25,942 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:25,942 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:25,942 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [370242855]
[2025-04-28 21:21:25,942 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,943 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:25,946 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,947 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:25,947 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:25,947 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), 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:26,004 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,004 INFO  L93              Difference]: Finished difference Result 31 states and 38 transitions.
[2025-04-28 21:21:26,005 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:26,005 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (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 15
[2025-04-28 21:21:26,006 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,007 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:26,007 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:26,007 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:26,008 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 1 mSDsluCounter, 48 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 78 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:26,011 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 78 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:26,012 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:26,019 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 27.
[2025-04-28 21:21:26,021 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:26,022 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:26,024 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:26,024 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,024 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:26,024 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (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:26,025 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:26,026 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:26,026 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,026 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:26,026 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:26,026 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,027 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,028 INFO  L85        PathProgramCache]: Analyzing trace with hash -98131277, now seen corresponding path program 1 times
[2025-04-28 21:21:26,028 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,028 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2088959035]
[2025-04-28 21:21:26,028 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,029 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,039 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:26,056 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:26,060 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,060 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,519 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:26,520 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,520 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2088959035]
[2025-04-28 21:21:26,520 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2088959035] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:26,520 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1251428006]
[2025-04-28 21:21:26,521 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,521 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:26,524 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:26,528 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:26,530 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:26,621 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:26,665 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:26,665 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,665 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,669 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:26,678 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,053 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:27,055 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:29,232 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,232 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1251428006] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:29,233 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:29,233 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 8
[2025-04-28 21:21:29,233 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2091485798]
[2025-04-28 21:21:29,233 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,234 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:29,234 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,234 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:29,235 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,235 INFO  L87              Difference]: Start difference. First operand 27 states and 32 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, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:21:29,307 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,307 INFO  L93              Difference]: Finished difference Result 34 states and 45 transitions.
[2025-04-28 21:21:29,308 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:29,308 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, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10) Word has length 30
[2025-04-28 21:21:29,308 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,309 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:29,309 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:29,309 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 57 SyntacticMatches, 3 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,310 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 3 mSDsluCounter, 90 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 117 SdHoareTripleChecker+Invalid, 38 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,311 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 117 Invalid, 38 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:29,311 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:29,316 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 32.
[2025-04-28 21:21:29,316 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 13 states have (on average 1.2307692307692308) internal successors, (16), 15 states have internal predecessors, (16), 9 states have call successors, (9), 6 states have call predecessors, (9), 9 states have return successors, (16), 11 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:29,317 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 41 transitions.
[2025-04-28 21:21:29,317 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 41 transitions. Word has length 30
[2025-04-28 21:21:29,317 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,318 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 41 transitions.
[2025-04-28 21:21:29,318 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, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:21:29,318 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 41 transitions.
[2025-04-28 21:21:29,319 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:29,319 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,319 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,325 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:29,523 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:29,524 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,524 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,524 INFO  L85        PathProgramCache]: Analyzing trace with hash -1623937109, now seen corresponding path program 1 times
[2025-04-28 21:21:29,524 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,524 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2107520178]
[2025-04-28 21:21:29,525 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,525 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,532 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:29,538 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,538 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,538 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,575 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,575 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,576 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2107520178]
[2025-04-28 21:21:29,576 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2107520178] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,576 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [478556048]
[2025-04-28 21:21:29,576 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,576 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,578 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,581 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,590 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,659 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:29,682 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,682 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,682 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,683 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,685 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,708 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,708 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:29,708 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [478556048] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,709 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:29,709 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:21:29,709 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1713990122]
[2025-04-28 21:21:29,709 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,709 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:29,709 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,710 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:29,710 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:29,710 INFO  L87              Difference]: Start difference. First operand 32 states and 41 transitions. Second operand  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 2 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 2 states have call successors, (8)
[2025-04-28 21:21:29,733 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,733 INFO  L93              Difference]: Finished difference Result 36 states and 45 transitions.
[2025-04-28 21:21:29,733 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:29,734 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), 2 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 2 states have call successors, (8) Word has length 30
[2025-04-28 21:21:29,734 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,735 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:29,735 INFO  L226             Difference]: Without dead ends: 36
[2025-04-28 21:21:29,735 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 29 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:29,736 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 1 mSDsluCounter, 47 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 77 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:29,736 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 77 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:29,737 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 36 states.
[2025-04-28 21:21:29,745 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 36 to 36.
[2025-04-28 21:21:29,746 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 15 states have (on average 1.2) internal successors, (18), 18 states have internal predecessors, (18), 9 states have call successors, (9), 6 states have call predecessors, (9), 11 states have return successors, (18), 11 states have call predecessors, (18), 9 states have call successors, (18)
[2025-04-28 21:21:29,748 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 45 transitions.
[2025-04-28 21:21:29,748 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 45 transitions. Word has length 30
[2025-04-28 21:21:29,748 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,748 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 45 transitions.
[2025-04-28 21:21:29,748 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), 2 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 2 states have call successors, (8)
[2025-04-28 21:21:29,748 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 45 transitions.
[2025-04-28 21:21:29,752 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:21:29,753 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,753 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:29,759 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:29,953 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,954 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,954 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,954 INFO  L85        PathProgramCache]: Analyzing trace with hash -389538591, now seen corresponding path program 1 times
[2025-04-28 21:21:29,954 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,955 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [623254007]
[2025-04-28 21:21:29,955 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,955 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,964 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:29,969 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:29,969 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,969 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,018 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 10 proven. 9 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-04-28 21:21:30,018 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,018 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [623254007]
[2025-04-28 21:21:30,018 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [623254007] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,018 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1582536849]
[2025-04-28 21:21:30,019 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,019 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,021 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,024 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:30,028 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:30,085 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:30,114 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:30,114 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,114 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,116 INFO  L256         TraceCheckSpWp]: Trace formula consists of 181 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:30,117 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,129 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 20 proven. 0 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:30,130 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:30,130 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1582536849] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,130 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:30,130 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 4
[2025-04-28 21:21:30,131 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1314945087]
[2025-04-28 21:21:30,131 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,131 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:30,131 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,132 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:30,132 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:30,132 INFO  L87              Difference]: Start difference. First operand 36 states and 45 transitions. Second operand  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:30,147 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,147 INFO  L93              Difference]: Finished difference Result 36 states and 43 transitions.
[2025-04-28 21:21:30,148 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:30,148 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11) Word has length 45
[2025-04-28 21:21:30,149 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,151 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:30,151 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:30,152 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 48 GetRequests, 46 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:30,152 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 1 mSDsluCounter, 47 mSDsCounter, 0 mSdLazyCounter, 5 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 77 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:30,153 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 77 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:30,156 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:30,163 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:21:30,163 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 9 states have call successors, (9), 6 states have call predecessors, (9), 9 states have return successors, (16), 11 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:30,164 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 39 transitions.
[2025-04-28 21:21:30,164 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 39 transitions. Word has length 45
[2025-04-28 21:21:30,164 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,164 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 39 transitions.
[2025-04-28 21:21:30,164 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:30,164 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 39 transitions.
[2025-04-28 21:21:30,165 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 61
[2025-04-28 21:21:30,165 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,166 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:30,171 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:30,366 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:30,366 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,367 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,367 INFO  L85        PathProgramCache]: Analyzing trace with hash 1904131543, now seen corresponding path program 2 times
[2025-04-28 21:21:30,367 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,367 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [908576227]
[2025-04-28 21:21:30,367 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:30,367 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,387 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:30,415 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:30,419 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:30,419 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,949 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 13 proven. 34 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:30,949 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,949 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [908576227]
[2025-04-28 21:21:30,950 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [908576227] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,950 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1181160211]
[2025-04-28 21:21:30,950 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:30,950 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,953 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,956 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:30,960 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,028 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:31,076 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:31,076 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:31,076 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,078 INFO  L256         TraceCheckSpWp]: Trace formula consists of 250 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,081 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,356 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 31 proven. 22 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:31,357 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:36,675 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 31 proven. 22 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:36,676 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1181160211] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:36,676 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:36,676 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 12, 12] total 19
[2025-04-28 21:21:36,676 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [88991094]
[2025-04-28 21:21:36,676 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,677 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:36,677 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,678 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:36,678 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=56, Invalid=286, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:36,678 INFO  L87              Difference]: Start difference. First operand 32 states and 39 transitions. Second operand  has 19 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 17 states have internal predecessors, (27), 12 states have call successors, (24), 1 states have call predecessors, (24), 11 states have return successors, (30), 18 states have call predecessors, (30), 12 states have call successors, (30)
[2025-04-28 21:21:37,216 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,216 INFO  L93              Difference]: Finished difference Result 63 states and 99 transitions.
[2025-04-28 21:21:37,216 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-04-28 21:21:37,217 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 17 states have internal predecessors, (27), 12 states have call successors, (24), 1 states have call predecessors, (24), 11 states have return successors, (30), 18 states have call predecessors, (30), 12 states have call successors, (30) Word has length 60
[2025-04-28 21:21:37,217 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,218 INFO  L225             Difference]: With dead ends: 63
[2025-04-28 21:21:37,218 INFO  L226             Difference]: Without dead ends: 63
[2025-04-28 21:21:37,219 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 141 GetRequests, 108 SyntacticMatches, 5 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 175 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=160, Invalid=710, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:37,220 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 24 mSDsluCounter, 348 mSDsCounter, 0 mSdLazyCounter, 246 mSolverCounterSat, 66 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 390 SdHoareTripleChecker+Invalid, 312 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 66 IncrementalHoareTripleChecker+Valid, 246 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,220 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 390 Invalid, 312 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [66 Valid, 246 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:37,221 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 63 states.
[2025-04-28 21:21:37,230 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 63 to 61.
[2025-04-28 21:21:37,231 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 61 states, 25 states have (on average 1.12) internal successors, (28), 28 states have internal predecessors, (28), 18 states have call successors, (18), 10 states have call predecessors, (18), 17 states have return successors, (49), 22 states have call predecessors, (49), 18 states have call successors, (49)
[2025-04-28 21:21:37,232 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 61 states to 61 states and 95 transitions.
[2025-04-28 21:21:37,232 INFO  L79                 Accepts]: Start accepts. Automaton has 61 states and 95 transitions. Word has length 60
[2025-04-28 21:21:37,233 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,233 INFO  L485      AbstractCegarLoop]: Abstraction has 61 states and 95 transitions.
[2025-04-28 21:21:37,233 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 17 states have internal predecessors, (27), 12 states have call successors, (24), 1 states have call predecessors, (24), 11 states have return successors, (30), 18 states have call predecessors, (30), 12 states have call successors, (30)
[2025-04-28 21:21:37,233 INFO  L278                IsEmpty]: Start isEmpty. Operand 61 states and 95 transitions.
[2025-04-28 21:21:37,238 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 181
[2025-04-28 21:21:37,239 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,239 INFO  L218           NwaCegarLoop]: trace histogram [23, 12, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,244 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:37,442 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:37,443 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,443 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,443 INFO  L85        PathProgramCache]: Analyzing trace with hash -140229545, now seen corresponding path program 3 times
[2025-04-28 21:21:37,443 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,443 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [825886446]
[2025-04-28 21:21:37,444 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:37,444 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,477 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 180 statements into 14 equivalence classes.
[2025-04-28 21:21:37,582 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s) and asserted 131 of 180 statements.
[2025-04-28 21:21:37,582 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s)
[2025-04-28 21:21:37,582 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,121 INFO  L134       CoverageAnalysis]: Checked inductivity of 1254 backedges. 394 proven. 74 refuted. 0 times theorem prover too weak. 786 trivial. 0 not checked.
[2025-04-28 21:21:39,121 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,121 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [825886446]
[2025-04-28 21:21:39,122 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [825886446] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,122 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [637481902]
[2025-04-28 21:21:39,122 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:39,122 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,125 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,127 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:39,131 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,266 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 180 statements into 14 equivalence classes.
[2025-04-28 21:21:39,370 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s) and asserted 131 of 180 statements.
[2025-04-28 21:21:39,370 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s)
[2025-04-28 21:21:39,370 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,378 INFO  L256         TraceCheckSpWp]: Trace formula consists of 581 conjuncts, 41 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,388 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,939 INFO  L134       CoverageAnalysis]: Checked inductivity of 1254 backedges. 393 proven. 72 refuted. 0 times theorem prover too weak. 789 trivial. 0 not checked.
[2025-04-28 21:21:39,939 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,773 INFO  L134       CoverageAnalysis]: Checked inductivity of 1254 backedges. 391 proven. 80 refuted. 0 times theorem prover too weak. 783 trivial. 0 not checked.
[2025-04-28 21:21:50,773 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [637481902] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,773 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,773 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 14, 17] total 22
[2025-04-28 21:21:50,774 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [560688164]
[2025-04-28 21:21:50,774 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,775 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:50,775 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,775 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:50,776 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=71, Invalid=391, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:50,776 INFO  L87              Difference]: Start difference. First operand 61 states and 95 transitions. Second operand  has 22 states, 11 states have (on average 3.090909090909091) internal successors, (34), 21 states have internal predecessors, (34), 13 states have call successors, (33), 1 states have call predecessors, (33), 11 states have return successors, (40), 19 states have call predecessors, (40), 13 states have call successors, (40)
[2025-04-28 21:21:51,208 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,208 INFO  L93              Difference]: Finished difference Result 83 states and 126 transitions.
[2025-04-28 21:21:51,209 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:51,209 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 3.090909090909091) internal successors, (34), 21 states have internal predecessors, (34), 13 states have call successors, (33), 1 states have call predecessors, (33), 11 states have return successors, (40), 19 states have call predecessors, (40), 13 states have call successors, (40) Word has length 180
[2025-04-28 21:21:51,210 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,211 INFO  L225             Difference]: With dead ends: 83
[2025-04-28 21:21:51,211 INFO  L226             Difference]: Without dead ends: 83
[2025-04-28 21:21:51,213 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 383 GetRequests, 351 SyntacticMatches, 5 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 163 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=150, Invalid=662, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:21:51,214 INFO  L437           NwaCegarLoop]: 33 mSDtfsCounter, 15 mSDsluCounter, 265 mSDsCounter, 0 mSdLazyCounter, 197 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 298 SdHoareTripleChecker+Invalid, 238 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 197 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,215 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 298 Invalid, 238 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 197 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:51,215 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 83 states.
[2025-04-28 21:21:51,229 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 83 to 79.
[2025-04-28 21:21:51,230 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 33 states have (on average 1.0303030303030303) internal successors, (34), 32 states have internal predecessors, (34), 26 states have call successors, (26), 16 states have call predecessors, (26), 19 states have return successors, (59), 30 states have call predecessors, (59), 26 states have call successors, (59)
[2025-04-28 21:21:51,232 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 119 transitions.
[2025-04-28 21:21:51,232 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 119 transitions. Word has length 180
[2025-04-28 21:21:51,233 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,233 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 119 transitions.
[2025-04-28 21:21:51,233 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 3.090909090909091) internal successors, (34), 21 states have internal predecessors, (34), 13 states have call successors, (33), 1 states have call predecessors, (33), 11 states have return successors, (40), 19 states have call predecessors, (40), 13 states have call successors, (40)
[2025-04-28 21:21:51,233 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 119 transitions.
[2025-04-28 21:21:51,236 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 151
[2025-04-28 21:21:51,236 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,236 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:51,243 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:51,437 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:51,437 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,438 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,438 INFO  L85        PathProgramCache]: Analyzing trace with hash -419005189, now seen corresponding path program 4 times
[2025-04-28 21:21:51,438 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,438 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [848161021]
[2025-04-28 21:21:51,438 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:51,438 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,456 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 150 statements into 2 equivalence classes.
[2025-04-28 21:21:51,494 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 150 of 150 statements.
[2025-04-28 21:21:51,494 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:51,494 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,621 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 140 proven. 194 refuted. 0 times theorem prover too weak. 503 trivial. 0 not checked.
[2025-04-28 21:21:52,622 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,622 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [848161021]
[2025-04-28 21:21:52,622 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [848161021] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,622 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1277131374]
[2025-04-28 21:21:52,622 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:52,622 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,625 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,627 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:52,630 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,836 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 150 statements into 2 equivalence classes.
[2025-04-28 21:21:52,939 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 150 of 150 statements.
[2025-04-28 21:21:52,940 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:52,940 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,944 INFO  L256         TraceCheckSpWp]: Trace formula consists of 664 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,951 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,389 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 73 proven. 206 refuted. 0 times theorem prover too weak. 558 trivial. 0 not checked.
[2025-04-28 21:21:53,390 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
