./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-098.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:33,323 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:33,420 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_91cc884c-a42e-47be-b593-895ad0a0e223/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:33,428 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:33,428 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:33,463 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:33,464 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:33,464 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:33,466 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:33,466 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:33,466 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:33,467 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:33,467 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:33,467 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:33,467 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:33,468 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:33,469 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:33,469 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:33,469 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:33,469 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:33,469 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:33,469 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:33,469 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:33,469 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:33,469 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:33,470 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:33,470 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:33,816 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:33,832 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:33,835 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:33,836 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:33,837 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:33,840 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_91cc884c-a42e-47be-b593-895ad0a0e223/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-098.smt2
[2025-04-28 21:21:33,843 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:33,847 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:34,480 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_91cc884c-a42e-47be-b593-895ad0a0e223/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-098.smt2
[2025-04-28 21:21:34,483 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:34,485 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:34,485 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:34,486 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:34,486 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:34,489 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,553 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34 Unit
[2025-04-28 21:21:34,553 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:34,558 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:34,558 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:34,558 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:34,576 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,576 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,621 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,621 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,636 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,639 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,646 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,652 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,657 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,689 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:34,690 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:34,694 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:34,694 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:34,695 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,698 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:34,718 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,734 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:34,738 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:34,752 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:34,752 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:34,752 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:34,752 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:34,753 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:34,753 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:34,753 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcmainStart__sem given in one single declaration
[2025-04-28 21:21:34,753 INFO  L130     BoogieDeclarations]: Found specification of procedure funcmainStart__sem
[2025-04-28 21:21:34,753 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcmainStart__sem
[2025-04-28 21:21:34,753 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__sem given in one single declaration
[2025-04-28 21:21:34,753 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__sem
[2025-04-28 21:21:34,753 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__sem
[2025-04-28 21:21:34,753 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT1__sem given in one single declaration
[2025-04-28 21:21:34,753 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT1__sem
[2025-04-28 21:21:34,753 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT1__sem
[2025-04-28 21:21:34,753 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT4__sem given in one single declaration
[2025-04-28 21:21:34,753 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT4__sem
[2025-04-28 21:21:34,754 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT4__sem
[2025-04-28 21:21:34,754 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT10__sem given in one single declaration
[2025-04-28 21:21:34,754 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT10__sem
[2025-04-28 21:21:34,754 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT10__sem
[2025-04-28 21:21:34,754 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT11__sem given in one single declaration
[2025-04-28 21:21:34,754 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT11__sem
[2025-04-28 21:21:34,754 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT11__sem
[2025-04-28 21:21:34,754 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT8__sem given in one single declaration
[2025-04-28 21:21:34,754 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT8__sem
[2025-04-28 21:21:34,754 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT8__sem
[2025-04-28 21:21:34,754 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT7__sem given in one single declaration
[2025-04-28 21:21:34,754 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT7__sem
[2025-04-28 21:21:34,754 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT7__sem
[2025-04-28 21:21:34,757 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT3__sem given in one single declaration
[2025-04-28 21:21:34,758 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT3__sem
[2025-04-28 21:21:34,758 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT3__sem
[2025-04-28 21:21:34,758 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT5__sem given in one single declaration
[2025-04-28 21:21:34,758 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT5__sem
[2025-04-28 21:21:34,759 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT5__sem
[2025-04-28 21:21:34,759 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT6__sem given in one single declaration
[2025-04-28 21:21:34,759 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT6__sem
[2025-04-28 21:21:34,759 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT6__sem
[2025-04-28 21:21:34,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT9__sem given in one single declaration
[2025-04-28 21:21:34,760 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT9__sem
[2025-04-28 21:21:34,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT9__sem
[2025-04-28 21:21:34,760 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:34,760 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:34,760 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:35,017 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:35,019 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:35,842 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:35,842 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:35,863 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:35,864 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:35,864 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:35 BoogieIcfgContainer
[2025-04-28 21:21:35,864 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:35,871 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:35,874 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:35,879 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:35,880 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:34" (1/3) ...
[2025-04-28 21:21:35,880 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@21bdba35 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:35, skipping insertion in model container
[2025-04-28 21:21:35,881 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (2/3) ...
[2025-04-28 21:21:35,881 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@21bdba35 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:35, skipping insertion in model container
[2025-04-28 21:21:35,881 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:35" (3/3) ...
[2025-04-28 21:21:35,883 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:35,901 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:35,904 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 15 procedures, 129 locations, 311 edges, 15 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:35,966 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:35,978 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;@4687f70, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:35,979 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:35,983 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 129 states, 29 states have (on average 2.0344827586206895) internal successors, (59), 56 states have internal predecessors, (59), 84 states have call successors, (84), 14 states have call predecessors, (84), 14 states have return successors, (84), 59 states have call predecessors, (84), 84 states have call successors, (84)
[2025-04-28 21:21:36,002 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:36,002 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,006 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,006 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,012 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,013 INFO  L85        PathProgramCache]: Analyzing trace with hash 1067520239, now seen corresponding path program 1 times
[2025-04-28 21:21:36,020 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,020 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1554322417]
[2025-04-28 21:21:36,021 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,021 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,063 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:36,176 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:36,177 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,178 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,853 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:36,854 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,854 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1554322417]
[2025-04-28 21:21:36,855 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1554322417] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,855 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,858 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:36,861 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [758078831]
[2025-04-28 21:21:36,864 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,869 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:36,869 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,920 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:36,921 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:36,927 INFO  L87              Difference]: Start difference. First operand  has 129 states, 29 states have (on average 2.0344827586206895) internal successors, (59), 56 states have internal predecessors, (59), 84 states have call successors, (84), 14 states have call predecessors, (84), 14 states have return successors, (84), 59 states have call predecessors, (84), 84 states have call successors, (84) Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:37,611 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,612 INFO  L93              Difference]: Finished difference Result 133 states and 258 transitions.
[2025-04-28 21:21:37,613 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:37,615 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:37,615 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,628 INFO  L225             Difference]: With dead ends: 133
[2025-04-28 21:21:37,628 INFO  L226             Difference]: Without dead ends: 129
[2025-04-28 21:21:37,630 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 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:37,633 INFO  L437           NwaCegarLoop]: 194 mSDtfsCounter, 3 mSDsluCounter, 929 mSDsCounter, 0 mSdLazyCounter, 220 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1123 SdHoareTripleChecker+Invalid, 220 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 220 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,638 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1123 Invalid, 220 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 220 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:37,655 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 129 states.
[2025-04-28 21:21:37,710 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 129 to 129.
[2025-04-28 21:21:37,711 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 129 states, 29 states have (on average 2.0) internal successors, (58), 56 states have internal predecessors, (58), 84 states have call successors, (84), 14 states have call predecessors, (84), 15 states have return successors, (112), 59 states have call predecessors, (112), 84 states have call successors, (112)
[2025-04-28 21:21:37,718 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 129 states to 129 states and 254 transitions.
[2025-04-28 21:21:37,719 INFO  L79                 Accepts]: Start accepts. Automaton has 129 states and 254 transitions. Word has length 20
[2025-04-28 21:21:37,720 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,720 INFO  L485      AbstractCegarLoop]: Abstraction has 129 states and 254 transitions.
[2025-04-28 21:21:37,720 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:37,720 INFO  L278                IsEmpty]: Start isEmpty. Operand 129 states and 254 transitions.
[2025-04-28 21:21:37,724 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:37,724 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,724 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,724 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:37,725 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,725 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,725 INFO  L85        PathProgramCache]: Analyzing trace with hash 34858487, now seen corresponding path program 1 times
[2025-04-28 21:21:37,726 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,726 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1865717051]
[2025-04-28 21:21:37,726 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,726 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,738 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:37,756 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:37,756 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,756 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,042 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:38,042 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,042 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1865717051]
[2025-04-28 21:21:38,042 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1865717051] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:38,043 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,043 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:38,043 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [651107798]
[2025-04-28 21:21:38,043 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,044 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:38,044 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,045 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:38,045 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:38,045 INFO  L87              Difference]: Start difference. First operand 129 states and 254 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:38,526 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,526 INFO  L93              Difference]: Finished difference Result 135 states and 287 transitions.
[2025-04-28 21:21:38,526 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:38,527 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:38,527 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,531 INFO  L225             Difference]: With dead ends: 135
[2025-04-28 21:21:38,531 INFO  L226             Difference]: Without dead ends: 131
[2025-04-28 21:21:38,531 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 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:38,532 INFO  L437           NwaCegarLoop]: 223 mSDtfsCounter, 3 mSDsluCounter, 1073 mSDsCounter, 0 mSdLazyCounter, 220 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1296 SdHoareTripleChecker+Invalid, 220 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 220 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,532 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1296 Invalid, 220 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 220 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:38,533 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 131 states.
[2025-04-28 21:21:38,557 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 131 to 129.
[2025-04-28 21:21:38,558 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 129 states, 29 states have (on average 2.0) internal successors, (58), 56 states have internal predecessors, (58), 84 states have call successors, (84), 14 states have call predecessors, (84), 15 states have return successors, (112), 59 states have call predecessors, (112), 84 states have call successors, (112)
[2025-04-28 21:21:38,561 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 129 states to 129 states and 254 transitions.
[2025-04-28 21:21:38,561 INFO  L79                 Accepts]: Start accepts. Automaton has 129 states and 254 transitions. Word has length 20
[2025-04-28 21:21:38,561 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,561 INFO  L485      AbstractCegarLoop]: Abstraction has 129 states and 254 transitions.
[2025-04-28 21:21:38,562 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:38,562 INFO  L278                IsEmpty]: Start isEmpty. Operand 129 states and 254 transitions.
[2025-04-28 21:21:38,567 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:38,569 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,569 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,569 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:38,570 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,570 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,570 INFO  L85        PathProgramCache]: Analyzing trace with hash -2065702586, now seen corresponding path program 1 times
[2025-04-28 21:21:38,570 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,570 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1647375557]
[2025-04-28 21:21:38,570 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,571 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,584 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:38,607 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:38,608 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,608 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,804 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:38,805 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,805 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1647375557]
[2025-04-28 21:21:38,805 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1647375557] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:38,805 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,805 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:38,805 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1918012260]
[2025-04-28 21:21:38,805 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,805 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:38,806 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,806 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:38,806 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:38,806 INFO  L87              Difference]: Start difference. First operand 129 states and 254 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:39,300 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,301 INFO  L93              Difference]: Finished difference Result 137 states and 316 transitions.
[2025-04-28 21:21:39,304 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:39,304 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:39,304 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,311 INFO  L225             Difference]: With dead ends: 137
[2025-04-28 21:21:39,311 INFO  L226             Difference]: Without dead ends: 133
[2025-04-28 21:21:39,311 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 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:39,312 INFO  L437           NwaCegarLoop]: 223 mSDtfsCounter, 3 mSDsluCounter, 1073 mSDsCounter, 0 mSdLazyCounter, 219 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1296 SdHoareTripleChecker+Invalid, 220 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 219 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,312 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1296 Invalid, 220 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 219 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:39,316 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-04-28 21:21:39,355 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 129.
[2025-04-28 21:21:39,355 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 129 states, 29 states have (on average 2.0) internal successors, (58), 56 states have internal predecessors, (58), 84 states have call successors, (84), 14 states have call predecessors, (84), 15 states have return successors, (112), 59 states have call predecessors, (112), 84 states have call successors, (112)
[2025-04-28 21:21:39,361 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 129 states to 129 states and 254 transitions.
[2025-04-28 21:21:39,361 INFO  L79                 Accepts]: Start accepts. Automaton has 129 states and 254 transitions. Word has length 20
[2025-04-28 21:21:39,362 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,362 INFO  L485      AbstractCegarLoop]: Abstraction has 129 states and 254 transitions.
[2025-04-28 21:21:39,362 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:39,362 INFO  L278                IsEmpty]: Start isEmpty. Operand 129 states and 254 transitions.
[2025-04-28 21:21:39,364 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:39,365 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,366 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,366 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:39,366 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,366 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,369 INFO  L85        PathProgramCache]: Analyzing trace with hash 551189363, now seen corresponding path program 1 times
[2025-04-28 21:21:39,370 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,370 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1301874531]
[2025-04-28 21:21:39,370 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,370 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,383 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:39,407 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:39,408 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,408 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,625 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:39,626 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,626 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1301874531]
[2025-04-28 21:21:39,626 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1301874531] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,626 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,627 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:39,627 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [825287431]
[2025-04-28 21:21:39,627 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,627 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:39,627 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,628 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:39,629 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:39,630 INFO  L87              Difference]: Start difference. First operand 129 states and 254 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:40,056 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,056 INFO  L93              Difference]: Finished difference Result 135 states and 287 transitions.
[2025-04-28 21:21:40,057 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:40,057 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:40,057 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,060 INFO  L225             Difference]: With dead ends: 135
[2025-04-28 21:21:40,060 INFO  L226             Difference]: Without dead ends: 131
[2025-04-28 21:21:40,060 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 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:40,061 INFO  L437           NwaCegarLoop]: 223 mSDtfsCounter, 3 mSDsluCounter, 1073 mSDsCounter, 0 mSdLazyCounter, 220 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1296 SdHoareTripleChecker+Invalid, 220 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 220 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,061 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1296 Invalid, 220 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 220 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:40,062 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 131 states.
[2025-04-28 21:21:40,081 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 131 to 129.
[2025-04-28 21:21:40,082 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 129 states, 29 states have (on average 2.0) internal successors, (58), 55 states have internal predecessors, (58), 84 states have call successors, (84), 14 states have call predecessors, (84), 15 states have return successors, (112), 59 states have call predecessors, (112), 84 states have call successors, (112)
[2025-04-28 21:21:40,086 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 129 states to 129 states and 254 transitions.
[2025-04-28 21:21:40,087 INFO  L79                 Accepts]: Start accepts. Automaton has 129 states and 254 transitions. Word has length 20
[2025-04-28 21:21:40,087 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,087 INFO  L485      AbstractCegarLoop]: Abstraction has 129 states and 254 transitions.
[2025-04-28 21:21:40,087 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:40,088 INFO  L278                IsEmpty]: Start isEmpty. Operand 129 states and 254 transitions.
[2025-04-28 21:21:40,091 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:40,091 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,091 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:21:40,091 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:40,092 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,092 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,092 INFO  L85        PathProgramCache]: Analyzing trace with hash -894884393, now seen corresponding path program 1 times
[2025-04-28 21:21:40,092 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,092 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1942735554]
[2025-04-28 21:21:40,093 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,094 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,108 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:40,138 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:40,138 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,138 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,566 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:40,566 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,567 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1942735554]
[2025-04-28 21:21:40,567 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1942735554] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,567 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,567 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:40,567 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [549012301]
[2025-04-28 21:21:40,567 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,567 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:40,568 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,568 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:40,568 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:40,568 INFO  L87              Difference]: Start difference. First operand 129 states and 254 transitions. Second operand  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:41,352 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,353 INFO  L93              Difference]: Finished difference Result 142 states and 320 transitions.
[2025-04-28 21:21:41,353 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:41,354 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7) Word has length 28
[2025-04-28 21:21:41,354 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,357 INFO  L225             Difference]: With dead ends: 142
[2025-04-28 21:21:41,357 INFO  L226             Difference]: Without dead ends: 138
[2025-04-28 21:21:41,357 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=31, Invalid=125, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:41,360 INFO  L437           NwaCegarLoop]: 186 mSDtfsCounter, 7 mSDsluCounter, 1408 mSDsCounter, 0 mSdLazyCounter, 478 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 1594 SdHoareTripleChecker+Invalid, 482 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 478 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,361 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 1594 Invalid, 482 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 478 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:41,361 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 138 states.
[2025-04-28 21:21:41,395 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 138 to 134.
[2025-04-28 21:21:41,396 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 134 states, 31 states have (on average 1.935483870967742) internal successors, (60), 58 states have internal predecessors, (60), 85 states have call successors, (85), 14 states have call predecessors, (85), 17 states have return successors, (151), 61 states have call predecessors, (151), 85 states have call successors, (151)
[2025-04-28 21:21:41,399 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 134 states to 134 states and 296 transitions.
[2025-04-28 21:21:41,399 INFO  L79                 Accepts]: Start accepts. Automaton has 134 states and 296 transitions. Word has length 28
[2025-04-28 21:21:41,400 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,400 INFO  L485      AbstractCegarLoop]: Abstraction has 134 states and 296 transitions.
[2025-04-28 21:21:41,400 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:41,400 INFO  L278                IsEmpty]: Start isEmpty. Operand 134 states and 296 transitions.
[2025-04-28 21:21:41,403 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:41,403 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,404 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:21:41,404 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:41,404 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,404 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,404 INFO  L85        PathProgramCache]: Analyzing trace with hash -1145382689, now seen corresponding path program 1 times
[2025-04-28 21:21:41,405 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,405 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1046076145]
[2025-04-28 21:21:41,405 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,405 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,417 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:41,435 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:41,435 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,436 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,757 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:41,757 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,757 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1046076145]
[2025-04-28 21:21:41,758 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1046076145] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,758 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [983108877]
[2025-04-28 21:21:41,758 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,758 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,761 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,765 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:41,768 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,892 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:41,973 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:41,973 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,973 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,977 INFO  L256         TraceCheckSpWp]: Trace formula consists of 367 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,985 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,360 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:42,360 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,495 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:44,495 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [983108877] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,495 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,496 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 24
[2025-04-28 21:21:44,496 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [752035723]
[2025-04-28 21:21:44,496 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,496 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:44,497 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,497 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:44,497 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=498, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:44,498 INFO  L87              Difference]: Start difference. First operand 134 states and 296 transitions. Second operand  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:46,490 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,490 INFO  L93              Difference]: Finished difference Result 146 states and 359 transitions.
[2025-04-28 21:21:46,491 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:46,491 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16) Word has length 28
[2025-04-28 21:21:46,491 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,494 INFO  L225             Difference]: With dead ends: 146
[2025-04-28 21:21:46,494 INFO  L226             Difference]: Without dead ends: 142
[2025-04-28 21:21:46,495 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 75 GetRequests, 40 SyntacticMatches, 4 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 47 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=110, Invalid=946, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:46,497 INFO  L437           NwaCegarLoop]: 191 mSDtfsCounter, 12 mSDsluCounter, 3189 mSDsCounter, 0 mSdLazyCounter, 1643 mSolverCounterSat, 31 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 3380 SdHoareTripleChecker+Invalid, 1674 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 31 IncrementalHoareTripleChecker+Valid, 1643 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,497 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 3380 Invalid, 1674 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [31 Valid, 1643 Invalid, 0 Unknown, 0 Unchecked, 1.7s Time]
[2025-04-28 21:21:46,498 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-04-28 21:21:46,528 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 136.
[2025-04-28 21:21:46,529 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 136 states, 32 states have (on average 1.90625) internal successors, (61), 60 states have internal predecessors, (61), 85 states have call successors, (85), 14 states have call predecessors, (85), 18 states have return successors, (180), 61 states have call predecessors, (180), 85 states have call successors, (180)
[2025-04-28 21:21:46,532 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 136 states to 136 states and 326 transitions.
[2025-04-28 21:21:46,532 INFO  L79                 Accepts]: Start accepts. Automaton has 136 states and 326 transitions. Word has length 28
[2025-04-28 21:21:46,532 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,532 INFO  L485      AbstractCegarLoop]: Abstraction has 136 states and 326 transitions.
[2025-04-28 21:21:46,533 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:46,533 INFO  L278                IsEmpty]: Start isEmpty. Operand 136 states and 326 transitions.
[2025-04-28 21:21:46,536 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:46,536 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,536 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:21:46,543 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:46,741 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable6
[2025-04-28 21:21:46,741 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,741 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,741 INFO  L85        PathProgramCache]: Analyzing trace with hash -1149944722, now seen corresponding path program 1 times
[2025-04-28 21:21:46,741 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,742 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [77991583]
[2025-04-28 21:21:46,742 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,742 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,757 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:46,779 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:46,779 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,779 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,105 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:47,105 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,105 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [77991583]
[2025-04-28 21:21:47,106 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [77991583] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,106 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1129328412]
[2025-04-28 21:21:47,106 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,106 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,109 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,111 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:47,113 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,248 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:47,303 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:47,304 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,304 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,307 INFO  L256         TraceCheckSpWp]: Trace formula consists of 367 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,309 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,572 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:47,572 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:49,328 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,328 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1129328412] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:49,328 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:49,328 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 24
[2025-04-28 21:21:49,328 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [569010038]
[2025-04-28 21:21:49,329 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,331 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:49,331 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,331 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:49,331 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=498, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:49,332 INFO  L87              Difference]: Start difference. First operand 136 states and 326 transitions. Second operand  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:51,196 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,197 INFO  L93              Difference]: Finished difference Result 150 states and 398 transitions.
[2025-04-28 21:21:51,197 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:51,198 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16) Word has length 28
[2025-04-28 21:21:51,198 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,201 INFO  L225             Difference]: With dead ends: 150
[2025-04-28 21:21:51,201 INFO  L226             Difference]: Without dead ends: 146
[2025-04-28 21:21:51,202 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 75 GetRequests, 40 SyntacticMatches, 4 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 47 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=110, Invalid=946, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:51,202 INFO  L437           NwaCegarLoop]: 192 mSDtfsCounter, 11 mSDsluCounter, 3203 mSDsCounter, 0 mSdLazyCounter, 1828 mSolverCounterSat, 31 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 3395 SdHoareTripleChecker+Invalid, 1859 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 31 IncrementalHoareTripleChecker+Valid, 1828 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,202 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 3395 Invalid, 1859 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [31 Valid, 1828 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:21:51,203 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 146 states.
[2025-04-28 21:21:51,227 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 146 to 136.
[2025-04-28 21:21:51,227 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 136 states, 32 states have (on average 1.90625) internal successors, (61), 60 states have internal predecessors, (61), 85 states have call successors, (85), 14 states have call predecessors, (85), 18 states have return successors, (180), 61 states have call predecessors, (180), 85 states have call successors, (180)
[2025-04-28 21:21:51,229 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 136 states to 136 states and 326 transitions.
[2025-04-28 21:21:51,230 INFO  L79                 Accepts]: Start accepts. Automaton has 136 states and 326 transitions. Word has length 28
[2025-04-28 21:21:51,230 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,230 INFO  L485      AbstractCegarLoop]: Abstraction has 136 states and 326 transitions.
[2025-04-28 21:21:51,230 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:51,230 INFO  L278                IsEmpty]: Start isEmpty. Operand 136 states and 326 transitions.
[2025-04-28 21:21:51,233 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:51,233 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,233 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:21:51,239 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:51,437 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,438 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,438 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,438 INFO  L85        PathProgramCache]: Analyzing trace with hash 1127350107, now seen corresponding path program 1 times
[2025-04-28 21:21:51,438 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,438 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1695919943]
[2025-04-28 21:21:51,438 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,439 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,447 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:51,460 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:51,460 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,460 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,755 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:51,756 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,756 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1695919943]
[2025-04-28 21:21:51,756 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1695919943] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:51,756 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1048312828]
[2025-04-28 21:21:51,756 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,756 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,762 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:51,764 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:51,769 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:51,939 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:51,994 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:51,994 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,994 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,002 INFO  L256         TraceCheckSpWp]: Trace formula consists of 367 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,004 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,247 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:52,247 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,310 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:54,311 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1048312828] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,311 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,311 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 24
[2025-04-28 21:21:54,311 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1836593035]
[2025-04-28 21:21:54,311 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,312 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:54,312 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,312 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:54,313 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=498, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:54,313 INFO  L87              Difference]: Start difference. First operand 136 states and 326 transitions. Second operand  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:56,140 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,140 INFO  L93              Difference]: Finished difference Result 146 states and 359 transitions.
[2025-04-28 21:21:56,140 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:56,141 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16) Word has length 28
[2025-04-28 21:21:56,141 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,143 INFO  L225             Difference]: With dead ends: 146
[2025-04-28 21:21:56,144 INFO  L226             Difference]: Without dead ends: 142
[2025-04-28 21:21:56,144 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 75 GetRequests, 40 SyntacticMatches, 4 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 47 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=110, Invalid=946, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:56,144 INFO  L437           NwaCegarLoop]: 191 mSDtfsCounter, 13 mSDsluCounter, 3191 mSDsCounter, 0 mSdLazyCounter, 1645 mSolverCounterSat, 24 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 3382 SdHoareTripleChecker+Invalid, 1669 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 24 IncrementalHoareTripleChecker+Valid, 1645 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,145 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 3382 Invalid, 1669 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [24 Valid, 1645 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:21:56,145 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-04-28 21:21:56,161 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 134.
[2025-04-28 21:21:56,161 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 134 states, 31 states have (on average 1.935483870967742) internal successors, (60), 58 states have internal predecessors, (60), 85 states have call successors, (85), 14 states have call predecessors, (85), 17 states have return successors, (151), 61 states have call predecessors, (151), 85 states have call successors, (151)
[2025-04-28 21:21:56,163 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 134 states to 134 states and 296 transitions.
[2025-04-28 21:21:56,163 INFO  L79                 Accepts]: Start accepts. Automaton has 134 states and 296 transitions. Word has length 28
[2025-04-28 21:21:56,164 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,164 INFO  L485      AbstractCegarLoop]: Abstraction has 134 states and 296 transitions.
[2025-04-28 21:21:56,164 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:56,164 INFO  L278                IsEmpty]: Start isEmpty. Operand 134 states and 296 transitions.
[2025-04-28 21:21:56,166 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:56,166 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,167 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:21:56,173 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:56,371 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,371 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,371 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,371 INFO  L85        PathProgramCache]: Analyzing trace with hash -1508240161, now seen corresponding path program 2 times
[2025-04-28 21:21:56,372 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,372 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [884674691]
[2025-04-28 21:21:56,372 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:56,372 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,384 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:56,406 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:56,406 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:56,406 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,655 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:56,655 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,655 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [884674691]
[2025-04-28 21:21:56,655 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [884674691] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,656 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [618651773]
[2025-04-28 21:21:56,656 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:56,656 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,658 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,661 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:56,662 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,826 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:56,876 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:56,877 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:56,877 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,878 INFO  L256         TraceCheckSpWp]: Trace formula consists of 367 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,880 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,077 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:57,077 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,640 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:58,640 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [618651773] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:58,640 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:58,640 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 24
[2025-04-28 21:21:58,641 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [358920023]
[2025-04-28 21:21:58,641 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,641 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:58,641 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,641 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:58,642 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=498, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:58,642 INFO  L87              Difference]: Start difference. First operand 134 states and 296 transitions. Second operand  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:00,524 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,525 INFO  L93              Difference]: Finished difference Result 147 states and 364 transitions.
[2025-04-28 21:22:00,525 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:00,525 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16) Word has length 28
[2025-04-28 21:22:00,526 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,528 INFO  L225             Difference]: With dead ends: 147
[2025-04-28 21:22:00,528 INFO  L226             Difference]: Without dead ends: 143
[2025-04-28 21:22:00,529 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 75 GetRequests, 40 SyntacticMatches, 4 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 47 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=110, Invalid=946, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:00,529 INFO  L437           NwaCegarLoop]: 188 mSDtfsCounter, 16 mSDsluCounter, 3313 mSDsCounter, 0 mSdLazyCounter, 1688 mSolverCounterSat, 32 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 3501 SdHoareTripleChecker+Invalid, 1720 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 32 IncrementalHoareTripleChecker+Valid, 1688 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,530 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 3501 Invalid, 1720 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [32 Valid, 1688 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:22:00,530 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 143 states.
[2025-04-28 21:22:00,547 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 143 to 137.
[2025-04-28 21:22:00,548 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 32 states have (on average 1.90625) internal successors, (61), 60 states have internal predecessors, (61), 86 states have call successors, (86), 14 states have call predecessors, (86), 18 states have return successors, (184), 62 states have call predecessors, (184), 86 states have call successors, (184)
[2025-04-28 21:22:00,550 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 331 transitions.
[2025-04-28 21:22:00,550 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 331 transitions. Word has length 28
[2025-04-28 21:22:00,550 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,550 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 331 transitions.
[2025-04-28 21:22:00,550 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:00,551 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 331 transitions.
[2025-04-28 21:22:00,553 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:00,553 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,554 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:22:00,561 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:22:00,754 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:00,754 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,755 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,755 INFO  L85        PathProgramCache]: Analyzing trace with hash -1758738457, now seen corresponding path program 1 times
[2025-04-28 21:22:00,755 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,755 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1268407394]
[2025-04-28 21:22:00,755 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,755 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,763 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:00,773 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:00,773 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,773 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,942 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:00,942 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,942 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1268407394]
[2025-04-28 21:22:00,942 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1268407394] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:00,942 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:00,942 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:22:00,942 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1903903801]
[2025-04-28 21:22:00,942 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,943 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:22:00,943 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,943 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:22:00,943 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:22:00,944 INFO  L87              Difference]: Start difference. First operand 137 states and 331 transitions. Second operand  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:22:01,723 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,723 INFO  L93              Difference]: Finished difference Result 149 states and 373 transitions.
[2025-04-28 21:22:01,723 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:01,723 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7) Word has length 28
[2025-04-28 21:22:01,724 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,725 INFO  L225             Difference]: With dead ends: 149
[2025-04-28 21:22:01,725 INFO  L226             Difference]: Without dead ends: 145
[2025-04-28 21:22:01,726 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=31, Invalid=125, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:22:01,726 INFO  L437           NwaCegarLoop]: 222 mSDtfsCounter, 4 mSDsluCounter, 1674 mSDsCounter, 0 mSdLazyCounter, 586 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 1896 SdHoareTripleChecker+Invalid, 587 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 586 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,726 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 1896 Invalid, 587 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 586 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:01,727 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 145 states.
[2025-04-28 21:22:01,742 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 145 to 137.
[2025-04-28 21:22:01,743 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 137 states, 32 states have (on average 1.90625) internal successors, (61), 60 states have internal predecessors, (61), 86 states have call successors, (86), 14 states have call predecessors, (86), 18 states have return successors, (184), 62 states have call predecessors, (184), 86 states have call successors, (184)
[2025-04-28 21:22:01,745 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 137 states to 137 states and 331 transitions.
[2025-04-28 21:22:01,745 INFO  L79                 Accepts]: Start accepts. Automaton has 137 states and 331 transitions. Word has length 28
[2025-04-28 21:22:01,745 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,745 INFO  L485      AbstractCegarLoop]: Abstraction has 137 states and 331 transitions.
[2025-04-28 21:22:01,745 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:22:01,745 INFO  L278                IsEmpty]: Start isEmpty. Operand 137 states and 331 transitions.
[2025-04-28 21:22:01,748 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:01,748 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,748 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:22:01,748 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:22:01,748 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,749 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,749 INFO  L85        PathProgramCache]: Analyzing trace with hash -1763300490, now seen corresponding path program 1 times
[2025-04-28 21:22:01,749 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,749 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1528159860]
[2025-04-28 21:22:01,749 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,749 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,757 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:01,767 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:01,767 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,767 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,948 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:22:01,948 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,948 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1528159860]
[2025-04-28 21:22:01,948 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1528159860] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:01,948 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:01,948 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:22:01,948 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [97916641]
[2025-04-28 21:22:01,948 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,948 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:22:01,948 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,949 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:22:01,949 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=90, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:22:01,949 INFO  L87              Difference]: Start difference. First operand 137 states and 331 transitions. Second operand  has 11 states, 7 states have (on average 2.0) internal successors, (14), 10 states have internal predecessors, (14), 5 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:22:02,867 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,867 INFO  L93              Difference]: Finished difference Result 152 states and 410 transitions.
[2025-04-28 21:22:02,867 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:02,868 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 7 states have (on average 2.0) internal successors, (14), 10 states have internal predecessors, (14), 5 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7) Word has length 28
[2025-04-28 21:22:02,868 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,870 INFO  L225             Difference]: With dead ends: 152
[2025-04-28 21:22:02,870 INFO  L226             Difference]: Without dead ends: 148
[2025-04-28 21:22:02,870 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=34, Invalid=148, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:22:02,871 INFO  L437           NwaCegarLoop]: 221 mSDtfsCounter, 5 mSDsluCounter, 1671 mSDsCounter, 0 mSdLazyCounter, 755 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1892 SdHoareTripleChecker+Invalid, 757 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 755 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,871 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1892 Invalid, 757 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 755 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:02,872 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 148 states.
[2025-04-28 21:22:02,893 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 148 to 140.
[2025-04-28 21:22:02,893 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 140 states, 33 states have (on average 1.878787878787879) internal successors, (62), 62 states have internal predecessors, (62), 87 states have call successors, (87), 14 states have call predecessors, (87), 19 states have return successors, (219), 63 states have call predecessors, (219), 87 states have call successors, (219)
[2025-04-28 21:22:02,895 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 140 states to 140 states and 368 transitions.
[2025-04-28 21:22:02,897 INFO  L79                 Accepts]: Start accepts. Automaton has 140 states and 368 transitions. Word has length 28
[2025-04-28 21:22:02,898 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:02,898 INFO  L485      AbstractCegarLoop]: Abstraction has 140 states and 368 transitions.
[2025-04-28 21:22:02,898 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 7 states have (on average 2.0) internal successors, (14), 10 states have internal predecessors, (14), 5 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:22:02,898 INFO  L278                IsEmpty]: Start isEmpty. Operand 140 states and 368 transitions.
[2025-04-28 21:22:02,902 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:02,902 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:02,902 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:22:02,903 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:22:02,903 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,903 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,903 INFO  L85        PathProgramCache]: Analyzing trace with hash 513994339, now seen corresponding path program 1 times
[2025-04-28 21:22:02,903 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,903 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [585818872]
[2025-04-28 21:22:02,903 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:02,903 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,915 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:02,925 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:02,926 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,926 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,173 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:22:03,174 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,174 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [585818872]
[2025-04-28 21:22:03,174 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [585818872] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:03,174 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [135901460]
[2025-04-28 21:22:03,174 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:03,174 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:03,176 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:03,179 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:22:03,183 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:22:03,353 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:03,403 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:03,404 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,404 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,411 INFO  L256         TraceCheckSpWp]: Trace formula consists of 367 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:03,413 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:03,517 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:22:03,517 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
