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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:42,844 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:42,930 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_41819ba9-f0bc-4dad-b40b-0a7ead027a18/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:42,936 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:42,936 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:42,963 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:42,964 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:42,964 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:42,964 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:42,964 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:42,965 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:42,965 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:42,965 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:42,965 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:42,965 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:42,965 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:42,965 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:42,966 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:42,966 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:42,966 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:42,966 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:42,966 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:42,966 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:42,966 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:42,966 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:42,968 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:42,969 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:43,311 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:43,325 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:43,327 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:43,329 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:43,331 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:43,332 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_41819ba9-f0bc-4dad-b40b-0a7ead027a18/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-199.smt2
[2025-04-28 21:21:43,333 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:43,339 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:43,649 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_41819ba9-f0bc-4dad-b40b-0a7ead027a18/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-199.smt2
[2025-04-28 21:21:43,653 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:43,655 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:43,656 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:43,656 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:43,656 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:43,660 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,691 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43 Unit
[2025-04-28 21:21:43,693 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:43,695 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:43,695 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:43,695 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:43,715 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,716 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,754 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,755 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,759 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,760 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,762 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,763 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,766 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,786 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:43,787 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:43,787 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:43,787 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:43,788 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,791 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:43,805 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,819 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:43,822 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:43,839 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:43,839 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:43,839 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:43,839 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:43,839 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:43,839 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:43,840 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h20 given in one single declaration
[2025-04-28 21:21:43,840 INFO  L130     BoogieDeclarations]: Found specification of procedure h20
[2025-04-28 21:21:43,840 INFO  L138     BoogieDeclarations]: Found implementation of procedure h20
[2025-04-28 21:21:43,840 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h18 given in one single declaration
[2025-04-28 21:21:43,840 INFO  L130     BoogieDeclarations]: Found specification of procedure h18
[2025-04-28 21:21:43,840 INFO  L138     BoogieDeclarations]: Found implementation of procedure h18
[2025-04-28 21:21:43,840 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h11 given in one single declaration
[2025-04-28 21:21:43,840 INFO  L130     BoogieDeclarations]: Found specification of procedure h11
[2025-04-28 21:21:43,840 INFO  L138     BoogieDeclarations]: Found implementation of procedure h11
[2025-04-28 21:21:43,840 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h10 given in one single declaration
[2025-04-28 21:21:43,840 INFO  L130     BoogieDeclarations]: Found specification of procedure h10
[2025-04-28 21:21:43,840 INFO  L138     BoogieDeclarations]: Found implementation of procedure h10
[2025-04-28 21:21:43,841 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h9 given in one single declaration
[2025-04-28 21:21:43,841 INFO  L130     BoogieDeclarations]: Found specification of procedure h9
[2025-04-28 21:21:43,841 INFO  L138     BoogieDeclarations]: Found implementation of procedure h9
[2025-04-28 21:21:43,841 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h6 given in one single declaration
[2025-04-28 21:21:43,841 INFO  L130     BoogieDeclarations]: Found specification of procedure h6
[2025-04-28 21:21:43,841 INFO  L138     BoogieDeclarations]: Found implementation of procedure h6
[2025-04-28 21:21:43,841 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h5 given in one single declaration
[2025-04-28 21:21:43,841 INFO  L130     BoogieDeclarations]: Found specification of procedure h5
[2025-04-28 21:21:43,841 INFO  L138     BoogieDeclarations]: Found implementation of procedure h5
[2025-04-28 21:21:43,841 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h17 given in one single declaration
[2025-04-28 21:21:43,842 INFO  L130     BoogieDeclarations]: Found specification of procedure h17
[2025-04-28 21:21:43,842 INFO  L138     BoogieDeclarations]: Found implementation of procedure h17
[2025-04-28 21:21:43,842 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h16 given in one single declaration
[2025-04-28 21:21:43,842 INFO  L130     BoogieDeclarations]: Found specification of procedure h16
[2025-04-28 21:21:43,842 INFO  L138     BoogieDeclarations]: Found implementation of procedure h16
[2025-04-28 21:21:43,842 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h15 given in one single declaration
[2025-04-28 21:21:43,842 INFO  L130     BoogieDeclarations]: Found specification of procedure h15
[2025-04-28 21:21:43,842 INFO  L138     BoogieDeclarations]: Found implementation of procedure h15
[2025-04-28 21:21:43,842 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h8 given in one single declaration
[2025-04-28 21:21:43,842 INFO  L130     BoogieDeclarations]: Found specification of procedure h8
[2025-04-28 21:21:43,843 INFO  L138     BoogieDeclarations]: Found implementation of procedure h8
[2025-04-28 21:21:43,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h7 given in one single declaration
[2025-04-28 21:21:43,843 INFO  L130     BoogieDeclarations]: Found specification of procedure h7
[2025-04-28 21:21:43,843 INFO  L138     BoogieDeclarations]: Found implementation of procedure h7
[2025-04-28 21:21:43,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h13 given in one single declaration
[2025-04-28 21:21:43,843 INFO  L130     BoogieDeclarations]: Found specification of procedure h13
[2025-04-28 21:21:43,843 INFO  L138     BoogieDeclarations]: Found implementation of procedure h13
[2025-04-28 21:21:43,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h14 given in one single declaration
[2025-04-28 21:21:43,843 INFO  L130     BoogieDeclarations]: Found specification of procedure h14
[2025-04-28 21:21:43,843 INFO  L138     BoogieDeclarations]: Found implementation of procedure h14
[2025-04-28 21:21:43,843 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h12 given in one single declaration
[2025-04-28 21:21:43,844 INFO  L130     BoogieDeclarations]: Found specification of procedure h12
[2025-04-28 21:21:43,844 INFO  L138     BoogieDeclarations]: Found implementation of procedure h12
[2025-04-28 21:21:43,844 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h4 given in one single declaration
[2025-04-28 21:21:43,844 INFO  L130     BoogieDeclarations]: Found specification of procedure h4
[2025-04-28 21:21:43,844 INFO  L138     BoogieDeclarations]: Found implementation of procedure h4
[2025-04-28 21:21:43,844 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h3 given in one single declaration
[2025-04-28 21:21:43,844 INFO  L130     BoogieDeclarations]: Found specification of procedure h3
[2025-04-28 21:21:43,844 INFO  L138     BoogieDeclarations]: Found implementation of procedure h3
[2025-04-28 21:21:43,844 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h2 given in one single declaration
[2025-04-28 21:21:43,844 INFO  L130     BoogieDeclarations]: Found specification of procedure h2
[2025-04-28 21:21:43,844 INFO  L138     BoogieDeclarations]: Found implementation of procedure h2
[2025-04-28 21:21:43,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h1 given in one single declaration
[2025-04-28 21:21:43,845 INFO  L130     BoogieDeclarations]: Found specification of procedure h1
[2025-04-28 21:21:43,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure h1
[2025-04-28 21:21:43,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h19 given in one single declaration
[2025-04-28 21:21:43,845 INFO  L130     BoogieDeclarations]: Found specification of procedure h19
[2025-04-28 21:21:43,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure h19
[2025-04-28 21:21:43,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:43,845 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:43,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:43,952 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:43,955 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:44,275 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:44,276 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:44,295 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:44,295 INFO  L312             CfgBuilder]: Removed 12 assume(true) statements.
[2025-04-28 21:21:44,296 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:44 BoogieIcfgContainer
[2025-04-28 21:21:44,296 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:44,301 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:44,301 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:44,307 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:44,308 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:43" (1/3) ...
[2025-04-28 21:21:44,309 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@58e325b4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:44, skipping insertion in model container
[2025-04-28 21:21:44,309 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (2/3) ...
[2025-04-28 21:21:44,310 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@58e325b4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:44, skipping insertion in model container
[2025-04-28 21:21:44,310 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:44" (3/3) ...
[2025-04-28 21:21:44,312 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:44,333 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:44,337 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 23 procedures, 88 locations, 133 edges, 23 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:44,387 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:44,407 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;@6f52b8ff, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:44,407 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:44,412 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 88 states, 36 states have (on average 1.1944444444444444) internal successors, (43), 43 states have internal predecessors, (43), 28 states have call successors, (30), 22 states have call predecessors, (30), 22 states have return successors, (30), 22 states have call predecessors, (30), 28 states have call successors, (30)
[2025-04-28 21:21:44,425 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:44,425 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,426 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, 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:44,426 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,431 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,432 INFO  L85        PathProgramCache]: Analyzing trace with hash -1372517223, now seen corresponding path program 1 times
[2025-04-28 21:21:44,437 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,438 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [39637756]
[2025-04-28 21:21:44,438 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,439 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,493 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:21:44,544 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:44,544 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,545 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,159 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:45,159 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,159 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [39637756]
[2025-04-28 21:21:45,160 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [39637756] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,160 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,163 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [12] imperfect sequences [] total 12
[2025-04-28 21:21:45,165 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1428785722]
[2025-04-28 21:21:45,166 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,170 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:45,170 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,242 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:45,243 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=111, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:45,246 INFO  L87              Difference]: Start difference. First operand  has 88 states, 36 states have (on average 1.1944444444444444) internal successors, (43), 43 states have internal predecessors, (43), 28 states have call successors, (30), 22 states have call predecessors, (30), 22 states have return successors, (30), 22 states have call predecessors, (30), 28 states have call successors, (30) Second operand  has 12 states, 11 states have (on average 1.6363636363636365) internal successors, (18), 12 states have internal predecessors, (18), 3 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (13), 10 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:45,589 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,590 INFO  L93              Difference]: Finished difference Result 98 states and 114 transitions.
[2025-04-28 21:21:45,591 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:45,593 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 11 states have (on average 1.6363636363636365) internal successors, (18), 12 states have internal predecessors, (18), 3 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (13), 10 states have call predecessors, (13), 3 states have call successors, (13) Word has length 44
[2025-04-28 21:21:45,593 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,602 INFO  L225             Difference]: With dead ends: 98
[2025-04-28 21:21:45,602 INFO  L226             Difference]: Without dead ends: 98
[2025-04-28 21:21:45,604 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=111, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:45,607 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 1 mSDsluCounter, 885 mSDsCounter, 0 mSdLazyCounter, 125 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 975 SdHoareTripleChecker+Invalid, 125 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 125 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,608 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 975 Invalid, 125 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 125 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:45,624 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-04-28 21:21:45,648 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 98.
[2025-04-28 21:21:45,649 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 98 states, 41 states have (on average 1.146341463414634) internal successors, (47), 47 states have internal predecessors, (47), 28 states have call successors, (30), 22 states have call predecessors, (30), 28 states have return successors, (37), 28 states have call predecessors, (37), 28 states have call successors, (37)
[2025-04-28 21:21:45,654 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 98 states to 98 states and 114 transitions.
[2025-04-28 21:21:45,655 INFO  L79                 Accepts]: Start accepts. Automaton has 98 states and 114 transitions. Word has length 44
[2025-04-28 21:21:45,656 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,656 INFO  L485      AbstractCegarLoop]: Abstraction has 98 states and 114 transitions.
[2025-04-28 21:21:45,657 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 11 states have (on average 1.6363636363636365) internal successors, (18), 12 states have internal predecessors, (18), 3 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (13), 10 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:45,657 INFO  L278                IsEmpty]: Start isEmpty. Operand 98 states and 114 transitions.
[2025-04-28 21:21:45,660 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:45,661 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,661 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, 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:45,661 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:45,661 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,662 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,662 INFO  L85        PathProgramCache]: Analyzing trace with hash -975180975, now seen corresponding path program 1 times
[2025-04-28 21:21:45,662 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,662 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [15856769]
[2025-04-28 21:21:45,662 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,662 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,677 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:21:45,686 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:45,686 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,686 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,005 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:46,005 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,005 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [15856769]
[2025-04-28 21:21:46,005 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [15856769] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,006 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,006 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [12] imperfect sequences [] total 12
[2025-04-28 21:21:46,006 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1407859909]
[2025-04-28 21:21:46,006 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,008 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:46,008 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,008 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:46,009 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=111, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:46,009 INFO  L87              Difference]: Start difference. First operand 98 states and 114 transitions. Second operand  has 12 states, 11 states have (on average 1.6363636363636365) internal successors, (18), 12 states have internal predecessors, (18), 3 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (13), 10 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:46,175 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,175 INFO  L93              Difference]: Finished difference Result 98 states and 113 transitions.
[2025-04-28 21:21:46,176 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:46,176 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 11 states have (on average 1.6363636363636365) internal successors, (18), 12 states have internal predecessors, (18), 3 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (13), 10 states have call predecessors, (13), 3 states have call successors, (13) Word has length 44
[2025-04-28 21:21:46,177 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,178 INFO  L225             Difference]: With dead ends: 98
[2025-04-28 21:21:46,178 INFO  L226             Difference]: Without dead ends: 90
[2025-04-28 21:21:46,178 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=111, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:46,179 INFO  L437           NwaCegarLoop]: 91 mSDtfsCounter, 1 mSDsluCounter, 895 mSDsCounter, 0 mSdLazyCounter, 114 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 986 SdHoareTripleChecker+Invalid, 114 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 114 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,180 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 986 Invalid, 114 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 114 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:46,180 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-04-28 21:21:46,188 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 90.
[2025-04-28 21:21:46,188 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 37 states have (on average 1.162162162162162) internal successors, (43), 43 states have internal predecessors, (43), 28 states have call successors, (30), 22 states have call predecessors, (30), 24 states have return successors, (32), 24 states have call predecessors, (32), 28 states have call successors, (32)
[2025-04-28 21:21:46,190 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 105 transitions.
[2025-04-28 21:21:46,190 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 105 transitions. Word has length 44
[2025-04-28 21:21:46,190 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,190 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 105 transitions.
[2025-04-28 21:21:46,190 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 11 states have (on average 1.6363636363636365) internal successors, (18), 12 states have internal predecessors, (18), 3 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (13), 10 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:46,190 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 105 transitions.
[2025-04-28 21:21:46,192 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-04-28 21:21:46,192 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,193 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,193 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:46,193 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,193 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,194 INFO  L85        PathProgramCache]: Analyzing trace with hash -399534371, now seen corresponding path program 1 times
[2025-04-28 21:21:46,194 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,194 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [786470194]
[2025-04-28 21:21:46,194 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,194 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,209 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:21:46,224 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:21:46,224 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,224 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,321 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:46,321 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,321 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [786470194]
[2025-04-28 21:21:46,321 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [786470194] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,321 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,321 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:46,321 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [367734800]
[2025-04-28 21:21:46,322 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,322 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:46,322 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,323 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:46,323 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:46,323 INFO  L87              Difference]: Start difference. First operand 90 states and 105 transitions. Second operand  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:21:46,391 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,391 INFO  L93              Difference]: Finished difference Result 92 states and 106 transitions.
[2025-04-28 21:21:46,392 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:46,393 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20) Word has length 69
[2025-04-28 21:21:46,393 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,394 INFO  L225             Difference]: With dead ends: 92
[2025-04-28 21:21:46,394 INFO  L226             Difference]: Without dead ends: 91
[2025-04-28 21:21:46,395 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:46,395 INFO  L437           NwaCegarLoop]: 97 mSDtfsCounter, 1 mSDsluCounter, 276 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 373 SdHoareTripleChecker+Invalid, 20 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,399 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 373 Invalid, 20 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:46,400 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-04-28 21:21:46,414 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 89.
[2025-04-28 21:21:46,415 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 89 states, 37 states have (on average 1.135135135135135) internal successors, (42), 42 states have internal predecessors, (42), 27 states have call successors, (29), 22 states have call predecessors, (29), 24 states have return successors, (31), 24 states have call predecessors, (31), 27 states have call successors, (31)
[2025-04-28 21:21:46,416 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 89 states to 89 states and 102 transitions.
[2025-04-28 21:21:46,416 INFO  L79                 Accepts]: Start accepts. Automaton has 89 states and 102 transitions. Word has length 69
[2025-04-28 21:21:46,417 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,417 INFO  L485      AbstractCegarLoop]: Abstraction has 89 states and 102 transitions.
[2025-04-28 21:21:46,417 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:21:46,417 INFO  L278                IsEmpty]: Start isEmpty. Operand 89 states and 102 transitions.
[2025-04-28 21:21:46,422 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-04-28 21:21:46,423 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,423 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,423 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:46,423 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,424 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,424 INFO  L85        PathProgramCache]: Analyzing trace with hash 1030715591, now seen corresponding path program 1 times
[2025-04-28 21:21:46,424 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,424 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [479571321]
[2025-04-28 21:21:46,424 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,424 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,451 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:21:46,479 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:21:46,480 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,480 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,215 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:47,215 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,215 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [479571321]
[2025-04-28 21:21:47,215 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [479571321] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,215 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [879696404]
[2025-04-28 21:21:47,215 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,215 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,218 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,222 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:47,224 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,332 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:21:47,418 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:21:47,418 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,418 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,422 INFO  L256         TraceCheckSpWp]: Trace formula consists of 472 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,433 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,565 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:47,566 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:47,566 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [879696404] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,566 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:47,566 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [16] total 19
[2025-04-28 21:21:47,566 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1010450955]
[2025-04-28 21:21:47,566 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,567 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:47,567 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,568 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:47,568 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=305, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:47,568 INFO  L87              Difference]: Start difference. First operand 89 states and 102 transitions. Second operand  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:21:47,617 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,618 INFO  L93              Difference]: Finished difference Result 93 states and 107 transitions.
[2025-04-28 21:21:47,619 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:47,619 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20) Word has length 69
[2025-04-28 21:21:47,620 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,622 INFO  L225             Difference]: With dead ends: 93
[2025-04-28 21:21:47,624 INFO  L226             Difference]: Without dead ends: 93
[2025-04-28 21:21:47,625 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 85 GetRequests, 68 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=37, Invalid=305, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:47,626 INFO  L437           NwaCegarLoop]: 97 mSDtfsCounter, 1 mSDsluCounter, 277 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 374 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,626 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 374 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:47,627 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 93 states.
[2025-04-28 21:21:47,639 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 93 to 91.
[2025-04-28 21:21:47,640 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 38 states have (on average 1.131578947368421) internal successors, (43), 43 states have internal predecessors, (43), 27 states have call successors, (29), 22 states have call predecessors, (29), 25 states have return successors, (33), 25 states have call predecessors, (33), 27 states have call successors, (33)
[2025-04-28 21:21:47,641 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 105 transitions.
[2025-04-28 21:21:47,643 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 105 transitions. Word has length 69
[2025-04-28 21:21:47,643 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,644 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 105 transitions.
[2025-04-28 21:21:47,644 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:21:47,644 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 105 transitions.
[2025-04-28 21:21:47,647 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-04-28 21:21:47,648 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,648 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,656 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:47,848 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,849 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,849 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,849 INFO  L85        PathProgramCache]: Analyzing trace with hash 147570888, now seen corresponding path program 1 times
[2025-04-28 21:21:47,850 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,851 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [987473342]
[2025-04-28 21:21:47,851 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,851 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,865 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:21:47,882 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:21:47,883 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,883 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,981 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:47,981 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,981 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [987473342]
[2025-04-28 21:21:47,981 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [987473342] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,981 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,982 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:47,982 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [64197179]
[2025-04-28 21:21:47,982 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,982 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:47,982 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,983 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:47,983 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:47,983 INFO  L87              Difference]: Start difference. First operand 91 states and 105 transitions. Second operand  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:21:48,022 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,023 INFO  L93              Difference]: Finished difference Result 93 states and 106 transitions.
[2025-04-28 21:21:48,024 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:48,024 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20) Word has length 69
[2025-04-28 21:21:48,025 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,026 INFO  L225             Difference]: With dead ends: 93
[2025-04-28 21:21:48,026 INFO  L226             Difference]: Without dead ends: 93
[2025-04-28 21:21:48,026 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:48,027 INFO  L437           NwaCegarLoop]: 98 mSDtfsCounter, 1 mSDsluCounter, 278 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 376 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,027 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 376 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:48,029 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 93 states.
[2025-04-28 21:21:48,038 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 93 to 91.
[2025-04-28 21:21:48,038 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 38 states have (on average 1.131578947368421) internal successors, (43), 43 states have internal predecessors, (43), 27 states have call successors, (29), 22 states have call predecessors, (29), 25 states have return successors, (32), 25 states have call predecessors, (32), 27 states have call successors, (32)
[2025-04-28 21:21:48,039 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 104 transitions.
[2025-04-28 21:21:48,039 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 104 transitions. Word has length 69
[2025-04-28 21:21:48,039 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,039 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 104 transitions.
[2025-04-28 21:21:48,040 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:21:48,040 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 104 transitions.
[2025-04-28 21:21:48,041 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-04-28 21:21:48,041 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,041 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,041 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:48,041 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,042 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,042 INFO  L85        PathProgramCache]: Analyzing trace with hash 1415331528, now seen corresponding path program 1 times
[2025-04-28 21:21:48,042 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,042 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1594634557]
[2025-04-28 21:21:48,042 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,042 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,055 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:21:48,072 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:21:48,074 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,075 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,710 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:48,710 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,710 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1594634557]
[2025-04-28 21:21:48,710 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1594634557] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:48,710 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [541327411]
[2025-04-28 21:21:48,710 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,710 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,713 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,715 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:48,718 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,811 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:21:48,895 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:21:48,895 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,895 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,900 INFO  L256         TraceCheckSpWp]: Trace formula consists of 472 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,922 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:49,556 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:49,557 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:14,290 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:22:14,291 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [541327411] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:14,291 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:14,291 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 16, 16] total 32
[2025-04-28 21:22:14,291 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [967567973]
[2025-04-28 21:22:14,291 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:14,292 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 32 states
[2025-04-28 21:22:14,292 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:14,293 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 32 interpolants.
[2025-04-28 21:22:14,293 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=86, Invalid=906, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:22:14,294 INFO  L87              Difference]: Start difference. First operand 91 states and 104 transitions. Second operand  has 32 states, 26 states have (on average 1.7692307692307692) internal successors, (46), 32 states have internal predecessors, (46), 9 states have call successors, (24), 1 states have call predecessors, (24), 26 states have return successors, (35), 25 states have call predecessors, (35), 9 states have call successors, (35)
[2025-04-28 21:22:14,720 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:14,721 INFO  L93              Difference]: Finished difference Result 105 states and 120 transitions.
[2025-04-28 21:22:14,724 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:22:14,725 INFO  L79                 Accepts]: Start accepts. Automaton has  has 32 states, 26 states have (on average 1.7692307692307692) internal successors, (46), 32 states have internal predecessors, (46), 9 states have call successors, (24), 1 states have call predecessors, (24), 26 states have return successors, (35), 25 states have call predecessors, (35), 9 states have call successors, (35) Word has length 69
[2025-04-28 21:22:14,725 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:14,727 INFO  L225             Difference]: With dead ends: 105
[2025-04-28 21:22:14,727 INFO  L226             Difference]: Without dead ends: 105
[2025-04-28 21:22:14,728 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 155 GetRequests, 124 SyntacticMatches, 0 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 146 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=93, Invalid=963, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:14,729 INFO  L437           NwaCegarLoop]: 86 mSDtfsCounter, 3 mSDsluCounter, 2246 mSDsCounter, 0 mSdLazyCounter, 433 mSolverCounterSat, 14 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 2332 SdHoareTripleChecker+Invalid, 447 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 14 IncrementalHoareTripleChecker+Valid, 433 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:14,731 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 2332 Invalid, 447 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [14 Valid, 433 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:14,732 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 105 states.
[2025-04-28 21:22:14,747 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 105 to 105.
[2025-04-28 21:22:14,749 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 45 states have (on average 1.1111111111111112) internal successors, (50), 50 states have internal predecessors, (50), 27 states have call successors, (29), 22 states have call predecessors, (29), 32 states have return successors, (41), 32 states have call predecessors, (41), 27 states have call successors, (41)
[2025-04-28 21:22:14,751 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 120 transitions.
[2025-04-28 21:22:14,752 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 120 transitions. Word has length 69
[2025-04-28 21:22:14,753 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:14,753 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 120 transitions.
[2025-04-28 21:22:14,753 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 32 states, 26 states have (on average 1.7692307692307692) internal successors, (46), 32 states have internal predecessors, (46), 9 states have call successors, (24), 1 states have call predecessors, (24), 26 states have return successors, (35), 25 states have call predecessors, (35), 9 states have call successors, (35)
[2025-04-28 21:22:14,753 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 120 transitions.
[2025-04-28 21:22:14,754 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-04-28 21:22:14,754 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:14,754 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:14,762 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:14,955 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:14,955 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:14,955 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:14,955 INFO  L85        PathProgramCache]: Analyzing trace with hash -92253055, now seen corresponding path program 1 times
[2025-04-28 21:22:14,956 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:14,956 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [270729059]
[2025-04-28 21:22:14,956 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:14,956 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:14,996 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:22:15,013 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:22:15,013 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:15,013 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:15,511 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:22:15,512 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:15,512 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [270729059]
[2025-04-28 21:22:15,512 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [270729059] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:15,512 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [714036213]
[2025-04-28 21:22:15,512 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:15,512 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:15,515 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:15,517 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:22:15,520 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:22:15,855 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:22:15,916 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:22:15,916 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:15,916 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:15,917 INFO  L256         TraceCheckSpWp]: Trace formula consists of 472 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:15,920 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:15,991 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:22:15,991 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:15,991 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [714036213] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:15,991 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:15,991 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [16] total 19
[2025-04-28 21:22:15,991 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [29691162]
[2025-04-28 21:22:15,991 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:15,992 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:15,992 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:15,993 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:15,993 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=305, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:22:15,993 INFO  L87              Difference]: Start difference. First operand 105 states and 120 transitions. Second operand  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:22:16,031 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:16,031 INFO  L93              Difference]: Finished difference Result 107 states and 121 transitions.
[2025-04-28 21:22:16,032 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:16,032 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20) Word has length 69
[2025-04-28 21:22:16,032 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:16,033 INFO  L225             Difference]: With dead ends: 107
[2025-04-28 21:22:16,034 INFO  L226             Difference]: Without dead ends: 107
[2025-04-28 21:22:16,034 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 85 GetRequests, 68 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=37, Invalid=305, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:22:16,035 INFO  L437           NwaCegarLoop]: 95 mSDtfsCounter, 1 mSDsluCounter, 271 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 366 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:16,035 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 366 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:22:16,036 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-04-28 21:22:16,042 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 105.
[2025-04-28 21:22:16,043 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 45 states have (on average 1.1111111111111112) internal successors, (50), 50 states have internal predecessors, (50), 27 states have call successors, (29), 22 states have call predecessors, (29), 32 states have return successors, (40), 32 states have call predecessors, (40), 27 states have call successors, (40)
[2025-04-28 21:22:16,044 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 119 transitions.
[2025-04-28 21:22:16,044 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 119 transitions. Word has length 69
[2025-04-28 21:22:16,044 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:16,044 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 119 transitions.
[2025-04-28 21:22:16,044 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:22:16,045 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 119 transitions.
[2025-04-28 21:22:16,045 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-04-28 21:22:16,046 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:16,046 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:16,052 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:22:16,246 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:16,246 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:16,247 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:16,247 INFO  L85        PathProgramCache]: Analyzing trace with hash -1360013695, now seen corresponding path program 1 times
[2025-04-28 21:22:16,247 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:16,247 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1432068988]
[2025-04-28 21:22:16,247 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:16,247 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:16,258 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:22:16,266 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:22:16,266 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:16,266 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:16,321 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:22:16,321 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:16,322 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1432068988]
[2025-04-28 21:22:16,322 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1432068988] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:16,322 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:16,322 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:22:16,322 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [906446577]
[2025-04-28 21:22:16,322 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:16,323 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:22:16,323 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:16,323 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:22:16,323 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:16,324 INFO  L87              Difference]: Start difference. First operand 105 states and 119 transitions. Second operand  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:22:16,352 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:16,352 INFO  L93              Difference]: Finished difference Result 107 states and 120 transitions.
[2025-04-28 21:22:16,355 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:16,355 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20) Word has length 69
[2025-04-28 21:22:16,355 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:16,356 INFO  L225             Difference]: With dead ends: 107
[2025-04-28 21:22:16,356 INFO  L226             Difference]: Without dead ends: 106
[2025-04-28 21:22:16,356 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:16,357 INFO  L437           NwaCegarLoop]: 95 mSDtfsCounter, 1 mSDsluCounter, 270 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 365 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:16,357 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 365 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:22:16,358 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-04-28 21:22:16,371 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 104.
[2025-04-28 21:22:16,371 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 104 states, 45 states have (on average 1.0888888888888888) internal successors, (49), 49 states have internal predecessors, (49), 26 states have call successors, (28), 22 states have call predecessors, (28), 32 states have return successors, (39), 32 states have call predecessors, (39), 26 states have call successors, (39)
[2025-04-28 21:22:16,375 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 104 states to 104 states and 116 transitions.
[2025-04-28 21:22:16,376 INFO  L79                 Accepts]: Start accepts. Automaton has 104 states and 116 transitions. Word has length 69
[2025-04-28 21:22:16,376 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:16,376 INFO  L485      AbstractCegarLoop]: Abstraction has 104 states and 116 transitions.
[2025-04-28 21:22:16,376 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 7.25) internal successors, (29), 5 states have internal predecessors, (29), 3 states have call successors, (19), 1 states have call predecessors, (19), 4 states have return successors, (20), 4 states have call predecessors, (20), 3 states have call successors, (20)
[2025-04-28 21:22:16,376 INFO  L278                IsEmpty]: Start isEmpty. Operand 104 states and 116 transitions.
[2025-04-28 21:22:16,377 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-04-28 21:22:16,377 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:16,377 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:16,377 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:22:16,378 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:16,378 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:16,382 INFO  L85        PathProgramCache]: Analyzing trace with hash -366115490, now seen corresponding path program 1 times
[2025-04-28 21:22:16,382 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:16,382 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2047433759]
[2025-04-28 21:22:16,382 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:16,382 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:16,393 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:22:16,402 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:22:16,404 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:16,404 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:16,869 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:22:16,869 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:16,869 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2047433759]
[2025-04-28 21:22:16,869 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2047433759] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:16,869 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [912551553]
[2025-04-28 21:22:16,869 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:16,869 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:16,872 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:16,874 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:22:16,877 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:17,210 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 69 statements into 1 equivalence classes.
[2025-04-28 21:22:17,276 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:22:17,276 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:17,276 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:17,282 INFO  L256         TraceCheckSpWp]: Trace formula consists of 474 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:17,286 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:17,744 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:22:17,744 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
