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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:42,131 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:42,226 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e63f02fe-0090-49ae-8e5c-ccd5f3744231/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:42,235 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:42,235 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:42,273 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:42,274 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:42,274 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:42,274 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:42,274 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:42,275 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:42,275 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:42,275 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:42,275 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:42,275 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:42,275 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:42,276 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:42,277 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:42,277 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:42,278 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:42,278 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:42,278 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:42,278 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:42,278 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:42,279 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:42,280 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:42,280 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:42,628 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:42,639 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:42,642 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:42,644 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:42,645 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:42,646 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e63f02fe-0090-49ae-8e5c-ccd5f3744231/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-196.smt2
[2025-04-28 21:21:42,649 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:42,652 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:42,964 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e63f02fe-0090-49ae-8e5c-ccd5f3744231/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-196.smt2
[2025-04-28 21:21:42,968 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:42,970 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:42,973 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:42,973 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:42,973 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:42,976 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:43,010 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,012 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:43,014 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:43,014 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:43,014 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:43,030 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,030 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,063 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,063 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,068 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,073 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,075 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,080 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,081 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,102 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:43,103 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:43,103 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:43,103 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:43,104 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,110 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:43,125 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,142 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,147 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,159 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:43,159 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:43,159 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:43,159 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:43,159 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:43,160 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:43,160 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h24 given in one single declaration
[2025-04-28 21:21:43,160 INFO  L130     BoogieDeclarations]: Found specification of procedure h24
[2025-04-28 21:21:43,160 INFO  L138     BoogieDeclarations]: Found implementation of procedure h24
[2025-04-28 21:21:43,160 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h19 given in one single declaration
[2025-04-28 21:21:43,160 INFO  L130     BoogieDeclarations]: Found specification of procedure h19
[2025-04-28 21:21:43,160 INFO  L138     BoogieDeclarations]: Found implementation of procedure h19
[2025-04-28 21:21:43,160 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h18 given in one single declaration
[2025-04-28 21:21:43,160 INFO  L130     BoogieDeclarations]: Found specification of procedure h18
[2025-04-28 21:21:43,160 INFO  L138     BoogieDeclarations]: Found implementation of procedure h18
[2025-04-28 21:21:43,161 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h17 given in one single declaration
[2025-04-28 21:21:43,161 INFO  L130     BoogieDeclarations]: Found specification of procedure h17
[2025-04-28 21:21:43,161 INFO  L138     BoogieDeclarations]: Found implementation of procedure h17
[2025-04-28 21:21:43,161 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h11 given in one single declaration
[2025-04-28 21:21:43,161 INFO  L130     BoogieDeclarations]: Found specification of procedure h11
[2025-04-28 21:21:43,161 INFO  L138     BoogieDeclarations]: Found implementation of procedure h11
[2025-04-28 21:21:43,161 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h10 given in one single declaration
[2025-04-28 21:21:43,161 INFO  L130     BoogieDeclarations]: Found specification of procedure h10
[2025-04-28 21:21:43,161 INFO  L138     BoogieDeclarations]: Found implementation of procedure h10
[2025-04-28 21:21:43,161 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h9 given in one single declaration
[2025-04-28 21:21:43,162 INFO  L130     BoogieDeclarations]: Found specification of procedure h9
[2025-04-28 21:21:43,162 INFO  L138     BoogieDeclarations]: Found implementation of procedure h9
[2025-04-28 21:21:43,162 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h6 given in one single declaration
[2025-04-28 21:21:43,162 INFO  L130     BoogieDeclarations]: Found specification of procedure h6
[2025-04-28 21:21:43,162 INFO  L138     BoogieDeclarations]: Found implementation of procedure h6
[2025-04-28 21:21:43,162 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h5 given in one single declaration
[2025-04-28 21:21:43,162 INFO  L130     BoogieDeclarations]: Found specification of procedure h5
[2025-04-28 21:21:43,162 INFO  L138     BoogieDeclarations]: Found implementation of procedure h5
[2025-04-28 21:21:43,162 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h4 given in one single declaration
[2025-04-28 21:21:43,163 INFO  L130     BoogieDeclarations]: Found specification of procedure h4
[2025-04-28 21:21:43,163 INFO  L138     BoogieDeclarations]: Found implementation of procedure h4
[2025-04-28 21:21:43,163 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h3 given in one single declaration
[2025-04-28 21:21:43,163 INFO  L130     BoogieDeclarations]: Found specification of procedure h3
[2025-04-28 21:21:43,163 INFO  L138     BoogieDeclarations]: Found implementation of procedure h3
[2025-04-28 21:21:43,163 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h2 given in one single declaration
[2025-04-28 21:21:43,163 INFO  L130     BoogieDeclarations]: Found specification of procedure h2
[2025-04-28 21:21:43,163 INFO  L138     BoogieDeclarations]: Found implementation of procedure h2
[2025-04-28 21:21:43,163 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h1 given in one single declaration
[2025-04-28 21:21:43,164 INFO  L130     BoogieDeclarations]: Found specification of procedure h1
[2025-04-28 21:21:43,164 INFO  L138     BoogieDeclarations]: Found implementation of procedure h1
[2025-04-28 21:21:43,164 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h16 given in one single declaration
[2025-04-28 21:21:43,164 INFO  L130     BoogieDeclarations]: Found specification of procedure h16
[2025-04-28 21:21:43,164 INFO  L138     BoogieDeclarations]: Found implementation of procedure h16
[2025-04-28 21:21:43,164 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h13 given in one single declaration
[2025-04-28 21:21:43,164 INFO  L130     BoogieDeclarations]: Found specification of procedure h13
[2025-04-28 21:21:43,164 INFO  L138     BoogieDeclarations]: Found implementation of procedure h13
[2025-04-28 21:21:43,165 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h14 given in one single declaration
[2025-04-28 21:21:43,165 INFO  L130     BoogieDeclarations]: Found specification of procedure h14
[2025-04-28 21:21:43,165 INFO  L138     BoogieDeclarations]: Found implementation of procedure h14
[2025-04-28 21:21:43,165 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h8 given in one single declaration
[2025-04-28 21:21:43,165 INFO  L130     BoogieDeclarations]: Found specification of procedure h8
[2025-04-28 21:21:43,165 INFO  L138     BoogieDeclarations]: Found implementation of procedure h8
[2025-04-28 21:21:43,165 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h7 given in one single declaration
[2025-04-28 21:21:43,165 INFO  L130     BoogieDeclarations]: Found specification of procedure h7
[2025-04-28 21:21:43,165 INFO  L138     BoogieDeclarations]: Found implementation of procedure h7
[2025-04-28 21:21:43,165 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h12 given in one single declaration
[2025-04-28 21:21:43,166 INFO  L130     BoogieDeclarations]: Found specification of procedure h12
[2025-04-28 21:21:43,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure h12
[2025-04-28 21:21:43,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h15 given in one single declaration
[2025-04-28 21:21:43,166 INFO  L130     BoogieDeclarations]: Found specification of procedure h15
[2025-04-28 21:21:43,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure h15
[2025-04-28 21:21:43,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h20 given in one single declaration
[2025-04-28 21:21:43,166 INFO  L130     BoogieDeclarations]: Found specification of procedure h20
[2025-04-28 21:21:43,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure h20
[2025-04-28 21:21:43,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h23 given in one single declaration
[2025-04-28 21:21:43,167 INFO  L130     BoogieDeclarations]: Found specification of procedure h23
[2025-04-28 21:21:43,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure h23
[2025-04-28 21:21:43,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:43,167 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:43,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:43,314 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:43,318 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:43,570 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:43,570 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:43,591 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:43,594 INFO  L312             CfgBuilder]: Removed 14 assume(true) statements.
[2025-04-28 21:21:43,594 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:43 BoogieIcfgContainer
[2025-04-28 21:21:43,594 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:43,597 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:43,598 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:43,603 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:43,604 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:42" (1/3) ...
[2025-04-28 21:21:43,604 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@66ca4016 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:43, skipping insertion in model container
[2025-04-28 21:21:43,605 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:43,605 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@66ca4016 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:43, skipping insertion in model container
[2025-04-28 21:21:43,605 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:43" (3/3) ...
[2025-04-28 21:21:43,607 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:43,624 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:43,627 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 25 procedures, 91 locations, 129 edges, 25 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:43,671 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:43,687 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;@6cbb6f66, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:43,687 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:43,692 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 91 states, 39 states have (on average 1.0769230769230769) internal successors, (42), 42 states have internal predecessors, (42), 26 states have call successors, (29), 24 states have call predecessors, (29), 24 states have return successors, (29), 24 states have call predecessors, (29), 26 states have call successors, (29)
[2025-04-28 21:21:43,707 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-04-28 21:21:43,709 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,709 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,710 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,715 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,716 INFO  L85        PathProgramCache]: Analyzing trace with hash 1190832251, now seen corresponding path program 1 times
[2025-04-28 21:21:43,722 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,723 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1971511616]
[2025-04-28 21:21:43,723 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,723 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,775 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-04-28 21:21:43,826 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-04-28 21:21:43,826 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,826 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,300 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:44,301 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,301 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1971511616]
[2025-04-28 21:21:44,302 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1971511616] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,302 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,307 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:44,311 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1785931694]
[2025-04-28 21:21:44,312 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,316 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:44,319 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,351 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:44,352 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:44,355 INFO  L87              Difference]: Start difference. First operand  has 91 states, 39 states have (on average 1.0769230769230769) internal successors, (42), 42 states have internal predecessors, (42), 26 states have call successors, (29), 24 states have call predecessors, (29), 24 states have return successors, (29), 24 states have call predecessors, (29), 26 states have call successors, (29) Second operand  has 8 states, 7 states have (on average 3.0) internal successors, (21), 8 states have internal predecessors, (21), 3 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (15), 6 states have call predecessors, (15), 3 states have call successors, (15)
[2025-04-28 21:21:44,487 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,491 INFO  L93              Difference]: Finished difference Result 93 states and 102 transitions.
[2025-04-28 21:21:44,493 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:44,494 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 3.0) internal successors, (21), 8 states have internal predecessors, (21), 3 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (15), 6 states have call predecessors, (15), 3 states have call successors, (15) Word has length 51
[2025-04-28 21:21:44,496 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,506 INFO  L225             Difference]: With dead ends: 93
[2025-04-28 21:21:44,506 INFO  L226             Difference]: Without dead ends: 93
[2025-04-28 21:21:44,508 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:44,516 INFO  L437           NwaCegarLoop]: 92 mSDtfsCounter, 1 mSDsluCounter, 538 mSDsCounter, 0 mSdLazyCounter, 45 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 630 SdHoareTripleChecker+Invalid, 45 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 45 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,516 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 630 Invalid, 45 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 45 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:44,561 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 93 states.
[2025-04-28 21:21:44,613 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 93 to 93.
[2025-04-28 21:21:44,614 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 93 states, 40 states have (on average 1.05) internal successors, (42), 42 states have internal predecessors, (42), 26 states have call successors, (29), 24 states have call predecessors, (29), 26 states have return successors, (31), 26 states have call predecessors, (31), 26 states have call successors, (31)
[2025-04-28 21:21:44,619 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 93 states to 93 states and 102 transitions.
[2025-04-28 21:21:44,620 INFO  L79                 Accepts]: Start accepts. Automaton has 93 states and 102 transitions. Word has length 51
[2025-04-28 21:21:44,621 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,621 INFO  L485      AbstractCegarLoop]: Abstraction has 93 states and 102 transitions.
[2025-04-28 21:21:44,622 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 3.0) internal successors, (21), 8 states have internal predecessors, (21), 3 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (15), 6 states have call predecessors, (15), 3 states have call successors, (15)
[2025-04-28 21:21:44,622 INFO  L278                IsEmpty]: Start isEmpty. Operand 93 states and 102 transitions.
[2025-04-28 21:21:44,625 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-04-28 21:21:44,625 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,625 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, 1, 1, 1]
[2025-04-28 21:21:44,625 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:44,625 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,626 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,626 INFO  L85        PathProgramCache]: Analyzing trace with hash -1587880440, now seen corresponding path program 1 times
[2025-04-28 21:21:44,626 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,627 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2127849694]
[2025-04-28 21:21:44,627 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,627 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,660 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:44,682 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:44,682 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,682 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,174 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:45,177 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,178 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2127849694]
[2025-04-28 21:21:45,178 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2127849694] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,178 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,178 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:45,178 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [72046319]
[2025-04-28 21:21:45,178 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,180 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:45,181 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,182 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:45,185 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:45,186 INFO  L87              Difference]: Start difference. First operand 93 states and 102 transitions. Second operand  has 11 states, 10 states have (on average 3.0) internal successors, (30), 11 states have internal predecessors, (30), 3 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (21), 10 states have call predecessors, (21), 3 states have call successors, (21)
[2025-04-28 21:21:45,395 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,396 INFO  L93              Difference]: Finished difference Result 107 states and 117 transitions.
[2025-04-28 21:21:45,397 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:45,397 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 10 states have (on average 3.0) internal successors, (30), 11 states have internal predecessors, (30), 3 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (21), 10 states have call predecessors, (21), 3 states have call successors, (21) Word has length 72
[2025-04-28 21:21:45,398 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,399 INFO  L225             Difference]: With dead ends: 107
[2025-04-28 21:21:45,399 INFO  L226             Difference]: Without dead ends: 107
[2025-04-28 21:21:45,399 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:45,400 INFO  L437           NwaCegarLoop]: 92 mSDtfsCounter, 1 mSDsluCounter, 814 mSDsCounter, 0 mSdLazyCounter, 104 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 906 SdHoareTripleChecker+Invalid, 104 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 104 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,403 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 906 Invalid, 104 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 104 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:45,404 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-04-28 21:21:45,416 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 107.
[2025-04-28 21:21:45,416 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 107 states, 47 states have (on average 1.0425531914893618) internal successors, (49), 49 states have internal predecessors, (49), 26 states have call successors, (29), 24 states have call predecessors, (29), 33 states have return successors, (39), 33 states have call predecessors, (39), 26 states have call successors, (39)
[2025-04-28 21:21:45,418 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 107 states to 107 states and 117 transitions.
[2025-04-28 21:21:45,418 INFO  L79                 Accepts]: Start accepts. Automaton has 107 states and 117 transitions. Word has length 72
[2025-04-28 21:21:45,419 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,419 INFO  L485      AbstractCegarLoop]: Abstraction has 107 states and 117 transitions.
[2025-04-28 21:21:45,419 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 10 states have (on average 3.0) internal successors, (30), 11 states have internal predecessors, (30), 3 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (21), 10 states have call predecessors, (21), 3 states have call successors, (21)
[2025-04-28 21:21:45,419 INFO  L278                IsEmpty]: Start isEmpty. Operand 107 states and 117 transitions.
[2025-04-28 21:21:45,421 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-04-28 21:21:45,421 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,421 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, 1, 1, 1]
[2025-04-28 21:21:45,422 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:45,422 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,422 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,423 INFO  L85        PathProgramCache]: Analyzing trace with hash -2076205816, now seen corresponding path program 1 times
[2025-04-28 21:21:45,423 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,423 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1297114906]
[2025-04-28 21:21:45,423 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,423 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,439 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:45,448 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:45,449 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,449 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,705 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:45,705 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,705 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1297114906]
[2025-04-28 21:21:45,706 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1297114906] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,706 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,706 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:45,706 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [919260467]
[2025-04-28 21:21:45,706 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,706 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:45,706 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,707 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:45,707 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:45,707 INFO  L87              Difference]: Start difference. First operand 107 states and 117 transitions. Second operand  has 11 states, 10 states have (on average 3.0) internal successors, (30), 11 states have internal predecessors, (30), 3 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (21), 10 states have call predecessors, (21), 3 states have call successors, (21)
[2025-04-28 21:21:45,843 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,843 INFO  L93              Difference]: Finished difference Result 107 states and 116 transitions.
[2025-04-28 21:21:45,844 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:45,845 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 10 states have (on average 3.0) internal successors, (30), 11 states have internal predecessors, (30), 3 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (21), 10 states have call predecessors, (21), 3 states have call successors, (21) Word has length 72
[2025-04-28 21:21:45,845 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,849 INFO  L225             Difference]: With dead ends: 107
[2025-04-28 21:21:45,849 INFO  L226             Difference]: Without dead ends: 99
[2025-04-28 21:21:45,849 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:45,850 INFO  L437           NwaCegarLoop]: 93 mSDtfsCounter, 1 mSDsluCounter, 823 mSDsCounter, 0 mSdLazyCounter, 94 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 916 SdHoareTripleChecker+Invalid, 94 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 94 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,850 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 916 Invalid, 94 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 94 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,851 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 99 states.
[2025-04-28 21:21:45,861 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 99 to 95.
[2025-04-28 21:21:45,862 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 95 states, 41 states have (on average 1.048780487804878) internal successors, (43), 43 states have internal predecessors, (43), 26 states have call successors, (29), 24 states have call predecessors, (29), 27 states have return successors, (32), 27 states have call predecessors, (32), 26 states have call successors, (32)
[2025-04-28 21:21:45,863 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 95 states to 95 states and 104 transitions.
[2025-04-28 21:21:45,863 INFO  L79                 Accepts]: Start accepts. Automaton has 95 states and 104 transitions. Word has length 72
[2025-04-28 21:21:45,864 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,864 INFO  L485      AbstractCegarLoop]: Abstraction has 95 states and 104 transitions.
[2025-04-28 21:21:45,864 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 10 states have (on average 3.0) internal successors, (30), 11 states have internal predecessors, (30), 3 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (21), 10 states have call predecessors, (21), 3 states have call successors, (21)
[2025-04-28 21:21:45,864 INFO  L278                IsEmpty]: Start isEmpty. Operand 95 states and 104 transitions.
[2025-04-28 21:21:45,866 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-04-28 21:21:45,866 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,867 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,867 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:45,867 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,867 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,868 INFO  L85        PathProgramCache]: Analyzing trace with hash 1967911707, now seen corresponding path program 1 times
[2025-04-28 21:21:45,870 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,870 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [539705031]
[2025-04-28 21:21:45,870 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,871 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,898 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:45,911 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:45,912 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,912 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,377 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,378 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,378 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [539705031]
[2025-04-28 21:21:46,378 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [539705031] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,378 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,378 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [12] imperfect sequences [] total 12
[2025-04-28 21:21:46,378 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1746753147]
[2025-04-28 21:21:46,378 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,379 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:46,379 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,379 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:46,380 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=111, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:46,380 INFO  L87              Difference]: Start difference. First operand 95 states and 104 transitions. Second operand  has 12 states, 11 states have (on average 2.909090909090909) internal successors, (32), 12 states have internal predecessors, (32), 3 states have call successors, (21), 1 states have call predecessors, (21), 11 states have return successors, (22), 11 states have call predecessors, (22), 3 states have call successors, (22)
[2025-04-28 21:21:46,561 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,562 INFO  L93              Difference]: Finished difference Result 111 states and 121 transitions.
[2025-04-28 21:21:46,563 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:46,563 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 11 states have (on average 2.909090909090909) internal successors, (32), 12 states have internal predecessors, (32), 3 states have call successors, (21), 1 states have call predecessors, (21), 11 states have return successors, (22), 11 states have call predecessors, (22), 3 states have call successors, (22) Word has length 76
[2025-04-28 21:21:46,564 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,566 INFO  L225             Difference]: With dead ends: 111
[2025-04-28 21:21:46,566 INFO  L226             Difference]: Without dead ends: 111
[2025-04-28 21:21:46,567 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 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,568 INFO  L437           NwaCegarLoop]: 104 mSDtfsCounter, 1 mSDsluCounter, 1014 mSDsCounter, 0 mSdLazyCounter, 125 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1118 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:46,568 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1118 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:46,569 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 111 states.
[2025-04-28 21:21:46,585 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 111 to 111.
[2025-04-28 21:21:46,586 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 111 states, 49 states have (on average 1.0408163265306123) internal successors, (51), 51 states have internal predecessors, (51), 26 states have call successors, (29), 24 states have call predecessors, (29), 35 states have return successors, (41), 35 states have call predecessors, (41), 26 states have call successors, (41)
[2025-04-28 21:21:46,587 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 111 states to 111 states and 121 transitions.
[2025-04-28 21:21:46,587 INFO  L79                 Accepts]: Start accepts. Automaton has 111 states and 121 transitions. Word has length 76
[2025-04-28 21:21:46,591 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,591 INFO  L485      AbstractCegarLoop]: Abstraction has 111 states and 121 transitions.
[2025-04-28 21:21:46,591 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 11 states have (on average 2.909090909090909) internal successors, (32), 12 states have internal predecessors, (32), 3 states have call successors, (21), 1 states have call predecessors, (21), 11 states have return successors, (22), 11 states have call predecessors, (22), 3 states have call successors, (22)
[2025-04-28 21:21:46,591 INFO  L278                IsEmpty]: Start isEmpty. Operand 111 states and 121 transitions.
[2025-04-28 21:21:46,593 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-04-28 21:21:46,593 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,593 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,597 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:46,597 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,598 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,598 INFO  L85        PathProgramCache]: Analyzing trace with hash -137751382, now seen corresponding path program 1 times
[2025-04-28 21:21:46,598 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,598 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1247584427]
[2025-04-28 21:21:46,598 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,598 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,629 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:46,650 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:46,650 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,650 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,366 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,367 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,367 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1247584427]
[2025-04-28 21:21:47,367 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1247584427] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,367 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1307050672]
[2025-04-28 21:21:47,367 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,367 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,370 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,372 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,378 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,481 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:47,587 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:47,587 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,587 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,592 INFO  L256         TraceCheckSpWp]: Trace formula consists of 516 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,603 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,807 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,809 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:07,778 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:07,778 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1307050672] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:07,778 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:07,779 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [22, 22, 22] total 25
[2025-04-28 21:22:07,779 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [801184472]
[2025-04-28 21:22:07,779 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,780 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:22:07,782 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,784 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:22:07,785 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=546, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:22:07,785 INFO  L87              Difference]: Start difference. First operand 111 states and 121 transitions. Second operand  has 25 states, 20 states have (on average 1.75) internal successors, (35), 25 states have internal predecessors, (35), 7 states have call successors, (24), 1 states have call predecessors, (24), 20 states have return successors, (25), 19 states have call predecessors, (25), 7 states have call successors, (25)
[2025-04-28 21:22:08,145 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:08,145 INFO  L93              Difference]: Finished difference Result 141 states and 155 transitions.
[2025-04-28 21:22:08,146 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 22 states. 
[2025-04-28 21:22:08,146 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 20 states have (on average 1.75) internal successors, (35), 25 states have internal predecessors, (35), 7 states have call successors, (24), 1 states have call predecessors, (24), 20 states have return successors, (25), 19 states have call predecessors, (25), 7 states have call successors, (25) Word has length 76
[2025-04-28 21:22:08,146 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,148 INFO  L225             Difference]: With dead ends: 141
[2025-04-28 21:22:08,148 INFO  L226             Difference]: Without dead ends: 141
[2025-04-28 21:22:08,148 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 174 GetRequests, 132 SyntacticMatches, 18 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 92 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=60, Invalid=590, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:22:08,149 INFO  L437           NwaCegarLoop]: 81 mSDtfsCounter, 5 mSDsluCounter, 1354 mSDsCounter, 0 mSdLazyCounter, 392 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1435 SdHoareTripleChecker+Invalid, 397 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 392 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,149 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1435 Invalid, 397 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 392 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:08,150 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 141 states.
[2025-04-28 21:22:08,160 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 141 to 141.
[2025-04-28 21:22:08,161 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 141 states, 64 states have (on average 1.03125) internal successors, (66), 66 states have internal predecessors, (66), 26 states have call successors, (29), 24 states have call predecessors, (29), 50 states have return successors, (60), 50 states have call predecessors, (60), 26 states have call successors, (60)
[2025-04-28 21:22:08,162 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 141 states to 141 states and 155 transitions.
[2025-04-28 21:22:08,162 INFO  L79                 Accepts]: Start accepts. Automaton has 141 states and 155 transitions. Word has length 76
[2025-04-28 21:22:08,163 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,163 INFO  L485      AbstractCegarLoop]: Abstraction has 141 states and 155 transitions.
[2025-04-28 21:22:08,163 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 20 states have (on average 1.75) internal successors, (35), 25 states have internal predecessors, (35), 7 states have call successors, (24), 1 states have call predecessors, (24), 20 states have return successors, (25), 19 states have call predecessors, (25), 7 states have call successors, (25)
[2025-04-28 21:22:08,163 INFO  L278                IsEmpty]: Start isEmpty. Operand 141 states and 155 transitions.
[2025-04-28 21:22:08,165 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-04-28 21:22:08,165 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,165 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:08,173 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:08,369 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:22:08,369 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:08,370 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:08,370 INFO  L85        PathProgramCache]: Analyzing trace with hash 388053217, now seen corresponding path program 1 times
[2025-04-28 21:22:08,370 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:08,370 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2016781970]
[2025-04-28 21:22:08,370 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:08,370 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:08,387 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:22:08,400 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:22:08,401 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:08,401 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,947 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:08,947 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:08,948 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2016781970]
[2025-04-28 21:22:08,948 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2016781970] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:08,948 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1774563048]
[2025-04-28 21:22:08,948 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:08,948 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:08,950 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:08,955 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:22:08,967 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:22:09,343 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:22:09,420 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:22:09,420 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:09,420 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,424 INFO  L256         TraceCheckSpWp]: Trace formula consists of 516 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:09,427 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:09,551 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:09,551 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
