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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:40,537 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:40,635 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6524679d-81e3-429c-9163-2dd82793bcea/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:40,639 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:40,640 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:40,663 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:40,663 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:40,663 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:40,664 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:40,664 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:40,664 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:40,664 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:40,665 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:40,665 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:40,665 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:40,665 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:40,665 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:40,665 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:40,665 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,666 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:40,666 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:40,666 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:40,666 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:40,666 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:40,666 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:40,667 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:40,667 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:41,032 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:41,043 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:41,045 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:41,048 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:41,049 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:41,050 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6524679d-81e3-429c-9163-2dd82793bcea/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-199.smt2
[2025-04-28 21:21:41,052 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:41,055 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:41,423 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6524679d-81e3-429c-9163-2dd82793bcea/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-199.smt2
[2025-04-28 21:21:41,426 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:41,427 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:41,428 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:41,428 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:41,429 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:41,432 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,474 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41 Unit
[2025-04-28 21:21:41,474 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:41,475 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,476 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:41,476 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:41,493 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,494 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,529 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,529 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,537 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,539 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,543 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,545 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,546 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,573 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,574 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:41,574 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:41,574 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:41,576 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,579 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,592 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,606 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:41,609 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,620 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:41,620 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:41,620 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:41,620 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:41,620 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:41,621 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:41,621 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure step_lturn given in one single declaration
[2025-04-28 21:21:41,621 INFO  L130     BoogieDeclarations]: Found specification of procedure step_lturn
[2025-04-28 21:21:41,621 INFO  L138     BoogieDeclarations]: Found implementation of procedure step_lturn
[2025-04-28 21:21:41,621 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure combined_lturn given in one single declaration
[2025-04-28 21:21:41,621 INFO  L130     BoogieDeclarations]: Found specification of procedure combined_lturn
[2025-04-28 21:21:41,621 INFO  L138     BoogieDeclarations]: Found implementation of procedure combined_lturn
[2025-04-28 21:21:41,621 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure lturn given in one single declaration
[2025-04-28 21:21:41,621 INFO  L130     BoogieDeclarations]: Found specification of procedure lturn
[2025-04-28 21:21:41,621 INFO  L138     BoogieDeclarations]: Found implementation of procedure lturn
[2025-04-28 21:21:41,622 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:41,622 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:41,622 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:41,676 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:41,678 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:42,226 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:42,227 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:42,254 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:42,257 INFO  L312             CfgBuilder]: Removed 17 assume(true) statements.
[2025-04-28 21:21:42,258 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:42 BoogieIcfgContainer
[2025-04-28 21:21:42,258 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:42,264 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:42,264 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:42,270 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:42,273 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/3) ...
[2025-04-28 21:21:42,274 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1d1b763e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:42, skipping insertion in model container
[2025-04-28 21:21:42,274 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (2/3) ...
[2025-04-28 21:21:42,274 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1d1b763e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:42, skipping insertion in model container
[2025-04-28 21:21:42,274 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:42" (3/3) ...
[2025-04-28 21:21:42,276 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:42,293 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:42,296 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 6 procedures, 132 locations, 415 edges, 6 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:42,342 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:42,354 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;@1464be69, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:42,354 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:42,361 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 132 states, 10 states have (on average 2.5) internal successors, (25), 25 states have internal predecessors, (25), 118 states have call successors, (130), 5 states have call predecessors, (130), 5 states have return successors, (130), 102 states have call predecessors, (130), 118 states have call successors, (130)
[2025-04-28 21:21:42,398 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:42,398 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,399 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,399 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,405 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,406 INFO  L85        PathProgramCache]: Analyzing trace with hash 678912481, now seen corresponding path program 1 times
[2025-04-28 21:21:42,412 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,412 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [249866793]
[2025-04-28 21:21:42,413 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,413 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,455 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:42,624 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:42,624 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,624 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,183 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:43,184 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,185 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [249866793]
[2025-04-28 21:21:43,186 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [249866793] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,186 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [999392182]
[2025-04-28 21:21:43,186 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,186 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,189 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,193 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,196 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,256 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:43,396 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:43,396 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,397 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,402 INFO  L256         TraceCheckSpWp]: Trace formula consists of 391 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,409 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,513 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:43,514 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,800 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:43,801 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [999392182] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,801 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,804 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 6
[2025-04-28 21:21:43,806 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2068911712]
[2025-04-28 21:21:43,806 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,810 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:43,811 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,846 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:43,847 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:43,849 INFO  L87              Difference]: Start difference. First operand  has 132 states, 10 states have (on average 2.5) internal successors, (25), 25 states have internal predecessors, (25), 118 states have call successors, (130), 5 states have call predecessors, (130), 5 states have return successors, (130), 102 states have call predecessors, (130), 118 states have call successors, (130) Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:45,449 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,450 INFO  L93              Difference]: Finished difference Result 184 states and 583 transitions.
[2025-04-28 21:21:45,451 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:45,452 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 18
[2025-04-28 21:21:45,452 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,474 INFO  L225             Difference]: With dead ends: 184
[2025-04-28 21:21:45,474 INFO  L226             Difference]: Without dead ends: 184
[2025-04-28 21:21:45,478 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 42 GetRequests, 33 SyntacticMatches, 4 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:45,482 INFO  L437           NwaCegarLoop]: 237 mSDtfsCounter, 6 mSDsluCounter, 754 mSDsCounter, 0 mSdLazyCounter, 898 mSolverCounterSat, 77 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 44 SdHoareTripleChecker+Valid, 991 SdHoareTripleChecker+Invalid, 975 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 77 IncrementalHoareTripleChecker+Valid, 898 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,482 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [44 Valid, 991 Invalid, 975 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [77 Valid, 898 Invalid, 0 Unknown, 0 Unchecked, 1.4s Time]
[2025-04-28 21:21:45,498 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 184 states.
[2025-04-28 21:21:45,709 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 184 to 181.
[2025-04-28 21:21:45,710 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 181 states, 13 states have (on average 2.4615384615384617) internal successors, (32), 31 states have internal predecessors, (32), 163 states have call successors, (179), 7 states have call predecessors, (179), 8 states have return successors, (367), 143 states have call predecessors, (367), 163 states have call successors, (367)
[2025-04-28 21:21:45,725 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 181 states to 181 states and 578 transitions.
[2025-04-28 21:21:45,726 INFO  L79                 Accepts]: Start accepts. Automaton has 181 states and 578 transitions. Word has length 18
[2025-04-28 21:21:45,727 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,727 INFO  L485      AbstractCegarLoop]: Abstraction has 181 states and 578 transitions.
[2025-04-28 21:21:45,728 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:45,730 INFO  L278                IsEmpty]: Start isEmpty. Operand 181 states and 578 transitions.
[2025-04-28 21:21:45,747 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:45,747 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,748 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,754 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:45,952 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,952 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,953 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,953 INFO  L85        PathProgramCache]: Analyzing trace with hash 1475092919, now seen corresponding path program 1 times
[2025-04-28 21:21:45,953 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,953 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1762196462]
[2025-04-28 21:21:45,953 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,954 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,967 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:45,985 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:45,986 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,986 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,261 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:46,261 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,261 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1762196462]
[2025-04-28 21:21:46,261 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1762196462] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,261 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [222962088]
[2025-04-28 21:21:46,261 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,261 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,264 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,266 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:46,270 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,323 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:46,389 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:46,389 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,389 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,391 INFO  L256         TraceCheckSpWp]: Trace formula consists of 417 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,393 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,424 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:46,424 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,782 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:46,783 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [222962088] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,783 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,783 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 6
[2025-04-28 21:21:46,783 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [866445538]
[2025-04-28 21:21:46,783 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,784 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:46,784 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,784 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:46,785 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:46,785 INFO  L87              Difference]: Start difference. First operand 181 states and 578 transitions. Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:48,009 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,010 INFO  L93              Difference]: Finished difference Result 221 states and 877 transitions.
[2025-04-28 21:21:48,010 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:48,010 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:21:48,011 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,023 INFO  L225             Difference]: With dead ends: 221
[2025-04-28 21:21:48,023 INFO  L226             Difference]: Without dead ends: 221
[2025-04-28 21:21:48,023 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 39 SyntacticMatches, 5 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:48,024 INFO  L437           NwaCegarLoop]: 204 mSDtfsCounter, 6 mSDsluCounter, 619 mSDsCounter, 0 mSdLazyCounter, 917 mSolverCounterSat, 77 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 52 SdHoareTripleChecker+Valid, 823 SdHoareTripleChecker+Invalid, 994 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 77 IncrementalHoareTripleChecker+Valid, 917 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,025 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [52 Valid, 823 Invalid, 994 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [77 Valid, 917 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:21:48,025 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 221 states.
[2025-04-28 21:21:48,164 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 221 to 218.
[2025-04-28 21:21:48,165 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 218 states, 16 states have (on average 2.5) internal successors, (40), 38 states have internal predecessors, (40), 196 states have call successors, (216), 9 states have call predecessors, (216), 10 states have return successors, (615), 171 states have call predecessors, (615), 196 states have call successors, (615)
[2025-04-28 21:21:48,170 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 218 states to 218 states and 871 transitions.
[2025-04-28 21:21:48,170 INFO  L79                 Accepts]: Start accepts. Automaton has 218 states and 871 transitions. Word has length 21
[2025-04-28 21:21:48,171 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,171 INFO  L485      AbstractCegarLoop]: Abstraction has 218 states and 871 transitions.
[2025-04-28 21:21:48,171 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:48,171 INFO  L278                IsEmpty]: Start isEmpty. Operand 218 states and 871 transitions.
[2025-04-28 21:21:48,180 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:48,180 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,180 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,188 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:48,384 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,384 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,385 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,387 INFO  L85        PathProgramCache]: Analyzing trace with hash -78050031, now seen corresponding path program 1 times
[2025-04-28 21:21:48,388 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,388 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1681837666]
[2025-04-28 21:21:48,388 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,388 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,399 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:48,414 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:48,414 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,414 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,634 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:48,634 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,634 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1681837666]
[2025-04-28 21:21:48,634 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1681837666] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:48,634 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1406325193]
[2025-04-28 21:21:48,634 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,634 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,637 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,639 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:48,646 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,697 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:48,764 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:48,765 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,765 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,767 INFO  L256         TraceCheckSpWp]: Trace formula consists of 417 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,768 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,803 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:48,804 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:49,177 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:49,177 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1406325193] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:49,178 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:49,178 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 7
[2025-04-28 21:21:49,178 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1122149248]
[2025-04-28 21:21:49,178 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,178 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:49,179 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,179 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:49,179 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:49,179 INFO  L87              Difference]: Start difference. First operand 218 states and 871 transitions. Second operand  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:50,855 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,855 INFO  L93              Difference]: Finished difference Result 329 states and 1799 transitions.
[2025-04-28 21:21:50,855 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:50,856 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:21:50,856 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,882 INFO  L225             Difference]: With dead ends: 329
[2025-04-28 21:21:50,882 INFO  L226             Difference]: Without dead ends: 329
[2025-04-28 21:21:50,882 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 38 SyntacticMatches, 5 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:50,883 INFO  L437           NwaCegarLoop]: 235 mSDtfsCounter, 11 mSDsluCounter, 955 mSDsCounter, 0 mSdLazyCounter, 1232 mSolverCounterSat, 116 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 101 SdHoareTripleChecker+Valid, 1190 SdHoareTripleChecker+Invalid, 1348 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 116 IncrementalHoareTripleChecker+Valid, 1232 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,883 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [101 Valid, 1190 Invalid, 1348 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [116 Valid, 1232 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:21:50,885 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 329 states.
[2025-04-28 21:21:51,298 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 329 to 326.
[2025-04-28 21:21:51,301 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 326 states, 24 states have (on average 2.5833333333333335) internal successors, (62), 58 states have internal predecessors, (62), 294 states have call successors, (325), 14 states have call predecessors, (325), 15 states have return successors, (1404), 254 states have call predecessors, (1404), 294 states have call successors, (1404)
[2025-04-28 21:21:51,314 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 326 states to 326 states and 1791 transitions.
[2025-04-28 21:21:51,314 INFO  L79                 Accepts]: Start accepts. Automaton has 326 states and 1791 transitions. Word has length 21
[2025-04-28 21:21:51,314 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,314 INFO  L485      AbstractCegarLoop]: Abstraction has 326 states and 1791 transitions.
[2025-04-28 21:21:51,314 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:51,315 INFO  L278                IsEmpty]: Start isEmpty. Operand 326 states and 1791 transitions.
[2025-04-28 21:21:51,334 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:51,334 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,334 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,341 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:51,535 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,535 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,536 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,536 INFO  L85        PathProgramCache]: Analyzing trace with hash 1903371905, now seen corresponding path program 1 times
[2025-04-28 21:21:51,536 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,536 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1598635171]
[2025-04-28 21:21:51,536 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,536 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,545 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:51,559 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:51,559 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,559 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,735 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:51,736 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,736 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1598635171]
[2025-04-28 21:21:51,736 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1598635171] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:51,736 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [915511484]
[2025-04-28 21:21:51,736 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,736 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,739 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:51,741 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:51,745 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:51,795 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:51,857 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:51,857 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,857 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,859 INFO  L256         TraceCheckSpWp]: Trace formula consists of 417 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:51,861 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:51,890 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:51,890 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,218 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:52,218 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [915511484] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,218 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,218 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 6
[2025-04-28 21:21:52,218 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [215483636]
[2025-04-28 21:21:52,219 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,219 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:52,219 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,220 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:52,220 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:52,220 INFO  L87              Difference]: Start difference. First operand 326 states and 1791 transitions. Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:53,733 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,733 INFO  L93              Difference]: Finished difference Result 611 states and 4125 transitions.
[2025-04-28 21:21:53,734 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:53,734 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:21:53,734 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,806 INFO  L225             Difference]: With dead ends: 611
[2025-04-28 21:21:53,806 INFO  L226             Difference]: Without dead ends: 611
[2025-04-28 21:21:53,807 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 39 SyntacticMatches, 5 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:53,807 INFO  L437           NwaCegarLoop]: 244 mSDtfsCounter, 6 mSDsluCounter, 755 mSDsCounter, 0 mSdLazyCounter, 990 mSolverCounterSat, 90 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 87 SdHoareTripleChecker+Valid, 999 SdHoareTripleChecker+Invalid, 1080 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 90 IncrementalHoareTripleChecker+Valid, 990 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,808 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [87 Valid, 999 Invalid, 1080 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [90 Valid, 990 Invalid, 0 Unknown, 0 Unchecked, 1.4s Time]
[2025-04-28 21:21:53,809 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 611 states.
[2025-04-28 21:21:54,489 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 611 to 599.
[2025-04-28 21:21:54,493 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 599 states, 45 states have (on average 2.4) internal successors, (108), 99 states have internal predecessors, (108), 535 states have call successors, (586), 24 states have call predecessors, (586), 31 states have return successors, (3349), 476 states have call predecessors, (3349), 535 states have call successors, (3349)
[2025-04-28 21:21:54,525 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 599 states to 599 states and 4043 transitions.
[2025-04-28 21:21:54,525 INFO  L79                 Accepts]: Start accepts. Automaton has 599 states and 4043 transitions. Word has length 21
[2025-04-28 21:21:54,525 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,525 INFO  L485      AbstractCegarLoop]: Abstraction has 599 states and 4043 transitions.
[2025-04-28 21:21:54,526 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:54,526 INFO  L278                IsEmpty]: Start isEmpty. Operand 599 states and 4043 transitions.
[2025-04-28 21:21:54,549 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:54,549 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,549 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,556 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:54,750 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,750 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,751 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,752 INFO  L85        PathProgramCache]: Analyzing trace with hash 295084565, now seen corresponding path program 2 times
[2025-04-28 21:21:54,752 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,752 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [617049967]
[2025-04-28 21:21:54,752 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:54,752 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,766 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:21:54,783 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:54,783 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:54,783 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,982 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:54,982 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,982 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [617049967]
[2025-04-28 21:21:54,982 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [617049967] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,982 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [375061183]
[2025-04-28 21:21:54,982 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:54,982 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,987 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,993 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:54,994 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,053 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:21:55,118 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:55,118 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:55,118 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,120 INFO  L256         TraceCheckSpWp]: Trace formula consists of 443 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,121 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,169 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:55,170 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:55,597 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:55,598 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [375061183] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:55,598 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:55,598 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:55,598 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1300703595]
[2025-04-28 21:21:55,598 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,598 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:55,598 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,599 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:55,599 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:55,599 INFO  L87              Difference]: Start difference. First operand 599 states and 4043 transitions. Second operand  has 8 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:58,077 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,077 INFO  L93              Difference]: Finished difference Result 936 states and 7499 transitions.
[2025-04-28 21:21:58,078 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:58,078 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10) Word has length 24
[2025-04-28 21:21:58,079 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,165 INFO  L225             Difference]: With dead ends: 936
[2025-04-28 21:21:58,165 INFO  L226             Difference]: Without dead ends: 936
[2025-04-28 21:21:58,165 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 59 GetRequests, 44 SyntacticMatches, 6 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=25, Invalid=85, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:58,166 INFO  L437           NwaCegarLoop]: 301 mSDtfsCounter, 14 mSDsluCounter, 1306 mSDsCounter, 0 mSdLazyCounter, 1793 mSolverCounterSat, 246 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 128 SdHoareTripleChecker+Valid, 1607 SdHoareTripleChecker+Invalid, 2039 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 246 IncrementalHoareTripleChecker+Valid, 1793 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,166 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [128 Valid, 1607 Invalid, 2039 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [246 Valid, 1793 Invalid, 0 Unknown, 0 Unchecked, 2.3s Time]
[2025-04-28 21:21:58,168 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 936 states.
[2025-04-28 21:21:59,618 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 936 to 797.
[2025-04-28 21:21:59,623 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 797 states, 60 states have (on average 2.6333333333333333) internal successors, (158), 142 states have internal predecessors, (158), 717 states have call successors, (796), 38 states have call predecessors, (796), 39 states have return successors, (4908), 617 states have call predecessors, (4908), 717 states have call successors, (4908)
[2025-04-28 21:21:59,670 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 797 states to 797 states and 5862 transitions.
[2025-04-28 21:21:59,671 INFO  L79                 Accepts]: Start accepts. Automaton has 797 states and 5862 transitions. Word has length 24
[2025-04-28 21:21:59,671 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,671 INFO  L485      AbstractCegarLoop]: Abstraction has 797 states and 5862 transitions.
[2025-04-28 21:21:59,672 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:59,672 INFO  L278                IsEmpty]: Start isEmpty. Operand 797 states and 5862 transitions.
[2025-04-28 21:21:59,705 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:59,706 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,706 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,711 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:59,906 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,906 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,907 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,907 INFO  L85        PathProgramCache]: Analyzing trace with hash -1258058385, now seen corresponding path program 1 times
[2025-04-28 21:21:59,907 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,907 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1825282944]
[2025-04-28 21:21:59,907 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,907 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,916 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:59,933 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:59,933 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,933 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,125 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:00,127 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,127 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1825282944]
[2025-04-28 21:22:00,128 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1825282944] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,128 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1050111861]
[2025-04-28 21:22:00,128 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,128 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,131 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,133 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:22:00,136 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,190 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:00,262 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:00,263 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,263 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,265 INFO  L256         TraceCheckSpWp]: Trace formula consists of 443 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,266 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,299 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:00,299 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:00,705 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:00,706 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1050111861] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:00,706 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:00,706 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 7
[2025-04-28 21:22:00,706 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1472747791]
[2025-04-28 21:22:00,706 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,706 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:22:00,706 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,707 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:22:00,707 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:22:00,707 INFO  L87              Difference]: Start difference. First operand 797 states and 5862 transitions. Second operand  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 2 states have call successors, (7)
[2025-04-28 21:22:02,172 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,172 INFO  L93              Difference]: Finished difference Result 869 states and 6652 transitions.
[2025-04-28 21:22:02,173 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:02,173 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 2 states have call successors, (7) Word has length 24
[2025-04-28 21:22:02,173 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,272 INFO  L225             Difference]: With dead ends: 869
[2025-04-28 21:22:02,273 INFO  L226             Difference]: Without dead ends: 869
[2025-04-28 21:22:02,273 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 44 SyntacticMatches, 6 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:02,273 INFO  L437           NwaCegarLoop]: 219 mSDtfsCounter, 11 mSDsluCounter, 878 mSDsCounter, 0 mSdLazyCounter, 1151 mSolverCounterSat, 126 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 118 SdHoareTripleChecker+Valid, 1097 SdHoareTripleChecker+Invalid, 1277 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 126 IncrementalHoareTripleChecker+Valid, 1151 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,274 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [118 Valid, 1097 Invalid, 1277 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [126 Valid, 1151 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:22:02,275 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 869 states.
[2025-04-28 21:22:03,441 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 869 to 852.
[2025-04-28 21:22:03,446 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 852 states, 65 states have (on average 2.5076923076923077) internal successors, (163), 147 states have internal predecessors, (163), 762 states have call successors, (841), 38 states have call predecessors, (841), 44 states have return successors, (5452), 667 states have call predecessors, (5452), 762 states have call successors, (5452)
[2025-04-28 21:22:03,501 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 852 states to 852 states and 6456 transitions.
[2025-04-28 21:22:03,502 INFO  L79                 Accepts]: Start accepts. Automaton has 852 states and 6456 transitions. Word has length 24
[2025-04-28 21:22:03,502 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,502 INFO  L485      AbstractCegarLoop]: Abstraction has 852 states and 6456 transitions.
[2025-04-28 21:22:03,502 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 2 states have call successors, (7)
[2025-04-28 21:22:03,502 INFO  L278                IsEmpty]: Start isEmpty. Operand 852 states and 6456 transitions.
[2025-04-28 21:22:03,534 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:22:03,534 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,534 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,540 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:22:03,735 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:03,735 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,736 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,736 INFO  L85        PathProgramCache]: Analyzing trace with hash -248063069, now seen corresponding path program 2 times
[2025-04-28 21:22:03,736 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,736 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [539697295]
[2025-04-28 21:22:03,736 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:03,737 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,745 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:22:03,758 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:03,758 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:03,758 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,957 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:03,957 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,957 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [539697295]
[2025-04-28 21:22:03,957 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [539697295] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:03,958 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1909361402]
[2025-04-28 21:22:03,958 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:03,959 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:03,962 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:03,964 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:22:03,970 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:04,025 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:22:04,087 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:04,087 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:04,087 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,089 INFO  L256         TraceCheckSpWp]: Trace formula consists of 443 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:04,091 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:04,149 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:04,150 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:04,698 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:04,699 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1909361402] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:04,699 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:04,699 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 10
[2025-04-28 21:22:04,699 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [698869460]
[2025-04-28 21:22:04,699 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:04,699 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:22:04,699 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:04,700 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:22:04,700 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:22:04,701 INFO  L87              Difference]: Start difference. First operand 852 states and 6456 transitions. Second operand  has 10 states, 8 states have (on average 1.375) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (12), 9 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:22:06,192 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,193 INFO  L93              Difference]: Finished difference Result 592 states and 2361 transitions.
[2025-04-28 21:22:06,193 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:22:06,193 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 1.375) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (12), 9 states have call predecessors, (12), 3 states have call successors, (12) Word has length 24
[2025-04-28 21:22:06,193 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,196 INFO  L225             Difference]: With dead ends: 592
[2025-04-28 21:22:06,196 INFO  L226             Difference]: Without dead ends: 80
[2025-04-28 21:22:06,196 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 61 GetRequests, 43 SyntacticMatches, 6 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 6 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=149, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:22:06,197 INFO  L437           NwaCegarLoop]: 231 mSDtfsCounter, 20 mSDsluCounter, 1362 mSDsCounter, 0 mSdLazyCounter, 1441 mSolverCounterSat, 137 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 1593 SdHoareTripleChecker+Invalid, 1578 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 137 IncrementalHoareTripleChecker+Valid, 1441 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,197 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 1593 Invalid, 1578 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [137 Valid, 1441 Invalid, 0 Unknown, 0 Unchecked, 1.4s Time]
[2025-04-28 21:22:06,198 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 80 states.
[2025-04-28 21:22:06,235 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 80 to 62.
[2025-04-28 21:22:06,235 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 8 states have (on average 1.625) internal successors, (13), 13 states have internal predecessors, (13), 49 states have call successors, (56), 5 states have call predecessors, (56), 5 states have return successors, (54), 44 states have call predecessors, (54), 49 states have call successors, (54)
[2025-04-28 21:22:06,236 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 123 transitions.
[2025-04-28 21:22:06,236 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 123 transitions. Word has length 24
[2025-04-28 21:22:06,237 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,237 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 123 transitions.
[2025-04-28 21:22:06,238 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 1.375) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (12), 9 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:22:06,238 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 123 transitions.
[2025-04-28 21:22:06,240 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 51
[2025-04-28 21:22:06,241 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,241 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 5, 5, 5, 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:22:06,246 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:06,445 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable7
[2025-04-28 21:22:06,445 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,446 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,446 INFO  L85        PathProgramCache]: Analyzing trace with hash -746568598, now seen corresponding path program 1 times
[2025-04-28 21:22:06,446 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,446 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1629306018]
[2025-04-28 21:22:06,446 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,446 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,466 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 50 statements into 1 equivalence classes.
[2025-04-28 21:22:06,472 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 50 of 50 statements.
[2025-04-28 21:22:06,472 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,472 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,831 INFO  L134       CoverageAnalysis]: Checked inductivity of 93 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 73 trivial. 0 not checked.
[2025-04-28 21:22:06,832 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,832 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1629306018]
[2025-04-28 21:22:06,832 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1629306018] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:06,832 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [581892176]
[2025-04-28 21:22:06,832 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,832 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,835 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:06,837 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:06,840 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:22:06,924 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 50 statements into 1 equivalence classes.
[2025-04-28 21:22:07,091 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 50 of 50 statements.
[2025-04-28 21:22:07,092 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,092 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,099 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1231 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,101 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:07,158 INFO  L134       CoverageAnalysis]: Checked inductivity of 93 backedges. 30 proven. 0 refuted. 0 times theorem prover too weak. 63 trivial. 0 not checked.
[2025-04-28 21:22:07,158 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:07,158 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [581892176] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:07,159 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:07,159 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [5] total 8
[2025-04-28 21:22:07,159 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [673326681]
[2025-04-28 21:22:07,160 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,160 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:07,160 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,160 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:07,162 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=40, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:07,162 INFO  L87              Difference]: Start difference. First operand 62 states and 123 transitions. Second operand  has 5 states, 4 states have (on average 2.5) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 2 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:22:07,482 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,482 INFO  L93              Difference]: Finished difference Result 66 states and 170 transitions.
[2025-04-28 21:22:07,483 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:07,483 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 2.5) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 2 states have call predecessors, (11), 3 states have call successors, (11) Word has length 50
[2025-04-28 21:22:07,483 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,484 INFO  L225             Difference]: With dead ends: 66
[2025-04-28 21:22:07,484 INFO  L226             Difference]: Without dead ends: 66
[2025-04-28 21:22:07,484 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=16, Invalid=40, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:07,485 INFO  L437           NwaCegarLoop]: 106 mSDtfsCounter, 1 mSDsluCounter, 228 mSDsCounter, 0 mSdLazyCounter, 202 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 43 SdHoareTripleChecker+Valid, 334 SdHoareTripleChecker+Invalid, 212 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 202 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,485 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [43 Valid, 334 Invalid, 212 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 202 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:07,485 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-04-28 21:22:07,495 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 66.
[2025-04-28 21:22:07,496 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 66 states, 10 states have (on average 1.5) internal successors, (15), 15 states have internal predecessors, (15), 49 states have call successors, (56), 5 states have call predecessors, (56), 7 states have return successors, (99), 45 states have call predecessors, (99), 49 states have call successors, (99)
[2025-04-28 21:22:07,497 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 170 transitions.
[2025-04-28 21:22:07,497 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 170 transitions. Word has length 50
[2025-04-28 21:22:07,497 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,497 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 170 transitions.
[2025-04-28 21:22:07,497 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 2.5) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 2 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:22:07,497 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 170 transitions.
[2025-04-28 21:22:07,498 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 51
[2025-04-28 21:22:07,498 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,498 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 5, 5, 5, 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:22:07,510 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:22:07,699 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,699 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,699 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,699 INFO  L85        PathProgramCache]: Analyzing trace with hash -1119977789, now seen corresponding path program 1 times
[2025-04-28 21:22:07,699 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,700 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1517765038]
[2025-04-28 21:22:07,700 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,700 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,739 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 50 statements into 1 equivalence classes.
[2025-04-28 21:22:07,745 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 50 of 50 statements.
[2025-04-28 21:22:07,745 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,745 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,997 INFO  L134       CoverageAnalysis]: Checked inductivity of 93 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 73 trivial. 0 not checked.
[2025-04-28 21:22:07,997 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,997 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1517765038]
[2025-04-28 21:22:07,997 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1517765038] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,997 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1647758449]
[2025-04-28 21:22:07,997 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,997 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,999 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:08,001 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:08,005 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:08,083 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 50 statements into 1 equivalence classes.
[2025-04-28 21:22:08,258 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 50 of 50 statements.
[2025-04-28 21:22:08,258 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:08,258 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,263 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1231 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:08,265 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:08,315 INFO  L134       CoverageAnalysis]: Checked inductivity of 93 backedges. 30 proven. 0 refuted. 0 times theorem prover too weak. 63 trivial. 0 not checked.
[2025-04-28 21:22:08,315 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:08,315 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1647758449] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:08,315 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:08,315 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [5] total 8
[2025-04-28 21:22:08,315 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [755022967]
[2025-04-28 21:22:08,315 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,316 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:08,316 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,316 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:08,316 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=40, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:08,316 INFO  L87              Difference]: Start difference. First operand 66 states and 170 transitions. Second operand  has 5 states, 4 states have (on average 2.5) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 2 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:22:08,621 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:08,621 INFO  L93              Difference]: Finished difference Result 66 states and 164 transitions.
[2025-04-28 21:22:08,621 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:08,621 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 2.5) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 2 states have call predecessors, (11), 3 states have call successors, (11) Word has length 50
[2025-04-28 21:22:08,622 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,622 INFO  L225             Difference]: With dead ends: 66
[2025-04-28 21:22:08,622 INFO  L226             Difference]: Without dead ends: 66
[2025-04-28 21:22:08,623 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=16, Invalid=40, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:08,623 INFO  L437           NwaCegarLoop]: 108 mSDtfsCounter, 1 mSDsluCounter, 232 mSDsCounter, 0 mSdLazyCounter, 184 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 41 SdHoareTripleChecker+Valid, 340 SdHoareTripleChecker+Invalid, 194 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 184 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,623 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [41 Valid, 340 Invalid, 194 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 184 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:08,624 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-04-28 21:22:08,630 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 66.
[2025-04-28 21:22:08,631 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 66 states, 10 states have (on average 1.5) internal successors, (15), 15 states have internal predecessors, (15), 49 states have call successors, (56), 5 states have call predecessors, (56), 7 states have return successors, (93), 45 states have call predecessors, (93), 49 states have call successors, (93)
[2025-04-28 21:22:08,631 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 164 transitions.
[2025-04-28 21:22:08,631 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 164 transitions. Word has length 50
[2025-04-28 21:22:08,632 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,632 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 164 transitions.
[2025-04-28 21:22:08,632 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 2.5) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 2 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:22:08,632 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 164 transitions.
[2025-04-28 21:22:08,633 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 57
[2025-04-28 21:22:08,633 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,633 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 5, 3, 3, 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:22:08,639 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:08,837 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:08,837 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:08,838 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:08,838 INFO  L85        PathProgramCache]: Analyzing trace with hash -291678042, now seen corresponding path program 1 times
[2025-04-28 21:22:08,838 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:08,838 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1899533835]
[2025-04-28 21:22:08,838 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:08,838 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:08,860 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 56 statements into 1 equivalence classes.
[2025-04-28 21:22:08,874 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 56 of 56 statements.
[2025-04-28 21:22:08,874 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:08,874 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,184 INFO  L134       CoverageAnalysis]: Checked inductivity of 96 backedges. 0 proven. 38 refuted. 0 times theorem prover too weak. 58 trivial. 0 not checked.
[2025-04-28 21:22:09,184 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:09,184 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1899533835]
[2025-04-28 21:22:09,184 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1899533835] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:09,184 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1779045860]
[2025-04-28 21:22:09,184 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:09,185 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,187 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:09,189 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:09,192 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:09,307 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 56 statements into 1 equivalence classes.
[2025-04-28 21:22:09,478 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 56 of 56 statements.
[2025-04-28 21:22:09,478 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:09,478 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,483 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1283 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:09,485 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:09,513 INFO  L134       CoverageAnalysis]: Checked inductivity of 96 backedges. 51 proven. 4 refuted. 0 times theorem prover too weak. 41 trivial. 0 not checked.
[2025-04-28 21:22:09,513 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:10,010 INFO  L134       CoverageAnalysis]: Checked inductivity of 96 backedges. 0 proven. 38 refuted. 0 times theorem prover too weak. 58 trivial. 0 not checked.
[2025-04-28 21:22:10,010 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1779045860] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:10,010 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:10,010 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 7
[2025-04-28 21:22:10,010 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [557113740]
[2025-04-28 21:22:10,011 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:10,011 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:22:10,011 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:10,012 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:22:10,012 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:22:10,012 INFO  L87              Difference]: Start difference. First operand 66 states and 164 transitions. Second operand  has 7 states, 6 states have (on average 3.0) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (19), 2 states have call predecessors, (19), 6 states have return successors, (21), 6 states have call predecessors, (21), 3 states have call successors, (21)
[2025-04-28 21:22:10,714 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:10,714 INFO  L93              Difference]: Finished difference Result 117 states and 396 transitions.
[2025-04-28 21:22:10,714 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:10,715 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 3.0) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (19), 2 states have call predecessors, (19), 6 states have return successors, (21), 6 states have call predecessors, (21), 3 states have call successors, (21) Word has length 56
[2025-04-28 21:22:10,715 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:10,716 INFO  L225             Difference]: With dead ends: 117
[2025-04-28 21:22:10,716 INFO  L226             Difference]: Without dead ends: 117
[2025-04-28 21:22:10,717 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 120 GetRequests, 108 SyntacticMatches, 6 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:10,717 INFO  L437           NwaCegarLoop]: 122 mSDtfsCounter, 1 mSDsluCounter, 502 mSDsCounter, 0 mSdLazyCounter, 535 mSolverCounterSat, 52 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 46 SdHoareTripleChecker+Valid, 624 SdHoareTripleChecker+Invalid, 587 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 52 IncrementalHoareTripleChecker+Valid, 535 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:10,717 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [46 Valid, 624 Invalid, 587 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [52 Valid, 535 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:10,718 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-04-28 21:22:10,738 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 106.
[2025-04-28 21:22:10,739 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 106 states, 15 states have (on average 1.3333333333333333) internal successors, (20), 19 states have internal predecessors, (20), 81 states have call successors, (95), 8 states have call predecessors, (95), 11 states have return successors, (243), 78 states have call predecessors, (243), 81 states have call successors, (243)
[2025-04-28 21:22:10,740 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 358 transitions.
[2025-04-28 21:22:10,740 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 358 transitions. Word has length 56
[2025-04-28 21:22:10,741 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:10,741 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 358 transitions.
[2025-04-28 21:22:10,741 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 3.0) internal successors, (18), 6 states have internal predecessors, (18), 3 states have call successors, (19), 2 states have call predecessors, (19), 6 states have return successors, (21), 6 states have call predecessors, (21), 3 states have call successors, (21)
[2025-04-28 21:22:10,741 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 358 transitions.
[2025-04-28 21:22:10,743 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 86
[2025-04-28 21:22:10,743 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:10,743 INFO  L218           NwaCegarLoop]: trace histogram [11, 8, 7, 5, 5, 5, 5, 5, 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]
[2025-04-28 21:22:10,749 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
