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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:51,270 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:51,371 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53e10b7d-fb32-45c2-96a9-0d07f2382865/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:51,380 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:51,380 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:51,423 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:51,423 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:51,424 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:51,426 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:51,426 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:51,427 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:51,428 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:51,428 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:51,428 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:51,429 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:51,429 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:51,429 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:51,429 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:51,429 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:51,429 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:51,430 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:51,430 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:51,430 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:51,430 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:51,430 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:51,431 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:51,431 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:51,774 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:51,785 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:51,788 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:51,791 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:51,792 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:51,793 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53e10b7d-fb32-45c2-96a9-0d07f2382865/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-217.smt2
[2025-04-28 21:21:51,797 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:51,801 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:52,249 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53e10b7d-fb32-45c2-96a9-0d07f2382865/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-217.smt2
[2025-04-28 21:21:52,252 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:52,253 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:52,256 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:52,256 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:52,256 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:52,259 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,322 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52 Unit
[2025-04-28 21:21:52,326 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:52,329 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:52,329 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:52,329 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:52,350 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,350 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,404 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,404 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,413 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,419 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,425 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,430 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,432 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,465 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:52,469 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:52,469 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:52,469 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:52,470 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,477 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:52,493 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,509 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:52,513 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:52,529 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:52,530 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:52,530 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:52,530 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_4_0 given in one single declaration
[2025-04-28 21:21:52,530 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_4_0
[2025-04-28 21:21:52,530 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_4_0
[2025-04-28 21:21:52,530 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_45_0 given in one single declaration
[2025-04-28 21:21:52,531 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_45_0
[2025-04-28 21:21:52,531 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_45_0
[2025-04-28 21:21:52,531 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_45_0 given in one single declaration
[2025-04-28 21:21:52,531 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_45_0
[2025-04-28 21:21:52,531 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_45_0
[2025-04-28 21:21:52,531 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_12_C_45_0 given in one single declaration
[2025-04-28 21:21:52,531 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_12_C_45_0
[2025-04-28 21:21:52,531 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_12_C_45_0
[2025-04-28 21:21:52,532 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_14_C_45_0 given in one single declaration
[2025-04-28 21:21:52,532 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_14_C_45_0
[2025-04-28 21:21:52,534 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_14_C_45_0
[2025-04-28 21:21:52,534 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_13_C_45_0 given in one single declaration
[2025-04-28 21:21:52,534 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_13_C_45_0
[2025-04-28 21:21:52,534 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_13_C_45_0
[2025-04-28 21:21:52,534 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_15_C_45_0 given in one single declaration
[2025-04-28 21:21:52,534 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_15_C_45_0
[2025-04-28 21:21:52,534 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_15_C_45_0
[2025-04-28 21:21:52,535 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_g__44_45_0 given in one single declaration
[2025-04-28 21:21:52,535 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_g__44_45_0
[2025-04-28 21:21:52,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_g__44_45_0
[2025-04-28 21:21:52,535 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_function_g__44_45_0 given in one single declaration
[2025-04-28 21:21:52,535 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_function_g__44_45_0
[2025-04-28 21:21:52,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_function_g__44_45_0
[2025-04-28 21:21:52,535 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_g__44_45_0 given in one single declaration
[2025-04-28 21:21:52,535 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_g__44_45_0
[2025-04-28 21:21:52,535 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_g__44_45_0
[2025-04-28 21:21:52,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_function_g__44_45_0 given in one single declaration
[2025-04-28 21:21:52,536 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_function_g__44_45_0
[2025-04-28 21:21:52,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_function_g__44_45_0
[2025-04-28 21:21:52,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure nondet_call_8_0 given in one single declaration
[2025-04-28 21:21:52,536 INFO  L130     BoogieDeclarations]: Found specification of procedure nondet_call_8_0
[2025-04-28 21:21:52,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure nondet_call_8_0
[2025-04-28 21:21:52,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure nondet_interface_1_C_45_0 given in one single declaration
[2025-04-28 21:21:52,536 INFO  L130     BoogieDeclarations]: Found specification of procedure nondet_interface_1_C_45_0
[2025-04-28 21:21:52,536 INFO  L138     BoogieDeclarations]: Found implementation of procedure nondet_interface_1_C_45_0
[2025-04-28 21:21:52,536 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_6_g_43_45_0 given in one single declaration
[2025-04-28 21:21:52,537 INFO  L130     BoogieDeclarations]: Found specification of procedure block_6_g_43_45_0
[2025-04-28 21:21:52,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_6_g_43_45_0
[2025-04-28 21:21:52,537 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_5_function_g__44_45_0 given in one single declaration
[2025-04-28 21:21:52,537 INFO  L130     BoogieDeclarations]: Found specification of procedure block_5_function_g__44_45_0
[2025-04-28 21:21:52,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_5_function_g__44_45_0
[2025-04-28 21:21:52,537 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_return_function_g__44_45_0 given in one single declaration
[2025-04-28 21:21:52,537 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_return_function_g__44_45_0
[2025-04-28 21:21:52,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_return_function_g__44_45_0
[2025-04-28 21:21:52,537 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_function_g__44_45_0 given in one single declaration
[2025-04-28 21:21:52,537 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_function_g__44_45_0
[2025-04-28 21:21:52,537 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_function_g__44_45_0
[2025-04-28 21:21:52,538 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:52,538 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:52,538 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:52,751 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:52,753 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:53,130 INFO  L?                        ?]: Removed 166 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:53,130 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:53,147 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:53,147 INFO  L312             CfgBuilder]: Removed 9 assume(true) statements.
[2025-04-28 21:21:53,148 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:53 BoogieIcfgContainer
[2025-04-28 21:21:53,152 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:53,154 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:53,154 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:53,160 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:53,160 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:52" (1/3) ...
[2025-04-28 21:21:53,160 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@68c18574 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:53, skipping insertion in model container
[2025-04-28 21:21:53,161 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (2/3) ...
[2025-04-28 21:21:53,161 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@68c18574 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:53, skipping insertion in model container
[2025-04-28 21:21:53,161 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:53" (3/3) ...
[2025-04-28 21:21:53,162 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:53,173 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:53,176 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 19 procedures, 79 locations, 126 edges, 19 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:53,220 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:53,231 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;@14bfbf35, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:53,231 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:53,235 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 79 states, 32 states have (on average 1.125) internal successors, (36), 36 states have internal predecessors, (36), 28 states have call successors, (30), 18 states have call predecessors, (30), 18 states have return successors, (30), 25 states have call predecessors, (30), 28 states have call successors, (30)
[2025-04-28 21:21:53,245 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 56
[2025-04-28 21:21:53,246 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,246 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, 1, 1, 1, 1]
[2025-04-28 21:21:53,247 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,251 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,252 INFO  L85        PathProgramCache]: Analyzing trace with hash -200191179, now seen corresponding path program 1 times
[2025-04-28 21:21:53,259 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,260 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [394008734]
[2025-04-28 21:21:53,260 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,261 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,335 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 55 statements into 1 equivalence classes.
[2025-04-28 21:21:53,458 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 55 of 55 statements.
[2025-04-28 21:21:53,458 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,458 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,832 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:53,832 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,832 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [394008734]
[2025-04-28 21:21:53,833 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [394008734] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,833 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,836 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:53,838 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2024156263]
[2025-04-28 21:21:53,841 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,846 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:53,846 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,876 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:53,877 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:53,879 INFO  L87              Difference]: Start difference. First operand  has 79 states, 32 states have (on average 1.125) internal successors, (36), 36 states have internal predecessors, (36), 28 states have call successors, (30), 18 states have call predecessors, (30), 18 states have return successors, (30), 25 states have call predecessors, (30), 28 states have call successors, (30) Second operand  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 3 states have call successors, (15), 1 states have call predecessors, (15), 4 states have return successors, (15), 4 states have call predecessors, (15), 3 states have call successors, (15)
[2025-04-28 21:21:54,124 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,125 INFO  L93              Difference]: Finished difference Result 83 states and 103 transitions.
[2025-04-28 21:21:54,127 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:54,129 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 3 states have call successors, (15), 1 states have call predecessors, (15), 4 states have return successors, (15), 4 states have call predecessors, (15), 3 states have call successors, (15) Word has length 55
[2025-04-28 21:21:54,130 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,140 INFO  L225             Difference]: With dead ends: 83
[2025-04-28 21:21:54,140 INFO  L226             Difference]: Without dead ends: 83
[2025-04-28 21:21:54,142 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:54,149 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 1 mSDsluCounter, 259 mSDsCounter, 0 mSdLazyCounter, 30 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 349 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 30 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,150 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 349 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 30 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:54,166 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 83 states.
[2025-04-28 21:21:54,203 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 83 to 81.
[2025-04-28 21:21:54,204 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 81 states, 33 states have (on average 1.0909090909090908) internal successors, (36), 36 states have internal predecessors, (36), 28 states have call successors, (30), 18 states have call predecessors, (30), 20 states have return successors, (35), 26 states have call predecessors, (35), 28 states have call successors, (35)
[2025-04-28 21:21:54,210 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 81 states to 81 states and 101 transitions.
[2025-04-28 21:21:54,211 INFO  L79                 Accepts]: Start accepts. Automaton has 81 states and 101 transitions. Word has length 55
[2025-04-28 21:21:54,212 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,212 INFO  L485      AbstractCegarLoop]: Abstraction has 81 states and 101 transitions.
[2025-04-28 21:21:54,212 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 6.25) internal successors, (25), 5 states have internal predecessors, (25), 3 states have call successors, (15), 1 states have call predecessors, (15), 4 states have return successors, (15), 4 states have call predecessors, (15), 3 states have call successors, (15)
[2025-04-28 21:21:54,213 INFO  L278                IsEmpty]: Start isEmpty. Operand 81 states and 101 transitions.
[2025-04-28 21:21:54,216 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-04-28 21:21:54,217 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,217 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,217 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:54,218 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,218 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,218 INFO  L85        PathProgramCache]: Analyzing trace with hash 1415991210, now seen corresponding path program 1 times
[2025-04-28 21:21:54,219 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,219 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1101372254]
[2025-04-28 21:21:54,219 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,219 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,292 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-04-28 21:21:54,376 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-04-28 21:21:54,376 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,376 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,701 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:54,702 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,702 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1101372254]
[2025-04-28 21:21:54,702 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1101372254] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,702 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,702 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:54,702 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [303150866]
[2025-04-28 21:21:54,702 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,703 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:54,703 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,704 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:54,704 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:54,706 INFO  L87              Difference]: Start difference. First operand 81 states and 101 transitions. Second operand  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 5 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 5 states have call successors, (16)
[2025-04-28 21:21:54,796 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,796 INFO  L93              Difference]: Finished difference Result 86 states and 108 transitions.
[2025-04-28 21:21:54,797 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:54,797 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 5 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 5 states have call successors, (16) Word has length 58
[2025-04-28 21:21:54,798 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,800 INFO  L225             Difference]: With dead ends: 86
[2025-04-28 21:21:54,800 INFO  L226             Difference]: Without dead ends: 86
[2025-04-28 21:21:54,800 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:54,801 INFO  L437           NwaCegarLoop]: 96 mSDtfsCounter, 1 mSDsluCounter, 367 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 463 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,801 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 463 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:54,802 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-04-28 21:21:54,819 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 86.
[2025-04-28 21:21:54,821 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 86 states, 35 states have (on average 1.0857142857142856) internal successors, (38), 38 states have internal predecessors, (38), 29 states have call successors, (31), 18 states have call predecessors, (31), 22 states have return successors, (39), 29 states have call predecessors, (39), 29 states have call successors, (39)
[2025-04-28 21:21:54,825 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 108 transitions.
[2025-04-28 21:21:54,825 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 108 transitions. Word has length 58
[2025-04-28 21:21:54,826 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,826 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 108 transitions.
[2025-04-28 21:21:54,826 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 5 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 5 states have call successors, (16)
[2025-04-28 21:21:54,826 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 108 transitions.
[2025-04-28 21:21:54,829 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-04-28 21:21:54,830 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,830 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,830 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:54,831 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,831 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,831 INFO  L85        PathProgramCache]: Analyzing trace with hash -1076256282, now seen corresponding path program 1 times
[2025-04-28 21:21:54,831 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,832 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [972702118]
[2025-04-28 21:21:54,832 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,832 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,866 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-04-28 21:21:54,882 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-04-28 21:21:54,882 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,882 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,082 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:55,082 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,082 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [972702118]
[2025-04-28 21:21:55,082 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [972702118] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,082 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,083 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:55,083 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [860548047]
[2025-04-28 21:21:55,083 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,083 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:55,083 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,084 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:55,084 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:55,084 INFO  L87              Difference]: Start difference. First operand 86 states and 108 transitions. Second operand  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:55,112 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,114 INFO  L93              Difference]: Finished difference Result 90 states and 112 transitions.
[2025-04-28 21:21:55,115 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:55,115 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16) Word has length 58
[2025-04-28 21:21:55,115 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,117 INFO  L225             Difference]: With dead ends: 90
[2025-04-28 21:21:55,118 INFO  L226             Difference]: Without dead ends: 86
[2025-04-28 21:21:55,118 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:55,119 INFO  L437           NwaCegarLoop]: 95 mSDtfsCounter, 1 mSDsluCounter, 182 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 277 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,119 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 277 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:55,120 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-04-28 21:21:55,128 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 84.
[2025-04-28 21:21:55,128 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 35 states have (on average 1.0571428571428572) internal successors, (37), 37 states have internal predecessors, (37), 27 states have call successors, (29), 18 states have call predecessors, (29), 22 states have return successors, (37), 28 states have call predecessors, (37), 27 states have call successors, (37)
[2025-04-28 21:21:55,130 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 103 transitions.
[2025-04-28 21:21:55,130 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 103 transitions. Word has length 58
[2025-04-28 21:21:55,130 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,130 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 103 transitions.
[2025-04-28 21:21:55,131 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:55,131 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 103 transitions.
[2025-04-28 21:21:55,132 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-04-28 21:21:55,133 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,133 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,133 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:55,133 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,134 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,134 INFO  L85        PathProgramCache]: Analyzing trace with hash 11951210, now seen corresponding path program 1 times
[2025-04-28 21:21:55,134 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,134 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [993286459]
[2025-04-28 21:21:55,134 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,134 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,179 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-04-28 21:21:55,198 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-04-28 21:21:55,198 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,198 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,396 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:55,396 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,396 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [993286459]
[2025-04-28 21:21:55,396 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [993286459] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,397 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,397 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:55,397 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1363951891]
[2025-04-28 21:21:55,397 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,398 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:55,398 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,399 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:55,399 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,399 INFO  L87              Difference]: Start difference. First operand 84 states and 103 transitions. Second operand  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 5 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 5 states have call successors, (16)
[2025-04-28 21:21:55,485 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,485 INFO  L93              Difference]: Finished difference Result 89 states and 110 transitions.
[2025-04-28 21:21:55,486 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:55,486 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 5 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 5 states have call successors, (16) Word has length 58
[2025-04-28 21:21:55,488 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,490 INFO  L225             Difference]: With dead ends: 89
[2025-04-28 21:21:55,490 INFO  L226             Difference]: Without dead ends: 89
[2025-04-28 21:21:55,490 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,491 INFO  L437           NwaCegarLoop]: 91 mSDtfsCounter, 1 mSDsluCounter, 347 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 438 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,495 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 438 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:55,496 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 89 states.
[2025-04-28 21:21:55,506 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 89 to 84.
[2025-04-28 21:21:55,510 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 35 states have (on average 1.0571428571428572) internal successors, (37), 37 states have internal predecessors, (37), 27 states have call successors, (29), 18 states have call predecessors, (29), 22 states have return successors, (37), 28 states have call predecessors, (37), 27 states have call successors, (37)
[2025-04-28 21:21:55,512 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 103 transitions.
[2025-04-28 21:21:55,512 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 103 transitions. Word has length 58
[2025-04-28 21:21:55,514 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,514 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 103 transitions.
[2025-04-28 21:21:55,514 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 5 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 5 states have call successors, (16)
[2025-04-28 21:21:55,514 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 103 transitions.
[2025-04-28 21:21:55,516 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-04-28 21:21:55,519 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,520 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,520 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:55,520 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,520 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,521 INFO  L85        PathProgramCache]: Analyzing trace with hash 431284010, now seen corresponding path program 1 times
[2025-04-28 21:21:55,521 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,521 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1693358235]
[2025-04-28 21:21:55,521 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,521 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,560 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-04-28 21:21:55,598 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-04-28 21:21:55,600 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,600 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,699 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:56,699 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,699 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1693358235]
[2025-04-28 21:21:56,699 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1693358235] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:56,699 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:56,699 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:56,699 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [298371494]
[2025-04-28 21:21:56,699 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,700 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:56,700 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,700 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:56,700 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:56,701 INFO  L87              Difference]: Start difference. First operand 84 states and 103 transitions. Second operand  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 4 states have call successors, (16)
[2025-04-28 21:21:56,834 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,834 INFO  L93              Difference]: Finished difference Result 84 states and 102 transitions.
[2025-04-28 21:21:56,835 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:56,835 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 4 states have call successors, (16) Word has length 58
[2025-04-28 21:21:56,835 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,836 INFO  L225             Difference]: With dead ends: 84
[2025-04-28 21:21:56,836 INFO  L226             Difference]: Without dead ends: 84
[2025-04-28 21:21:56,837 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 6 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:56,837 INFO  L437           NwaCegarLoop]: 80 mSDtfsCounter, 1 mSDsluCounter, 303 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 383 SdHoareTripleChecker+Invalid, 54 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,838 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 383 Invalid, 54 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,838 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 84 states.
[2025-04-28 21:21:56,852 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 84 to 84.
[2025-04-28 21:21:56,852 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 35 states have (on average 1.0571428571428572) internal successors, (37), 37 states have internal predecessors, (37), 27 states have call successors, (29), 18 states have call predecessors, (29), 22 states have return successors, (36), 28 states have call predecessors, (36), 27 states have call successors, (36)
[2025-04-28 21:21:56,853 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 102 transitions.
[2025-04-28 21:21:56,856 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 102 transitions. Word has length 58
[2025-04-28 21:21:56,856 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,856 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 102 transitions.
[2025-04-28 21:21:56,857 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 4 states have call successors, (16)
[2025-04-28 21:21:56,857 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 102 transitions.
[2025-04-28 21:21:56,859 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 88
[2025-04-28 21:21:56,861 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,861 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,861 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:56,861 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,862 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,863 INFO  L85        PathProgramCache]: Analyzing trace with hash -2132354008, now seen corresponding path program 1 times
[2025-04-28 21:21:56,863 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,863 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1511231027]
[2025-04-28 21:21:56,863 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,863 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,920 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 87 statements into 1 equivalence classes.
[2025-04-28 21:21:56,959 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 87 of 87 statements.
[2025-04-28 21:21:56,959 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,959 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,242 INFO  L134       CoverageAnalysis]: Checked inductivity of 28 backedges. 11 proven. 0 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-04-28 21:21:57,242 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,242 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1511231027]
[2025-04-28 21:21:57,242 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1511231027] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:57,242 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:57,242 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:57,242 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1822446607]
[2025-04-28 21:21:57,242 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,243 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:57,243 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,243 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:57,244 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:57,244 INFO  L87              Difference]: Start difference. First operand 84 states and 102 transitions. Second operand  has 8 states, 7 states have (on average 4.571428571428571) internal successors, (32), 8 states have internal predecessors, (32), 6 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (23), 8 states have call predecessors, (23), 6 states have call successors, (23)
[2025-04-28 21:21:57,419 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,419 INFO  L93              Difference]: Finished difference Result 96 states and 122 transitions.
[2025-04-28 21:21:57,420 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:57,420 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 4.571428571428571) internal successors, (32), 8 states have internal predecessors, (32), 6 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (23), 8 states have call predecessors, (23), 6 states have call successors, (23) Word has length 87
[2025-04-28 21:21:57,422 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,423 INFO  L225             Difference]: With dead ends: 96
[2025-04-28 21:21:57,423 INFO  L226             Difference]: Without dead ends: 96
[2025-04-28 21:21:57,423 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:57,424 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 1 mSDsluCounter, 509 mSDsCounter, 0 mSdLazyCounter, 92 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 599 SdHoareTripleChecker+Invalid, 93 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 92 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,424 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 599 Invalid, 93 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 92 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:57,428 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 96 states.
[2025-04-28 21:21:57,441 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 96 to 94.
[2025-04-28 21:21:57,445 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 39 states have (on average 1.0512820512820513) internal successors, (41), 41 states have internal predecessors, (41), 29 states have call successors, (31), 18 states have call predecessors, (31), 26 states have return successors, (48), 34 states have call predecessors, (48), 29 states have call successors, (48)
[2025-04-28 21:21:57,446 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 120 transitions.
[2025-04-28 21:21:57,446 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 120 transitions. Word has length 87
[2025-04-28 21:21:57,446 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,446 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 120 transitions.
[2025-04-28 21:21:57,447 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 4.571428571428571) internal successors, (32), 8 states have internal predecessors, (32), 6 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (23), 8 states have call predecessors, (23), 6 states have call successors, (23)
[2025-04-28 21:21:57,447 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 120 transitions.
[2025-04-28 21:21:57,448 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 88
[2025-04-28 21:21:57,448 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,448 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:57,448 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:57,448 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,452 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,452 INFO  L85        PathProgramCache]: Analyzing trace with hash 1399455976, now seen corresponding path program 1 times
[2025-04-28 21:21:57,452 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,452 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1088858242]
[2025-04-28 21:21:57,452 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,452 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,501 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 87 statements into 1 equivalence classes.
[2025-04-28 21:21:57,531 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 87 of 87 statements.
[2025-04-28 21:21:57,532 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,532 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,818 INFO  L134       CoverageAnalysis]: Checked inductivity of 28 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 22 trivial. 0 not checked.
[2025-04-28 21:21:57,818 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,818 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1088858242]
[2025-04-28 21:21:57,818 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1088858242] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:57,818 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:57,818 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:57,818 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1669052163]
[2025-04-28 21:21:57,819 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,819 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:57,822 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,823 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:57,823 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:57,823 INFO  L87              Difference]: Start difference. First operand 94 states and 120 transitions. Second operand  has 8 states, 7 states have (on average 4.285714285714286) internal successors, (30), 8 states have internal predecessors, (30), 6 states have call successors, (20), 1 states have call predecessors, (20), 7 states have return successors, (21), 7 states have call predecessors, (21), 6 states have call successors, (21)
[2025-04-28 21:21:57,979 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,980 INFO  L93              Difference]: Finished difference Result 104 states and 141 transitions.
[2025-04-28 21:21:57,980 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:57,981 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 4.285714285714286) internal successors, (30), 8 states have internal predecessors, (30), 6 states have call successors, (20), 1 states have call predecessors, (20), 7 states have return successors, (21), 7 states have call predecessors, (21), 6 states have call successors, (21) Word has length 87
[2025-04-28 21:21:57,981 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,982 INFO  L225             Difference]: With dead ends: 104
[2025-04-28 21:21:57,985 INFO  L226             Difference]: Without dead ends: 104
[2025-04-28 21:21:57,985 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:57,986 INFO  L437           NwaCegarLoop]: 88 mSDtfsCounter, 1 mSDsluCounter, 502 mSDsCounter, 0 mSdLazyCounter, 88 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 590 SdHoareTripleChecker+Invalid, 88 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 88 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,986 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 590 Invalid, 88 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 88 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:57,987 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 104 states.
[2025-04-28 21:21:58,008 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 104 to 99.
[2025-04-28 21:21:58,009 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 99 states, 41 states have (on average 1.048780487804878) internal successors, (43), 43 states have internal predecessors, (43), 30 states have call successors, (32), 18 states have call predecessors, (32), 28 states have return successors, (59), 37 states have call predecessors, (59), 30 states have call successors, (59)
[2025-04-28 21:21:58,012 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 99 states to 99 states and 134 transitions.
[2025-04-28 21:21:58,013 INFO  L79                 Accepts]: Start accepts. Automaton has 99 states and 134 transitions. Word has length 87
[2025-04-28 21:21:58,015 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,016 INFO  L485      AbstractCegarLoop]: Abstraction has 99 states and 134 transitions.
[2025-04-28 21:21:58,016 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 4.285714285714286) internal successors, (30), 8 states have internal predecessors, (30), 6 states have call successors, (20), 1 states have call predecessors, (20), 7 states have return successors, (21), 7 states have call predecessors, (21), 6 states have call successors, (21)
[2025-04-28 21:21:58,016 INFO  L278                IsEmpty]: Start isEmpty. Operand 99 states and 134 transitions.
[2025-04-28 21:21:58,018 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-04-28 21:21:58,018 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,018 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:58,018 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:58,018 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,019 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,019 INFO  L85        PathProgramCache]: Analyzing trace with hash 1821903901, now seen corresponding path program 1 times
[2025-04-28 21:21:58,022 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,022 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1690790129]
[2025-04-28 21:21:58,022 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,022 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,082 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-04-28 21:21:58,098 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-04-28 21:21:58,098 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,099 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,380 INFO  L134       CoverageAnalysis]: Checked inductivity of 28 backedges. 11 proven. 0 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-04-28 21:21:58,380 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,380 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1690790129]
[2025-04-28 21:21:58,380 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1690790129] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:58,380 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:58,380 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:58,380 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [633600028]
[2025-04-28 21:21:58,381 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,381 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:58,381 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,382 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:58,382 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:58,382 INFO  L87              Difference]: Start difference. First operand 99 states and 134 transitions. Second operand  has 8 states, 7 states have (on average 4.714285714285714) internal successors, (33), 8 states have internal predecessors, (33), 6 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (24), 8 states have call predecessors, (24), 6 states have call successors, (24)
[2025-04-28 21:21:58,505 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,505 INFO  L93              Difference]: Finished difference Result 99 states and 133 transitions.
[2025-04-28 21:21:58,506 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:58,506 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 4.714285714285714) internal successors, (33), 8 states have internal predecessors, (33), 6 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (24), 8 states have call predecessors, (24), 6 states have call successors, (24) Word has length 90
[2025-04-28 21:21:58,506 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,507 INFO  L225             Difference]: With dead ends: 99
[2025-04-28 21:21:58,507 INFO  L226             Difference]: Without dead ends: 99
[2025-04-28 21:21:58,508 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:58,508 INFO  L437           NwaCegarLoop]: 89 mSDtfsCounter, 1 mSDsluCounter, 507 mSDsCounter, 0 mSdLazyCounter, 75 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 596 SdHoareTripleChecker+Invalid, 76 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 75 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,509 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 596 Invalid, 76 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 75 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:58,510 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 99 states.
[2025-04-28 21:21:58,518 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 99 to 99.
[2025-04-28 21:21:58,518 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 99 states, 41 states have (on average 1.048780487804878) internal successors, (43), 43 states have internal predecessors, (43), 30 states have call successors, (32), 18 states have call predecessors, (32), 28 states have return successors, (58), 37 states have call predecessors, (58), 30 states have call successors, (58)
[2025-04-28 21:21:58,520 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 99 states to 99 states and 133 transitions.
[2025-04-28 21:21:58,520 INFO  L79                 Accepts]: Start accepts. Automaton has 99 states and 133 transitions. Word has length 90
[2025-04-28 21:21:58,520 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,520 INFO  L485      AbstractCegarLoop]: Abstraction has 99 states and 133 transitions.
[2025-04-28 21:21:58,521 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 4.714285714285714) internal successors, (33), 8 states have internal predecessors, (33), 6 states have call successors, (22), 1 states have call predecessors, (22), 7 states have return successors, (24), 8 states have call predecessors, (24), 6 states have call successors, (24)
[2025-04-28 21:21:58,521 INFO  L278                IsEmpty]: Start isEmpty. Operand 99 states and 133 transitions.
[2025-04-28 21:21:58,522 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 91
[2025-04-28 21:21:58,522 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,523 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:58,523 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:58,523 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,523 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,523 INFO  L85        PathProgramCache]: Analyzing trace with hash 776673117, now seen corresponding path program 1 times
[2025-04-28 21:21:58,523 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,524 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [115761047]
[2025-04-28 21:21:58,524 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,524 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,577 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-04-28 21:21:58,621 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-04-28 21:21:58,622 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,622 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,196 INFO  L134       CoverageAnalysis]: Checked inductivity of 28 backedges. 7 proven. 9 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:22:00,196 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,196 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [115761047]
[2025-04-28 21:22:00,196 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [115761047] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,196 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1356739492]
[2025-04-28 21:22:00,196 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,197 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,200 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,204 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:22:00,206 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,528 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 90 statements into 1 equivalence classes.
[2025-04-28 21:22:00,739 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 90 of 90 statements.
[2025-04-28 21:22:00,739 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,739 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,747 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1107 conjuncts, 82 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,758 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,793 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 0 select indices, 0 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 0 new quantified variables, introduced 0 case distinctions, treesize of input 8 treesize of output 1
[2025-04-28 21:22:01,527 INFO  L134       CoverageAnalysis]: Checked inductivity of 28 backedges. 8 proven. 6 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:01,527 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:07,323 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 24 treesize of output 22
[2025-04-28 21:22:07,638 INFO  L325             Elim1Store]: treesize reduction 0, result has 100.0 percent of original size
[2025-04-28 21:22:07,639 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 24 treesize of output 28
[2025-04-28 21:22:07,759 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 12 treesize of output 10
[2025-04-28 21:22:07,978 INFO  L134       CoverageAnalysis]: Checked inductivity of 28 backedges. 6 proven. 6 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:22:07,978 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1356739492] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:07,978 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:07,978 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 16, 16] total 30
[2025-04-28 21:22:07,978 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2042688662]
[2025-04-28 21:22:07,978 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,979 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-04-28 21:22:07,979 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,980 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-04-28 21:22:07,981 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=73, Invalid=797, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:22:07,981 INFO  L87              Difference]: Start difference. First operand 99 states and 133 transitions. Second operand  has 30 states, 15 states have (on average 3.933333333333333) internal successors, (59), 23 states have internal predecessors, (59), 21 states have call successors, (43), 2 states have call predecessors, (43), 15 states have return successors, (49), 22 states have call predecessors, (49), 21 states have call successors, (49)
[2025-04-28 21:22:08,985 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:08,985 INFO  L93              Difference]: Finished difference Result 125 states and 188 transitions.
[2025-04-28 21:22:08,986 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-04-28 21:22:08,986 INFO  L79                 Accepts]: Start accepts. Automaton has  has 30 states, 15 states have (on average 3.933333333333333) internal successors, (59), 23 states have internal predecessors, (59), 21 states have call successors, (43), 2 states have call predecessors, (43), 15 states have return successors, (49), 22 states have call predecessors, (49), 21 states have call successors, (49) Word has length 90
[2025-04-28 21:22:08,987 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,988 INFO  L225             Difference]: With dead ends: 125
[2025-04-28 21:22:08,988 INFO  L226             Difference]: Without dead ends: 125
[2025-04-28 21:22:08,989 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 209 GetRequests, 169 SyntacticMatches, 0 SemanticMatches, 40 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 101 ImplicationChecksByTransitivity, 1.2s TimeCoverageRelationStatistics Valid=155, Invalid=1567, Unknown=0, NotChecked=0, Total=1722
[2025-04-28 21:22:08,990 INFO  L437           NwaCegarLoop]: 80 mSDtfsCounter, 17 mSDsluCounter, 1581 mSDsCounter, 0 mSdLazyCounter, 518 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 1661 SdHoareTripleChecker+Invalid, 540 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 518 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,990 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 1661 Invalid, 540 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 518 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:08,991 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 125 states.
[2025-04-28 21:22:09,000 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 125 to 107.
[2025-04-28 21:22:09,001 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 107 states, 44 states have (on average 1.0454545454545454) internal successors, (46), 46 states have internal predecessors, (46), 32 states have call successors, (34), 18 states have call predecessors, (34), 31 states have return successors, (67), 43 states have call predecessors, (67), 32 states have call successors, (67)
[2025-04-28 21:22:09,002 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 107 states to 107 states and 147 transitions.
[2025-04-28 21:22:09,002 INFO  L79                 Accepts]: Start accepts. Automaton has 107 states and 147 transitions. Word has length 90
[2025-04-28 21:22:09,003 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:09,003 INFO  L485      AbstractCegarLoop]: Abstraction has 107 states and 147 transitions.
[2025-04-28 21:22:09,003 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 30 states, 15 states have (on average 3.933333333333333) internal successors, (59), 23 states have internal predecessors, (59), 21 states have call successors, (43), 2 states have call predecessors, (43), 15 states have return successors, (49), 22 states have call predecessors, (49), 21 states have call successors, (49)
[2025-04-28 21:22:09,003 INFO  L278                IsEmpty]: Start isEmpty. Operand 107 states and 147 transitions.
[2025-04-28 21:22:09,005 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 123
[2025-04-28 21:22:09,005 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:09,005 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:09,018 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:22:09,209 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:09,209 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,210 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,210 INFO  L85        PathProgramCache]: Analyzing trace with hash 1693375178, now seen corresponding path program 1 times
[2025-04-28 21:22:09,210 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,210 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1547807324]
[2025-04-28 21:22:09,210 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:09,210 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,253 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-04-28 21:22:09,274 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-04-28 21:22:09,274 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:09,274 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,710 INFO  L134       CoverageAnalysis]: Checked inductivity of 89 backedges. 24 proven. 2 refuted. 0 times theorem prover too weak. 63 trivial. 0 not checked.
[2025-04-28 21:22:09,711 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:09,711 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1547807324]
[2025-04-28 21:22:09,711 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1547807324] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:09,711 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1555148801]
[2025-04-28 21:22:09,711 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:09,711 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,714 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:09,716 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:09,719 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:22:10,084 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 122 statements into 1 equivalence classes.
[2025-04-28 21:22:10,336 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 122 of 122 statements.
[2025-04-28 21:22:10,336 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:10,336 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,343 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1541 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:10,349 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:10,475 INFO  L134       CoverageAnalysis]: Checked inductivity of 89 backedges. 41 proven. 0 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:22:10,475 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:10,475 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1555148801] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:10,475 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:10,475 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [10] total 16
[2025-04-28 21:22:10,476 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [128339200]
[2025-04-28 21:22:10,476 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:10,476 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:22:10,476 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:10,477 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:22:10,477 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=34, Invalid=206, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:22:10,477 INFO  L87              Difference]: Start difference. First operand 107 states and 147 transitions. Second operand  has 8 states, 7 states have (on average 5.571428571428571) internal successors, (39), 8 states have internal predecessors, (39), 6 states have call successors, (26), 2 states have call predecessors, (26), 7 states have return successors, (30), 8 states have call predecessors, (30), 6 states have call successors, (30)
[2025-04-28 21:22:10,565 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:10,565 INFO  L93              Difference]: Finished difference Result 53 states and 67 transitions.
[2025-04-28 21:22:10,565 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:10,566 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 5.571428571428571) internal successors, (39), 8 states have internal predecessors, (39), 6 states have call successors, (26), 2 states have call predecessors, (26), 7 states have return successors, (30), 8 states have call predecessors, (30), 6 states have call successors, (30) Word has length 122
[2025-04-28 21:22:10,566 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:10,566 INFO  L225             Difference]: With dead ends: 53
[2025-04-28 21:22:10,566 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:22:10,567 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 135 GetRequests, 121 SyntacticMatches, 0 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=34, Invalid=206, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:22:10,568 INFO  L437           NwaCegarLoop]: 58 mSDtfsCounter, 1 mSDsluCounter, 317 mSDsCounter, 0 mSdLazyCounter, 61 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 375 SdHoareTripleChecker+Invalid, 62 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 61 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:10,568 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 375 Invalid, 62 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 61 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:10,568 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:22:10,569 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:22:10,569 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:22:10,569 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:22:10,569 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 122
[2025-04-28 21:22:10,569 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:10,569 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:22:10,569 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 5.571428571428571) internal successors, (39), 8 states have internal predecessors, (39), 6 states have call successors, (26), 2 states have call predecessors, (26), 7 states have return successors, (30), 8 states have call predecessors, (30), 6 states have call successors, (30)
[2025-04-28 21:22:10,570 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:22:10,570 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:22:10,572 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:22:10,580 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:22:10,774 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:10,777 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:10,781 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:22:10,784 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:22:10 BoogieIcfgContainer
[2025-04-28 21:22:10,784 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:22:10,789 INFO  L158              Benchmark]: Toolchain (without parser) took 18531.61ms. Allocated memory was 234.9MB in the beginning and 453.0MB in the end (delta: 218.1MB). Free memory was 149.7MB in the beginning and 314.6MB in the end (delta: -165.0MB). Peak memory consumption was 63.1MB. Max. memory is 33.6GB.
[2025-04-28 21:22:10,789 INFO  L158              Benchmark]: SmtParser took 0.40ms. Allocated memory is still 234.9MB. Free memory is still 171.2MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:10,790 INFO  L158              Benchmark]: ChcToBoogie took 70.61ms. Allocated memory is still 234.9MB. Free memory was 149.7MB in the beginning and 147.6MB in the end (delta: 2.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:10,790 INFO  L158              Benchmark]: Boogie Preprocessor took 139.82ms. Allocated memory is still 234.9MB. Free memory was 147.6MB in the beginning and 144.2MB in the end (delta: 3.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:10,790 INFO  L158              Benchmark]: RCFGBuilder took 682.55ms. Allocated memory is still 234.9MB. Free memory was 144.2MB in the beginning and 115.4MB in the end (delta: 28.8MB). Peak memory consumption was 33.6MB. Max. memory is 33.6GB.
[2025-04-28 21:22:10,790 INFO  L158              Benchmark]: TraceAbstraction took 17630.21ms. Allocated memory was 234.9MB in the beginning and 453.0MB in the end (delta: 218.1MB). Free memory was 114.8MB in the beginning and 314.6MB in the end (delta: -199.9MB). Peak memory consumption was 29.5MB. Max. memory is 33.6GB.
[2025-04-28 21:22:10,793 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.40ms. Allocated memory is still 234.9MB. Free memory is still 171.2MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 70.61ms. Allocated memory is still 234.9MB. Free memory was 149.7MB in the beginning and 147.6MB in the end (delta: 2.0MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 139.82ms. Allocated memory is still 234.9MB. Free memory was 147.6MB in the beginning and 144.2MB in the end (delta: 3.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 682.55ms. Allocated memory is still 234.9MB. Free memory was 144.2MB in the beginning and 115.4MB in the end (delta: 28.8MB). Peak memory consumption was 33.6MB. Max. memory is 33.6GB.
 * TraceAbstraction took 17630.21ms. Allocated memory was 234.9MB in the beginning and 453.0MB in the end (delta: 218.1MB). Free memory was 114.8MB in the beginning and 314.6MB in the end (delta: -199.9MB). Peak memory consumption was 29.5MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 19 procedures, 79 locations, 126 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 17.6s, OverallIterations: 10, TraceHistogramMax: 5, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 2.3s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 40 SdHoareTripleChecker+Valid, 1.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 26 mSDsluCounter, 5731 SdHoareTripleChecker+Invalid, 1.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 4874 mSDsCounter, 25 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 968 IncrementalHoareTripleChecker+Invalid, 993 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 25 mSolverCounterUnsat, 857 mSDtfsCounter, 968 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 401 GetRequests, 312 SyntacticMatches, 0 SemanticMatches, 89 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 111 ImplicationChecksByTransitivity, 1.6s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=107occurred in iteration=9, InterpolantAutomatonStates: 80, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.2s AutomataMinimizationTime, 10 MinimizatonAttempts, 34 StatesRemovedByMinimization, 6 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.3s SsaConstructionTime, 0.9s SatisfiabilityAnalysisTime, 12.4s InterpolantComputationTime, 975 NumberOfCodeBlocks, 975 NumberOfCodeBlocksAsserted, 12 NumberOfCheckSat, 1052 ConstructedInterpolants, 0 QuantifiedInterpolants, 2122 SizeOfPredicates, 37 NumberOfNonLiveVariables, 2648 ConjunctsInSsa, 89 ConjunctsInUnsatCore, 13 InterpolantComputations, 9 PerfectInterpolantSequences, 323/346 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:22:10,809 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
sat
