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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:28,103 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:28,182 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b563c3d1-2252-492a-a6f6-761d4134575f/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:28,191 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:28,194 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:28,226 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:28,226 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:28,227 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:28,227 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:28,227 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:28,227 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:28,228 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:28,228 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:28,228 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:28,228 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:28,228 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:28,228 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:28,228 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:28,228 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:28,229 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:28,229 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:28,229 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:28,229 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:28,231 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:28,231 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:28,232 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:28,232 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:28,567 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:28,580 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:28,583 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:28,585 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:28,586 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:28,589 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b563c3d1-2252-492a-a6f6-761d4134575f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-141.smt2
[2025-04-28 21:21:28,591 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:28,594 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:28,932 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b563c3d1-2252-492a-a6f6-761d4134575f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-141.smt2
[2025-04-28 21:21:28,936 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:28,939 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:28,940 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:28,941 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:28,941 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:28,944 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,999 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28 Unit
[2025-04-28 21:21:29,001 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:29,002 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:29,002 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:29,002 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:29,021 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,022 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,051 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,052 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,057 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,059 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,061 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,063 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,064 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,080 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:29,081 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:29,081 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:29,081 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:29,082 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:29,085 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:29,099 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,115 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:29,120 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:29,132 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:29,132 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:29,133 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:29,133 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fail.DLRunknown.CLN30 given in one single declaration
[2025-04-28 21:21:29,133 INFO  L130     BoogieDeclarations]: Found specification of procedure fail.DLRunknown.CLN30
[2025-04-28 21:21:29,133 INFO  L138     BoogieDeclarations]: Found implementation of procedure fail.DLRunknown.CLN30
[2025-04-28 21:21:29,133 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure ack_1030.DLRunknown.CLN17 given in one single declaration
[2025-04-28 21:21:29,133 INFO  L130     BoogieDeclarations]: Found specification of procedure ack_1030.DLRunknown.CLN17
[2025-04-28 21:21:29,133 INFO  L138     BoogieDeclarations]: Found implementation of procedure ack_1030.DLRunknown.CLN17
[2025-04-28 21:21:29,133 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure ack_without_checking_1087.DLRunknown.CLN26 given in one single declaration
[2025-04-28 21:21:29,134 INFO  L130     BoogieDeclarations]: Found specification of procedure ack_without_checking_1087.DLRunknown.CLN26
[2025-04-28 21:21:29,134 INFO  L138     BoogieDeclarations]: Found implementation of procedure ack_without_checking_1087.DLRunknown.CLN26
[2025-04-28 21:21:29,134 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main_1033.DLRunknown.CLN37 given in one single declaration
[2025-04-28 21:21:29,134 INFO  L130     BoogieDeclarations]: Found specification of procedure main_1033.DLRunknown.CLN37
[2025-04-28 21:21:29,134 INFO  L138     BoogieDeclarations]: Found implementation of procedure main_1033.DLRunknown.CLN37
[2025-04-28 21:21:29,134 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure ack_1030.DLRunknown.CLN8 given in one single declaration
[2025-04-28 21:21:29,134 INFO  L130     BoogieDeclarations]: Found specification of procedure ack_1030.DLRunknown.CLN8
[2025-04-28 21:21:29,134 INFO  L138     BoogieDeclarations]: Found implementation of procedure ack_1030.DLRunknown.CLN8
[2025-04-28 21:21:29,134 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure ack_1030.DLRunknown.CLN18 given in one single declaration
[2025-04-28 21:21:29,134 INFO  L130     BoogieDeclarations]: Found specification of procedure ack_1030.DLRunknown.CLN18
[2025-04-28 21:21:29,135 INFO  L138     BoogieDeclarations]: Found implementation of procedure ack_1030.DLRunknown.CLN18
[2025-04-28 21:21:29,135 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure ack_1030.DLRunknown.CLN9 given in one single declaration
[2025-04-28 21:21:29,135 INFO  L130     BoogieDeclarations]: Found specification of procedure ack_1030.DLRunknown.CLN9
[2025-04-28 21:21:29,135 INFO  L138     BoogieDeclarations]: Found implementation of procedure ack_1030.DLRunknown.CLN9
[2025-04-28 21:21:29,135 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure ack_without_checking_1087.DLRunknown.CLN27 given in one single declaration
[2025-04-28 21:21:29,135 INFO  L130     BoogieDeclarations]: Found specification of procedure ack_without_checking_1087.DLRunknown.CLN27
[2025-04-28 21:21:29,135 INFO  L138     BoogieDeclarations]: Found implementation of procedure ack_without_checking_1087.DLRunknown.CLN27
[2025-04-28 21:21:29,135 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:29,135 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:29,136 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:29,225 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:29,228 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:29,549 INFO  L?                        ?]: Removed 83 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:29,549 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:29,571 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:29,573 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:29,573 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:29 BoogieIcfgContainer
[2025-04-28 21:21:29,573 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:29,577 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:29,577 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:29,582 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:29,582 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:28" (1/3) ...
[2025-04-28 21:21:29,583 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7cb7729c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:29, skipping insertion in model container
[2025-04-28 21:21:29,583 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (2/3) ...
[2025-04-28 21:21:29,583 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7cb7729c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:29, skipping insertion in model container
[2025-04-28 21:21:29,583 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:29" (3/3) ...
[2025-04-28 21:21:29,585 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:29,600 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:29,603 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 10 procedures, 55 locations, 102 edges, 10 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:29,656 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:29,670 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;@5c16d7b9, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:29,671 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:29,676 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 55 states, 19 states have (on average 1.4210526315789473) internal successors, (27), 27 states have internal predecessors, (27), 25 states have call successors, (25), 9 states have call predecessors, (25), 9 states have return successors, (25), 18 states have call predecessors, (25), 25 states have call successors, (25)
[2025-04-28 21:21:29,689 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:29,689 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,690 INFO  L218           NwaCegarLoop]: trace histogram [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,691 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,697 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,698 INFO  L85        PathProgramCache]: Analyzing trace with hash 859608848, now seen corresponding path program 1 times
[2025-04-28 21:21:29,708 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,708 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1335039078]
[2025-04-28 21:21:29,708 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,709 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,756 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:29,821 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:29,821 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,822 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,684 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:30,684 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,685 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1335039078]
[2025-04-28 21:21:30,685 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1335039078] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,685 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:30,689 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:30,691 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1525111414]
[2025-04-28 21:21:30,692 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,697 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:30,700 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,766 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:30,769 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:30,771 INFO  L87              Difference]: Start difference. First operand  has 55 states, 19 states have (on average 1.4210526315789473) internal successors, (27), 27 states have internal predecessors, (27), 25 states have call successors, (25), 9 states have call predecessors, (25), 9 states have return successors, (25), 18 states have call predecessors, (25), 25 states have call successors, (25) Second operand  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:31,055 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,056 INFO  L93              Difference]: Finished difference Result 57 states and 89 transitions.
[2025-04-28 21:21:31,058 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:31,060 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:31,060 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,073 INFO  L225             Difference]: With dead ends: 57
[2025-04-28 21:21:31,073 INFO  L226             Difference]: Without dead ends: 57
[2025-04-28 21:21:31,076 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:31,082 INFO  L437           NwaCegarLoop]: 62 mSDtfsCounter, 2 mSDsluCounter, 165 mSDsCounter, 0 mSdLazyCounter, 66 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 227 SdHoareTripleChecker+Invalid, 67 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 66 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,086 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 227 Invalid, 67 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 66 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:31,112 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 57 states.
[2025-04-28 21:21:31,152 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 57 to 57.
[2025-04-28 21:21:31,154 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 20 states have (on average 1.35) internal successors, (27), 27 states have internal predecessors, (27), 25 states have call successors, (25), 9 states have call predecessors, (25), 11 states have return successors, (37), 20 states have call predecessors, (37), 25 states have call successors, (37)
[2025-04-28 21:21:31,166 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 89 transitions.
[2025-04-28 21:21:31,167 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 89 transitions. Word has length 20
[2025-04-28 21:21:31,168 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,169 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 89 transitions.
[2025-04-28 21:21:31,169 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:31,169 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 89 transitions.
[2025-04-28 21:21:31,175 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:31,175 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,177 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,177 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:31,177 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,178 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,178 INFO  L85        PathProgramCache]: Analyzing trace with hash -810967959, now seen corresponding path program 1 times
[2025-04-28 21:21:31,178 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,179 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [79735085]
[2025-04-28 21:21:31,179 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,179 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,209 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:31,229 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:31,229 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,230 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,323 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 7 proven. 0 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:31,323 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,323 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [79735085]
[2025-04-28 21:21:31,323 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [79735085] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:31,324 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:31,324 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:31,324 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1472527102]
[2025-04-28 21:21:31,324 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,325 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:31,325 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,326 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:31,326 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:31,326 INFO  L87              Difference]: Start difference. First operand 57 states and 89 transitions. Second operand  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 4 states have call successors, (9), 1 states have call predecessors, (9), 3 states have return successors, (9), 3 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:31,410 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,410 INFO  L93              Difference]: Finished difference Result 57 states and 87 transitions.
[2025-04-28 21:21:31,411 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:31,412 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), 4 states have call successors, (9), 1 states have call predecessors, (9), 3 states have return successors, (9), 3 states have call predecessors, (9), 4 states have call successors, (9) Word has length 40
[2025-04-28 21:21:31,412 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,415 INFO  L225             Difference]: With dead ends: 57
[2025-04-28 21:21:31,417 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:31,417 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:31,418 INFO  L437           NwaCegarLoop]: 70 mSDtfsCounter, 0 mSDsluCounter, 128 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 198 SdHoareTripleChecker+Invalid, 20 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,420 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 198 Invalid, 20 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:31,421 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:31,436 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 56.
[2025-04-28 21:21:31,438 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 20 states have (on average 1.3) internal successors, (26), 26 states have internal predecessors, (26), 24 states have call successors, (24), 9 states have call predecessors, (24), 11 states have return successors, (35), 20 states have call predecessors, (35), 24 states have call successors, (35)
[2025-04-28 21:21:31,441 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 85 transitions.
[2025-04-28 21:21:31,444 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 85 transitions. Word has length 40
[2025-04-28 21:21:31,445 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,445 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 85 transitions.
[2025-04-28 21:21:31,445 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), 4 states have call successors, (9), 1 states have call predecessors, (9), 3 states have return successors, (9), 3 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:31,445 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 85 transitions.
[2025-04-28 21:21:31,447 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:31,447 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,449 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,450 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:31,450 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,450 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,450 INFO  L85        PathProgramCache]: Analyzing trace with hash 1632606534, now seen corresponding path program 1 times
[2025-04-28 21:21:31,450 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,451 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1957133655]
[2025-04-28 21:21:31,451 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,451 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,474 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:31,499 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:31,500 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,501 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,295 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:32,295 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,296 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1957133655]
[2025-04-28 21:21:32,296 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1957133655] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:32,296 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1023600760]
[2025-04-28 21:21:32,296 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,296 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,299 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:32,304 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:32,306 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:32,398 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:32,481 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:32,481 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,481 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,485 INFO  L256         TraceCheckSpWp]: Trace formula consists of 335 conjuncts, 38 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:32,494 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,924 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:32,925 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:35,878 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:35,879 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1023600760] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:35,879 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:35,879 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 10
[2025-04-28 21:21:35,879 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2083415431]
[2025-04-28 21:21:35,879 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,880 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:35,880 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,881 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:35,881 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:35,881 INFO  L87              Difference]: Start difference. First operand 56 states and 85 transitions. Second operand  has 10 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 10 states have internal predecessors, (19), 7 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 6 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:36,100 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,100 INFO  L93              Difference]: Finished difference Result 60 states and 98 transitions.
[2025-04-28 21:21:36,102 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:36,103 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 10 states have internal predecessors, (19), 7 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 6 states have call predecessors, (12), 7 states have call successors, (12) Word has length 40
[2025-04-28 21:21:36,104 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,105 INFO  L225             Difference]: With dead ends: 60
[2025-04-28 21:21:36,109 INFO  L226             Difference]: Without dead ends: 60
[2025-04-28 21:21:36,109 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 86 GetRequests, 75 SyntacticMatches, 3 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 13 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:36,110 INFO  L437           NwaCegarLoop]: 58 mSDtfsCounter, 3 mSDsluCounter, 305 mSDsCounter, 0 mSdLazyCounter, 126 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 363 SdHoareTripleChecker+Invalid, 129 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 126 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,110 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 363 Invalid, 129 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 126 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:36,113 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 60 states.
[2025-04-28 21:21:36,127 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 60 to 56.
[2025-04-28 21:21:36,128 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 20 states have (on average 1.3) internal successors, (26), 26 states have internal predecessors, (26), 24 states have call successors, (24), 9 states have call predecessors, (24), 11 states have return successors, (35), 20 states have call predecessors, (35), 24 states have call successors, (35)
[2025-04-28 21:21:36,129 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 85 transitions.
[2025-04-28 21:21:36,130 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 85 transitions. Word has length 40
[2025-04-28 21:21:36,130 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,130 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 85 transitions.
[2025-04-28 21:21:36,130 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 10 states have internal predecessors, (19), 7 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 6 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:36,130 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 85 transitions.
[2025-04-28 21:21:36,134 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-04-28 21:21:36,134 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,134 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 5, 5, 3, 3, 3, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,139 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:36,335 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,335 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,336 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,336 INFO  L85        PathProgramCache]: Analyzing trace with hash 330514003, now seen corresponding path program 1 times
[2025-04-28 21:21:36,336 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,336 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1359779222]
[2025-04-28 21:21:36,336 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,337 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,356 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-04-28 21:21:36,363 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-04-28 21:21:36,363 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,363 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,473 INFO  L134       CoverageAnalysis]: Checked inductivity of 97 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 83 trivial. 0 not checked.
[2025-04-28 21:21:36,473 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,473 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1359779222]
[2025-04-28 21:21:36,474 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1359779222] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,474 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,474 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:36,474 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1367300358]
[2025-04-28 21:21:36,475 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,475 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:36,475 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,476 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:36,477 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:36,477 INFO  L87              Difference]: Start difference. First operand 56 states and 85 transitions. Second operand  has 4 states, 3 states have (on average 7.0) internal successors, (21), 4 states have internal predecessors, (21), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (15), 3 states have call predecessors, (15), 4 states have call successors, (15)
[2025-04-28 21:21:36,564 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,565 INFO  L93              Difference]: Finished difference Result 60 states and 96 transitions.
[2025-04-28 21:21:36,565 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:36,566 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.0) internal successors, (21), 4 states have internal predecessors, (21), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (15), 3 states have call predecessors, (15), 4 states have call successors, (15) Word has length 80
[2025-04-28 21:21:36,566 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,568 INFO  L225             Difference]: With dead ends: 60
[2025-04-28 21:21:36,570 INFO  L226             Difference]: Without dead ends: 60
[2025-04-28 21:21:36,570 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:36,571 INFO  L437           NwaCegarLoop]: 72 mSDtfsCounter, 1 mSDsluCounter, 121 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 193 SdHoareTripleChecker+Invalid, 40 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,571 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 193 Invalid, 40 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,572 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 60 states.
[2025-04-28 21:21:36,585 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 60 to 58.
[2025-04-28 21:21:36,586 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 58 states, 21 states have (on average 1.2857142857142858) internal successors, (27), 27 states have internal predecessors, (27), 24 states have call successors, (24), 9 states have call predecessors, (24), 12 states have return successors, (36), 21 states have call predecessors, (36), 24 states have call successors, (36)
[2025-04-28 21:21:36,587 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 87 transitions.
[2025-04-28 21:21:36,588 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 87 transitions. Word has length 80
[2025-04-28 21:21:36,589 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,590 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 87 transitions.
[2025-04-28 21:21:36,590 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.0) internal successors, (21), 4 states have internal predecessors, (21), 4 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (15), 3 states have call predecessors, (15), 4 states have call successors, (15)
[2025-04-28 21:21:36,590 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 87 transitions.
[2025-04-28 21:21:36,592 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-04-28 21:21:36,596 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,596 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 5, 5, 3, 3, 3, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,596 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:36,596 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,597 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,597 INFO  L85        PathProgramCache]: Analyzing trace with hash -1132963633, now seen corresponding path program 1 times
[2025-04-28 21:21:36,597 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,597 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [438431962]
[2025-04-28 21:21:36,597 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,597 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,621 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-04-28 21:21:36,633 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-04-28 21:21:36,633 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,633 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,821 INFO  L134       CoverageAnalysis]: Checked inductivity of 97 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 83 trivial. 0 not checked.
[2025-04-28 21:21:36,821 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,821 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [438431962]
[2025-04-28 21:21:36,823 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [438431962] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,823 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,823 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:36,823 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1032969540]
[2025-04-28 21:21:36,823 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,824 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:36,824 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,825 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:36,825 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:36,826 INFO  L87              Difference]: Start difference. First operand 58 states and 87 transitions. Second operand  has 6 states, 5 states have (on average 4.2) internal successors, (21), 6 states have internal predecessors, (21), 5 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (15), 5 states have call predecessors, (15), 5 states have call successors, (15)
[2025-04-28 21:21:36,905 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,908 INFO  L93              Difference]: Finished difference Result 68 states and 104 transitions.
[2025-04-28 21:21:36,908 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:36,909 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 4.2) internal successors, (21), 6 states have internal predecessors, (21), 5 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (15), 5 states have call predecessors, (15), 5 states have call successors, (15) Word has length 80
[2025-04-28 21:21:36,909 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,910 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:21:36,913 INFO  L226             Difference]: Without dead ends: 68
[2025-04-28 21:21:36,913 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 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:36,914 INFO  L437           NwaCegarLoop]: 75 mSDtfsCounter, 1 mSDsluCounter, 285 mSDsCounter, 0 mSdLazyCounter, 37 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 360 SdHoareTripleChecker+Invalid, 38 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 37 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,914 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 360 Invalid, 38 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 37 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,915 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 68 states.
[2025-04-28 21:21:36,925 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 68 to 63.
[2025-04-28 21:21:36,927 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 63 states, 23 states have (on average 1.2608695652173914) internal successors, (29), 29 states have internal predecessors, (29), 25 states have call successors, (25), 9 states have call predecessors, (25), 14 states have return successors, (43), 24 states have call predecessors, (43), 25 states have call successors, (43)
[2025-04-28 21:21:36,929 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 63 states to 63 states and 97 transitions.
[2025-04-28 21:21:36,931 INFO  L79                 Accepts]: Start accepts. Automaton has 63 states and 97 transitions. Word has length 80
[2025-04-28 21:21:36,932 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,932 INFO  L485      AbstractCegarLoop]: Abstraction has 63 states and 97 transitions.
[2025-04-28 21:21:36,933 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 4.2) internal successors, (21), 6 states have internal predecessors, (21), 5 states have call successors, (14), 1 states have call predecessors, (14), 5 states have return successors, (15), 5 states have call predecessors, (15), 5 states have call successors, (15)
[2025-04-28 21:21:36,933 INFO  L278                IsEmpty]: Start isEmpty. Operand 63 states and 97 transitions.
[2025-04-28 21:21:36,936 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 93
[2025-04-28 21:21:36,936 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,936 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 6, 6, 3, 3, 3, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,936 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:36,937 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,938 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,938 INFO  L85        PathProgramCache]: Analyzing trace with hash -650429208, now seen corresponding path program 1 times
[2025-04-28 21:21:36,938 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,939 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [532783365]
[2025-04-28 21:21:36,939 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,939 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,967 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-04-28 21:21:36,992 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-04-28 21:21:36,992 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,993 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,156 INFO  L134       CoverageAnalysis]: Checked inductivity of 138 backedges. 26 proven. 12 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:21:37,156 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,156 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [532783365]
[2025-04-28 21:21:37,156 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [532783365] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,156 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [123495471]
[2025-04-28 21:21:37,157 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,157 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,159 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,162 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:37,166 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,295 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-04-28 21:21:37,432 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-04-28 21:21:37,432 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,432 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,437 INFO  L256         TraceCheckSpWp]: Trace formula consists of 780 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,443 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,566 INFO  L134       CoverageAnalysis]: Checked inductivity of 138 backedges. 60 proven. 8 refuted. 0 times theorem prover too weak. 70 trivial. 0 not checked.
[2025-04-28 21:21:37,566 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:39,331 INFO  L134       CoverageAnalysis]: Checked inductivity of 138 backedges. 26 proven. 12 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:21:39,332 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [123495471] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:39,332 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:39,332 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 13
[2025-04-28 21:21:39,332 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2073155073]
[2025-04-28 21:21:39,333 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,333 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:39,334 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,334 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:39,335 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=27, Invalid=129, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:39,335 INFO  L87              Difference]: Start difference. First operand 63 states and 97 transitions. Second operand  has 13 states, 11 states have (on average 3.3636363636363638) internal successors, (37), 13 states have internal predecessors, (37), 7 states have call successors, (22), 2 states have call predecessors, (22), 11 states have return successors, (27), 9 states have call predecessors, (27), 7 states have call successors, (27)
[2025-04-28 21:21:39,890 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,890 INFO  L93              Difference]: Finished difference Result 107 states and 200 transitions.
[2025-04-28 21:21:39,890 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:39,891 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 11 states have (on average 3.3636363636363638) internal successors, (37), 13 states have internal predecessors, (37), 7 states have call successors, (22), 2 states have call predecessors, (22), 11 states have return successors, (27), 9 states have call predecessors, (27), 7 states have call successors, (27) Word has length 92
[2025-04-28 21:21:39,891 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,893 INFO  L225             Difference]: With dead ends: 107
[2025-04-28 21:21:39,894 INFO  L226             Difference]: Without dead ends: 107
[2025-04-28 21:21:39,894 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 190 GetRequests, 173 SyntacticMatches, 6 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 30 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=27, Invalid=129, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:39,895 INFO  L437           NwaCegarLoop]: 77 mSDtfsCounter, 8 mSDsluCounter, 523 mSDsCounter, 0 mSdLazyCounter, 401 mSolverCounterSat, 19 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 600 SdHoareTripleChecker+Invalid, 420 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 19 IncrementalHoareTripleChecker+Valid, 401 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,895 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 600 Invalid, 420 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [19 Valid, 401 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:39,898 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-04-28 21:21:39,923 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 91.
[2025-04-28 21:21:39,924 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 32 states have (on average 1.28125) internal successors, (41), 39 states have internal predecessors, (41), 39 states have call successors, (39), 13 states have call predecessors, (39), 19 states have return successors, (84), 38 states have call predecessors, (84), 39 states have call successors, (84)
[2025-04-28 21:21:39,926 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 164 transitions.
[2025-04-28 21:21:39,926 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 164 transitions. Word has length 92
[2025-04-28 21:21:39,926 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,926 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 164 transitions.
[2025-04-28 21:21:39,927 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 11 states have (on average 3.3636363636363638) internal successors, (37), 13 states have internal predecessors, (37), 7 states have call successors, (22), 2 states have call predecessors, (22), 11 states have return successors, (27), 9 states have call predecessors, (27), 7 states have call successors, (27)
[2025-04-28 21:21:39,927 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 164 transitions.
[2025-04-28 21:21:39,930 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 97
[2025-04-28 21:21:39,933 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,934 INFO  L218           NwaCegarLoop]: trace histogram [8, 6, 6, 6, 6, 6, 3, 3, 3, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,941 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:40,134 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,134 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,135 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,135 INFO  L85        PathProgramCache]: Analyzing trace with hash 1151355801, now seen corresponding path program 1 times
[2025-04-28 21:21:40,135 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,135 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [219436646]
[2025-04-28 21:21:40,135 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,135 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,154 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-04-28 21:21:40,171 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-04-28 21:21:40,171 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,171 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,376 INFO  L134       CoverageAnalysis]: Checked inductivity of 159 backedges. 26 proven. 6 refuted. 0 times theorem prover too weak. 127 trivial. 0 not checked.
[2025-04-28 21:21:40,376 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,376 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [219436646]
[2025-04-28 21:21:40,377 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [219436646] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,377 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1900906347]
[2025-04-28 21:21:40,377 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,377 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,380 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,382 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:40,386 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,511 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 96 statements into 1 equivalence classes.
[2025-04-28 21:21:40,640 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 96 of 96 statements.
[2025-04-28 21:21:40,640 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,640 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,645 INFO  L256         TraceCheckSpWp]: Trace formula consists of 819 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,649 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,773 INFO  L134       CoverageAnalysis]: Checked inductivity of 159 backedges. 63 proven. 4 refuted. 0 times theorem prover too weak. 92 trivial. 0 not checked.
[2025-04-28 21:21:40,773 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:42,743 INFO  L134       CoverageAnalysis]: Checked inductivity of 159 backedges. 26 proven. 6 refuted. 0 times theorem prover too weak. 127 trivial. 0 not checked.
[2025-04-28 21:21:42,744 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1900906347] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:42,744 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:42,744 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 12
[2025-04-28 21:21:42,744 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1646815303]
[2025-04-28 21:21:42,744 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,745 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:42,745 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,746 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:42,746 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=111, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:42,747 INFO  L87              Difference]: Start difference. First operand 91 states and 164 transitions. Second operand  has 12 states, 10 states have (on average 3.4) internal successors, (34), 12 states have internal predecessors, (34), 10 states have call successors, (23), 2 states have call predecessors, (23), 10 states have return successors, (27), 10 states have call predecessors, (27), 10 states have call successors, (27)
[2025-04-28 21:21:43,235 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,236 INFO  L93              Difference]: Finished difference Result 127 states and 289 transitions.
[2025-04-28 21:21:43,238 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:43,239 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 10 states have (on average 3.4) internal successors, (34), 12 states have internal predecessors, (34), 10 states have call successors, (23), 2 states have call predecessors, (23), 10 states have return successors, (27), 10 states have call predecessors, (27), 10 states have call successors, (27) Word has length 96
[2025-04-28 21:21:43,239 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,247 INFO  L225             Difference]: With dead ends: 127
[2025-04-28 21:21:43,247 INFO  L226             Difference]: Without dead ends: 127
[2025-04-28 21:21:43,248 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 206 GetRequests, 186 SyntacticMatches, 5 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=42, Invalid=230, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:43,248 INFO  L437           NwaCegarLoop]: 77 mSDtfsCounter, 2 mSDsluCounter, 660 mSDsCounter, 0 mSdLazyCounter, 309 mSolverCounterSat, 17 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 737 SdHoareTripleChecker+Invalid, 326 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 17 IncrementalHoareTripleChecker+Valid, 309 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,249 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 737 Invalid, 326 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [17 Valid, 309 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:43,250 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 127 states.
[2025-04-28 21:21:43,294 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 127 to 96.
[2025-04-28 21:21:43,295 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 96 states, 33 states have (on average 1.2727272727272727) internal successors, (42), 40 states have internal predecessors, (42), 42 states have call successors, (42), 13 states have call predecessors, (42), 20 states have return successors, (102), 42 states have call predecessors, (102), 42 states have call successors, (102)
[2025-04-28 21:21:43,299 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 96 states to 96 states and 186 transitions.
[2025-04-28 21:21:43,299 INFO  L79                 Accepts]: Start accepts. Automaton has 96 states and 186 transitions. Word has length 96
[2025-04-28 21:21:43,300 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,301 INFO  L485      AbstractCegarLoop]: Abstraction has 96 states and 186 transitions.
[2025-04-28 21:21:43,301 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 10 states have (on average 3.4) internal successors, (34), 12 states have internal predecessors, (34), 10 states have call successors, (23), 2 states have call predecessors, (23), 10 states have return successors, (27), 10 states have call predecessors, (27), 10 states have call successors, (27)
[2025-04-28 21:21:43,301 INFO  L278                IsEmpty]: Start isEmpty. Operand 96 states and 186 transitions.
[2025-04-28 21:21:43,304 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 117
[2025-04-28 21:21:43,306 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,307 INFO  L218           NwaCegarLoop]: trace histogram [10, 7, 7, 7, 7, 7, 4, 4, 4, 4, 2, 2, 2, 2, 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, 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:43,313 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:43,510 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,510 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,511 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,511 INFO  L85        PathProgramCache]: Analyzing trace with hash -387979121, now seen corresponding path program 1 times
[2025-04-28 21:21:43,511 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,511 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [437943944]
[2025-04-28 21:21:43,511 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,511 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,542 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 116 statements into 1 equivalence classes.
[2025-04-28 21:21:43,567 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 116 of 116 statements.
[2025-04-28 21:21:43,567 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,567 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,786 INFO  L134       CoverageAnalysis]: Checked inductivity of 250 backedges. 48 proven. 10 refuted. 0 times theorem prover too weak. 192 trivial. 0 not checked.
[2025-04-28 21:21:43,786 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,786 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [437943944]
[2025-04-28 21:21:43,786 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [437943944] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,786 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1902819976]
[2025-04-28 21:21:43,787 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,787 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,790 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,792 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:43,796 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,971 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 116 statements into 1 equivalence classes.
[2025-04-28 21:21:44,136 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 116 of 116 statements.
[2025-04-28 21:21:44,137 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,137 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,143 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1005 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,147 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,216 INFO  L134       CoverageAnalysis]: Checked inductivity of 250 backedges. 138 proven. 2 refuted. 0 times theorem prover too weak. 110 trivial. 0 not checked.
[2025-04-28 21:21:44,219 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,406 INFO  L134       CoverageAnalysis]: Checked inductivity of 250 backedges. 50 proven. 12 refuted. 0 times theorem prover too weak. 188 trivial. 0 not checked.
[2025-04-28 21:21:46,406 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1902819976] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,406 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,406 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [4, 6, 6] total 8
[2025-04-28 21:21:46,407 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1217541894]
[2025-04-28 21:21:46,407 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,408 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:46,409 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,409 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:46,409 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:46,410 INFO  L87              Difference]: Start difference. First operand 96 states and 186 transitions. Second operand  has 8 states, 5 states have (on average 7.0) internal successors, (35), 8 states have internal predecessors, (35), 6 states have call successors, (29), 2 states have call predecessors, (29), 5 states have return successors, (31), 7 states have call predecessors, (31), 6 states have call successors, (31)
[2025-04-28 21:21:46,680 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,681 INFO  L93              Difference]: Finished difference Result 110 states and 237 transitions.
[2025-04-28 21:21:46,681 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:46,681 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 7.0) internal successors, (35), 8 states have internal predecessors, (35), 6 states have call successors, (29), 2 states have call predecessors, (29), 5 states have return successors, (31), 7 states have call predecessors, (31), 6 states have call successors, (31) Word has length 116
[2025-04-28 21:21:46,682 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,684 INFO  L225             Difference]: With dead ends: 110
[2025-04-28 21:21:46,685 INFO  L226             Difference]: Without dead ends: 110
[2025-04-28 21:21:46,685 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 239 GetRequests, 228 SyntacticMatches, 3 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:46,686 INFO  L437           NwaCegarLoop]: 76 mSDtfsCounter, 3 mSDsluCounter, 308 mSDsCounter, 0 mSdLazyCounter, 225 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 384 SdHoareTripleChecker+Invalid, 234 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 225 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,686 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 384 Invalid, 234 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 225 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:46,687 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-04-28 21:21:46,705 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 102.
[2025-04-28 21:21:46,705 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 102 states, 35 states have (on average 1.2571428571428571) internal successors, (44), 42 states have internal predecessors, (44), 44 states have call successors, (44), 13 states have call predecessors, (44), 22 states have return successors, (118), 46 states have call predecessors, (118), 44 states have call successors, (118)
[2025-04-28 21:21:46,708 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 206 transitions.
[2025-04-28 21:21:46,708 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 206 transitions. Word has length 116
[2025-04-28 21:21:46,708 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,708 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 206 transitions.
[2025-04-28 21:21:46,709 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 7.0) internal successors, (35), 8 states have internal predecessors, (35), 6 states have call successors, (29), 2 states have call predecessors, (29), 5 states have return successors, (31), 7 states have call predecessors, (31), 6 states have call successors, (31)
[2025-04-28 21:21:46,709 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 206 transitions.
[2025-04-28 21:21:46,715 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 133
[2025-04-28 21:21:46,716 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,716 INFO  L218           NwaCegarLoop]: trace histogram [11, 8, 8, 8, 8, 8, 5, 5, 5, 5, 3, 3, 3, 3, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,724 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:46,917 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,917 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,917 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,917 INFO  L85        PathProgramCache]: Analyzing trace with hash 416330708, now seen corresponding path program 1 times
[2025-04-28 21:21:46,918 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,918 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [198277294]
[2025-04-28 21:21:46,918 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,918 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,937 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 132 statements into 1 equivalence classes.
[2025-04-28 21:21:46,973 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 132 of 132 statements.
[2025-04-28 21:21:46,976 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,976 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,431 INFO  L134       CoverageAnalysis]: Checked inductivity of 334 backedges. 56 proven. 7 refuted. 0 times theorem prover too weak. 271 trivial. 0 not checked.
[2025-04-28 21:21:47,432 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,432 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [198277294]
[2025-04-28 21:21:47,432 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [198277294] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,432 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1279628271]
[2025-04-28 21:21:47,432 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,432 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,435 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,438 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:47,442 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,633 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 132 statements into 1 equivalence classes.
[2025-04-28 21:21:47,810 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 132 of 132 statements.
[2025-04-28 21:21:47,811 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,811 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,817 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1152 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,822 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,929 INFO  L134       CoverageAnalysis]: Checked inductivity of 334 backedges. 162 proven. 0 refuted. 0 times theorem prover too weak. 172 trivial. 0 not checked.
[2025-04-28 21:21:47,929 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:47,930 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1279628271] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,930 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:47,930 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [7] total 12
[2025-04-28 21:21:47,930 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1760937428]
[2025-04-28 21:21:47,930 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,930 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:47,931 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,931 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:47,931 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=22, Invalid=110, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:47,932 INFO  L87              Difference]: Start difference. First operand 102 states and 206 transitions. Second operand  has 7 states, 6 states have (on average 5.333333333333333) internal successors, (32), 7 states have internal predecessors, (32), 5 states have call successors, (22), 2 states have call predecessors, (22), 6 states have return successors, (25), 7 states have call predecessors, (25), 5 states have call successors, (25)
[2025-04-28 21:21:48,158 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,158 INFO  L93              Difference]: Finished difference Result 112 states and 236 transitions.
[2025-04-28 21:21:48,159 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:48,159 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 5.333333333333333) internal successors, (32), 7 states have internal predecessors, (32), 5 states have call successors, (22), 2 states have call predecessors, (22), 6 states have return successors, (25), 7 states have call predecessors, (25), 5 states have call successors, (25) Word has length 132
[2025-04-28 21:21:48,159 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,162 INFO  L225             Difference]: With dead ends: 112
[2025-04-28 21:21:48,162 INFO  L226             Difference]: Without dead ends: 112
[2025-04-28 21:21:48,162 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 139 GetRequests, 128 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=26, Invalid=130, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:48,163 INFO  L437           NwaCegarLoop]: 69 mSDtfsCounter, 2 mSDsluCounter, 292 mSDsCounter, 0 mSdLazyCounter, 148 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 361 SdHoareTripleChecker+Invalid, 152 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 148 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,163 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 361 Invalid, 152 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 148 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:48,164 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-04-28 21:21:48,178 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 102.
[2025-04-28 21:21:48,178 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 102 states, 35 states have (on average 1.2571428571428571) internal successors, (44), 42 states have internal predecessors, (44), 44 states have call successors, (44), 13 states have call predecessors, (44), 22 states have return successors, (114), 46 states have call predecessors, (114), 44 states have call successors, (114)
[2025-04-28 21:21:48,180 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 102 states to 102 states and 202 transitions.
[2025-04-28 21:21:48,181 INFO  L79                 Accepts]: Start accepts. Automaton has 102 states and 202 transitions. Word has length 132
[2025-04-28 21:21:48,181 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,181 INFO  L485      AbstractCegarLoop]: Abstraction has 102 states and 202 transitions.
[2025-04-28 21:21:48,181 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 5.333333333333333) internal successors, (32), 7 states have internal predecessors, (32), 5 states have call successors, (22), 2 states have call predecessors, (22), 6 states have return successors, (25), 7 states have call predecessors, (25), 5 states have call successors, (25)
[2025-04-28 21:21:48,181 INFO  L278                IsEmpty]: Start isEmpty. Operand 102 states and 202 transitions.
[2025-04-28 21:21:48,202 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 137
[2025-04-28 21:21:48,203 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,203 INFO  L218           NwaCegarLoop]: trace histogram [12, 8, 8, 8, 8, 8, 5, 5, 5, 5, 3, 3, 3, 3, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,212 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:48,404 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,404 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,405 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,405 INFO  L85        PathProgramCache]: Analyzing trace with hash -463205307, now seen corresponding path program 2 times
[2025-04-28 21:21:48,405 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,405 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [441898993]
[2025-04-28 21:21:48,405 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:48,405 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,428 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 136 statements into 2 equivalence classes.
[2025-04-28 21:21:48,459 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 136 of 136 statements.
[2025-04-28 21:21:48,459 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,459 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,562 INFO  L134       CoverageAnalysis]: Checked inductivity of 367 backedges. 30 proven. 6 refuted. 0 times theorem prover too weak. 331 trivial. 0 not checked.
[2025-04-28 21:21:49,562 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,562 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [441898993]
[2025-04-28 21:21:49,562 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [441898993] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:49,562 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [824587496]
[2025-04-28 21:21:49,562 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:49,562 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,565 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,568 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:49,571 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,765 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 136 statements into 2 equivalence classes.
[2025-04-28 21:21:49,947 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 136 of 136 statements.
[2025-04-28 21:21:49,947 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:49,948 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,952 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1191 conjuncts, 35 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:49,956 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,164 INFO  L134       CoverageAnalysis]: Checked inductivity of 367 backedges. 30 proven. 6 refuted. 0 times theorem prover too weak. 331 trivial. 0 not checked.
[2025-04-28 21:21:50,164 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,770 INFO  L134       CoverageAnalysis]: Checked inductivity of 367 backedges. 30 proven. 6 refuted. 0 times theorem prover too weak. 331 trivial. 0 not checked.
[2025-04-28 21:21:51,770 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [824587496] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,770 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,770 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 10, 10] total 23
[2025-04-28 21:21:51,772 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1005679439]
[2025-04-28 21:21:51,772 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,773 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:51,773 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,774 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:51,774 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=49, Invalid=457, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:51,774 INFO  L87              Difference]: Start difference. First operand 102 states and 202 transitions. Second operand  has 23 states, 13 states have (on average 3.1538461538461537) internal successors, (41), 23 states have internal predecessors, (41), 17 states have call successors, (33), 1 states have call predecessors, (33), 13 states have return successors, (34), 16 states have call predecessors, (34), 17 states have call successors, (34)
[2025-04-28 21:21:54,012 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,012 INFO  L93              Difference]: Finished difference Result 265 states and 969 transitions.
[2025-04-28 21:21:54,012 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 31 states. 
[2025-04-28 21:21:54,013 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 13 states have (on average 3.1538461538461537) internal successors, (41), 23 states have internal predecessors, (41), 17 states have call successors, (33), 1 states have call predecessors, (33), 13 states have return successors, (34), 16 states have call predecessors, (34), 17 states have call successors, (34) Word has length 136
[2025-04-28 21:21:54,013 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,022 INFO  L225             Difference]: With dead ends: 265
[2025-04-28 21:21:54,023 INFO  L226             Difference]: Without dead ends: 238
[2025-04-28 21:21:54,024 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 306 GetRequests, 266 SyntacticMatches, 0 SemanticMatches, 40 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 194 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=183, Invalid=1539, Unknown=0, NotChecked=0, Total=1722
[2025-04-28 21:21:54,024 INFO  L437           NwaCegarLoop]: 101 mSDtfsCounter, 18 mSDsluCounter, 1543 mSDsCounter, 0 mSdLazyCounter, 1886 mSolverCounterSat, 57 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 41 SdHoareTripleChecker+Valid, 1644 SdHoareTripleChecker+Invalid, 1943 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 57 IncrementalHoareTripleChecker+Valid, 1886 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,025 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [41 Valid, 1644 Invalid, 1943 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [57 Valid, 1886 Invalid, 0 Unknown, 0 Unchecked, 1.7s Time]
[2025-04-28 21:21:54,026 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 238 states.
[2025-04-28 21:21:54,104 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 238 to 175.
[2025-04-28 21:21:54,106 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 175 states, 61 states have (on average 1.1967213114754098) internal successors, (73), 70 states have internal predecessors, (73), 71 states have call successors, (71), 19 states have call predecessors, (71), 42 states have return successors, (335), 85 states have call predecessors, (335), 71 states have call successors, (335)
[2025-04-28 21:21:54,112 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 175 states to 175 states and 479 transitions.
[2025-04-28 21:21:54,112 INFO  L79                 Accepts]: Start accepts. Automaton has 175 states and 479 transitions. Word has length 136
[2025-04-28 21:21:54,113 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,113 INFO  L485      AbstractCegarLoop]: Abstraction has 175 states and 479 transitions.
[2025-04-28 21:21:54,114 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 13 states have (on average 3.1538461538461537) internal successors, (41), 23 states have internal predecessors, (41), 17 states have call successors, (33), 1 states have call predecessors, (33), 13 states have return successors, (34), 16 states have call predecessors, (34), 17 states have call successors, (34)
[2025-04-28 21:21:54,114 INFO  L278                IsEmpty]: Start isEmpty. Operand 175 states and 479 transitions.
[2025-04-28 21:21:54,122 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 257
[2025-04-28 21:21:54,123 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,123 INFO  L218           NwaCegarLoop]: trace histogram [23, 15, 15, 15, 15, 15, 10, 10, 10, 10, 7, 7, 7, 7, 5, 5, 5, 5, 5, 3, 2, 2, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,130 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:54,323 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,323 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,324 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,324 INFO  L85        PathProgramCache]: Analyzing trace with hash 1459923118, now seen corresponding path program 1 times
[2025-04-28 21:21:54,324 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,324 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [327046061]
[2025-04-28 21:21:54,324 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,324 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,362 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 256 statements into 1 equivalence classes.
[2025-04-28 21:21:54,391 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 256 of 256 statements.
[2025-04-28 21:21:54,391 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,392 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,932 INFO  L134       CoverageAnalysis]: Checked inductivity of 1485 backedges. 64 proven. 3 refuted. 0 times theorem prover too weak. 1418 trivial. 0 not checked.
[2025-04-28 21:21:54,934 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,934 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [327046061]
[2025-04-28 21:21:54,934 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [327046061] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,934 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1739720678]
[2025-04-28 21:21:54,934 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,934 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,937 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,939 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:54,943 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,201 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 256 statements into 1 equivalence classes.
[2025-04-28 21:21:55,535 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 256 of 256 statements.
[2025-04-28 21:21:55,536 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,536 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,547 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2282 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,554 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,658 INFO  L134       CoverageAnalysis]: Checked inductivity of 1485 backedges. 751 proven. 2 refuted. 0 times theorem prover too weak. 732 trivial. 0 not checked.
[2025-04-28 21:21:55,658 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
