./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/control_flow/branches_assert_condition_1.sol_1_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:26:03,308 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:26:03,346 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cf3c94bf-40ff-4ea3-8c9e-fd090a15dde7/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:26:03,349 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:26:03,349 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:26:03,362 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:26:03,363 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:26:03,363 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:26:03,363 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:26:03,363 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:26:03,363 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:26:03,363 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:26:03,363 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:26:03,363 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:26:03,363 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:26:03,364 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:26:03,364 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:26:03,364 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:26:03,364 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:03,364 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:26:03,364 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:26:03,364 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:26:03,364 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:26:03,364 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:26:03,364 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:26:03,365 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:26:03,365 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:26:03,549 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:26:03,554 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:26:03,556 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:26:03,557 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:26:03,557 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:26:03,558 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cf3c94bf-40ff-4ea3-8c9e-fd090a15dde7/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/control_flow/branches_assert_condition_1.sol_1_no_adts_000.smt2
[2025-05-07 17:26:03,559 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:26:03,561 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:26:03,745 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cf3c94bf-40ff-4ea3-8c9e-fd090a15dde7/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/control_flow/branches_assert_condition_1.sol_1_no_adts_000.smt2
[2025-05-07 17:26:03,747 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:26:03,748 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:26:03,749 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:26:03,749 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:26:03,749 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:26:03,751 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,777 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03 Unit
[2025-05-07 17:26:03,777 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:26:03,778 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:26:03,778 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:26:03,778 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:26:03,789 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,790 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,810 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,811 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,814 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,815 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,816 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,818 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,819 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,828 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:26:03,828 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:26:03,828 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:26:03,828 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:26:03,829 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (1/1) ...
[2025-05-07 17:26:03,831 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:26:03,839 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:03,848 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-05-07 17:26:03,850 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:26:03,860 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:26:03,860 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:26:03,860 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:26:03,860 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_5_0 given in one single declaration
[2025-05-07 17:26:03,860 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_5_0
[2025-05-07 17:26:03,860 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_5_0
[2025-05-07 17:26:03,860 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__24_25_0 given in one single declaration
[2025-05-07 17:26:03,860 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__24_25_0
[2025-05-07 17:26:03,861 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__24_25_0
[2025-05-07 17:26:03,861 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_function_f__24_25_0 given in one single declaration
[2025-05-07 17:26:03,861 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_function_f__24_25_0
[2025-05-07 17:26:03,861 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_function_f__24_25_0
[2025-05-07 17:26:03,861 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_f__24_25_0 given in one single declaration
[2025-05-07 17:26:03,861 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_f__24_25_0
[2025-05-07 17:26:03,861 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_f__24_25_0
[2025-05-07 17:26:03,861 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_if_true_f_14_25_0 given in one single declaration
[2025-05-07 17:26:03,861 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_if_true_f_14_25_0
[2025-05-07 17:26:03,861 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_if_true_f_14_25_0
[2025-05-07 17:26:03,861 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_if_header_f_22_25_0 given in one single declaration
[2025-05-07 17:26:03,861 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_if_header_f_22_25_0
[2025-05-07 17:26:03,862 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_if_header_f_22_25_0
[2025-05-07 17:26:03,862 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_6_f_23_25_0 given in one single declaration
[2025-05-07 17:26:03,862 INFO  L130     BoogieDeclarations]: Found specification of procedure block_6_f_23_25_0
[2025-05-07 17:26:03,862 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_6_f_23_25_0
[2025-05-07 17:26:03,862 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_5_function_f__24_25_0 given in one single declaration
[2025-05-07 17:26:03,862 INFO  L130     BoogieDeclarations]: Found specification of procedure block_5_function_f__24_25_0
[2025-05-07 17:26:03,862 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_5_function_f__24_25_0
[2025-05-07 17:26:03,862 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_return_function_f__24_25_0 given in one single declaration
[2025-05-07 17:26:03,862 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_return_function_f__24_25_0
[2025-05-07 17:26:03,862 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_return_function_f__24_25_0
[2025-05-07 17:26:03,862 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_f_23_25_0 given in one single declaration
[2025-05-07 17:26:03,862 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_f_23_25_0
[2025-05-07 17:26:03,862 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_f_23_25_0
[2025-05-07 17:26:03,862 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_if_false_f_21_25_0 given in one single declaration
[2025-05-07 17:26:03,862 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_if_false_f_21_25_0
[2025-05-07 17:26:03,863 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_if_false_f_21_25_0
[2025-05-07 17:26:03,863 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_function_f__24_25_0 given in one single declaration
[2025-05-07 17:26:03,863 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_function_f__24_25_0
[2025-05-07 17:26:03,863 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_function_f__24_25_0
[2025-05-07 17:26:03,863 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14_function_f__24_25_0 given in one single declaration
[2025-05-07 17:26:03,863 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14_function_f__24_25_0
[2025-05-07 17:26:03,863 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14_function_f__24_25_0
[2025-05-07 17:26:03,863 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_25_0 given in one single declaration
[2025-05-07 17:26:03,863 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_25_0
[2025-05-07 17:26:03,863 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_25_0
[2025-05-07 17:26:03,863 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_25_0 given in one single declaration
[2025-05-07 17:26:03,863 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_25_0
[2025-05-07 17:26:03,863 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_25_0
[2025-05-07 17:26:03,863 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_18_C_25_0 given in one single declaration
[2025-05-07 17:26:03,863 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_18_C_25_0
[2025-05-07 17:26:03,864 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_18_C_25_0
[2025-05-07 17:26:03,864 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_15_C_25_0 given in one single declaration
[2025-05-07 17:26:03,864 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_15_C_25_0
[2025-05-07 17:26:03,864 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_15_C_25_0
[2025-05-07 17:26:03,864 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_17_C_25_0 given in one single declaration
[2025-05-07 17:26:03,864 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_17_C_25_0
[2025-05-07 17:26:03,864 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_17_C_25_0
[2025-05-07 17:26:03,864 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_16_C_25_0 given in one single declaration
[2025-05-07 17:26:03,864 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_16_C_25_0
[2025-05-07 17:26:03,864 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_16_C_25_0
[2025-05-07 17:26:03,864 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:26:03,864 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:26:03,864 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:26:03,980 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:26:03,982 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:26:04,151 INFO  L?                        ?]: Removed 125 outVars from TransFormulas that were not future-live.
[2025-05-07 17:26:04,151 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:26:04,159 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:26:04,160 INFO  L312             CfgBuilder]: Removed 9 assume(true) statements.
[2025-05-07 17:26:04,160 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:04 BoogieIcfgContainer
[2025-05-07 17:26:04,160 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:26:04,162 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:26:04,162 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:26:04,165 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:26:04,165 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:26:03" (1/3) ...
[2025-05-07 17:26:04,165 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5ce87f3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:26:04, skipping insertion in model container
[2025-05-07 17:26:04,165 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:26:03" (2/3) ...
[2025-05-07 17:26:04,165 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5ce87f3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:26:04, skipping insertion in model container
[2025-05-07 17:26:04,165 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:26:04" (3/3) ...
[2025-05-07 17:26:04,166 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:26:04,177 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:26:04,179 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 21 procedures, 82 locations, 120 edges, 21 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:26:04,218 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:26:04,229 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;@37023d7a, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:26:04,229 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:26:04,232 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 82 states, 35 states have (on average 1.1142857142857143) internal successors, (39), 39 states have internal predecessors, (39), 25 states have call successors, (27), 20 states have call predecessors, (27), 20 states have return successors, (27), 22 states have call predecessors, (27), 25 states have call successors, (27)
[2025-05-07 17:26:04,241 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:26:04,241 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:04,241 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, 1]
[2025-05-07 17:26:04,242 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:04,246 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:04,246 INFO  L85        PathProgramCache]: Analyzing trace with hash -923356844, now seen corresponding path program 1 times
[2025-05-07 17:26:04,252 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:04,253 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [445281060]
[2025-05-07 17:26:04,253 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:04,253 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:04,306 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:26:04,392 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:26:04,393 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:04,393 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:04,569 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:26:04,570 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:04,570 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [445281060]
[2025-05-07 17:26:04,570 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [445281060] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:04,570 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:04,572 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:26:04,573 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1167531237]
[2025-05-07 17:26:04,574 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:04,576 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:04,577 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:04,603 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:04,604 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:04,605 INFO  L87              Difference]: Start difference. First operand  has 82 states, 35 states have (on average 1.1142857142857143) internal successors, (39), 39 states have internal predecessors, (39), 25 states have call successors, (27), 20 states have call predecessors, (27), 20 states have return successors, (27), 22 states have call predecessors, (27), 25 states have call successors, (27) Second operand  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:26:04,677 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:04,677 INFO  L93              Difference]: Finished difference Result 84 states and 95 transitions.
[2025-05-07 17:26:04,679 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:04,680 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16) Word has length 59
[2025-05-07 17:26:04,681 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:04,688 INFO  L225             Difference]: With dead ends: 84
[2025-05-07 17:26:04,689 INFO  L226             Difference]: Without dead ends: 84
[2025-05-07 17:26:04,690 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-05-07 17:26:04,693 INFO  L437           NwaCegarLoop]: 89 mSDtfsCounter, 1 mSDsluCounter, 346 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 435 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:04,694 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 435 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:04,708 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 84 states.
[2025-05-07 17:26:04,731 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 84 to 84.
[2025-05-07 17:26:04,732 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 36 states have (on average 1.0833333333333333) internal successors, (39), 39 states have internal predecessors, (39), 25 states have call successors, (27), 20 states have call predecessors, (27), 22 states have return successors, (29), 24 states have call predecessors, (29), 25 states have call successors, (29)
[2025-05-07 17:26:04,736 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 95 transitions.
[2025-05-07 17:26:04,737 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 95 transitions. Word has length 59
[2025-05-07 17:26:04,738 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:04,738 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 95 transitions.
[2025-05-07 17:26:04,738 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.4) internal successors, (27), 6 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16)
[2025-05-07 17:26:04,738 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 95 transitions.
[2025-05-07 17:26:04,742 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:26:04,742 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:04,742 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, 1]
[2025-05-07 17:26:04,742 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:26:04,742 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:04,743 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:04,743 INFO  L85        PathProgramCache]: Analyzing trace with hash -679755810, now seen corresponding path program 1 times
[2025-05-07 17:26:04,743 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:04,743 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1173770135]
[2025-05-07 17:26:04,743 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:04,743 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:04,775 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:26:04,782 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:26:04,782 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:04,782 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:04,866 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:26:04,866 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:04,866 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1173770135]
[2025-05-07 17:26:04,866 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1173770135] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:04,866 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:04,866 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:04,866 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1416894291]
[2025-05-07 17:26:04,867 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:04,868 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:04,868 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:04,868 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:04,868 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:04,869 INFO  L87              Difference]: Start difference. First operand 84 states and 95 transitions. Second operand  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:26:04,881 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:04,881 INFO  L93              Difference]: Finished difference Result 88 states and 99 transitions.
[2025-05-07 17:26:04,882 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:04,882 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16) Word has length 59
[2025-05-07 17:26:04,882 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:04,883 INFO  L225             Difference]: With dead ends: 88
[2025-05-07 17:26:04,883 INFO  L226             Difference]: Without dead ends: 84
[2025-05-07 17:26:04,884 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-05-07 17:26:04,884 INFO  L437           NwaCegarLoop]: 91 mSDtfsCounter, 1 mSDsluCounter, 175 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 266 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-05-07 17:26:04,885 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 266 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:04,885 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 84 states.
[2025-05-07 17:26:04,891 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 84 to 82.
[2025-05-07 17:26:04,891 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 36 states have (on average 1.0555555555555556) internal successors, (38), 38 states have internal predecessors, (38), 23 states have call successors, (25), 20 states have call predecessors, (25), 22 states have return successors, (27), 23 states have call predecessors, (27), 23 states have call successors, (27)
[2025-05-07 17:26:04,893 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 90 transitions.
[2025-05-07 17:26:04,893 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 90 transitions. Word has length 59
[2025-05-07 17:26:04,893 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:04,893 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 90 transitions.
[2025-05-07 17:26:04,893 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:26:04,894 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 90 transitions.
[2025-05-07 17:26:04,895 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-05-07 17:26:04,895 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:04,895 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, 1]
[2025-05-07 17:26:04,895 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:26:04,895 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:04,896 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:04,896 INFO  L85        PathProgramCache]: Analyzing trace with hash 344990682, now seen corresponding path program 1 times
[2025-05-07 17:26:04,896 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:04,896 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [714910272]
[2025-05-07 17:26:04,896 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:04,896 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:04,922 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-05-07 17:26:04,941 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-05-07 17:26:04,942 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:04,942 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:05,115 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:26:05,115 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:05,115 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [714910272]
[2025-05-07 17:26:05,115 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [714910272] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:05,116 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:05,116 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:05,116 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1287380261]
[2025-05-07 17:26:05,116 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:05,116 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:05,116 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:05,117 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:05,117 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:05,117 INFO  L87              Difference]: Start difference. First operand 82 states and 90 transitions. Second operand  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 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-05-07 17:26:05,134 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:05,134 INFO  L93              Difference]: Finished difference Result 80 states and 87 transitions.
[2025-05-07 17:26:05,135 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:05,135 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 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 59
[2025-05-07 17:26:05,135 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:05,136 INFO  L225             Difference]: With dead ends: 80
[2025-05-07 17:26:05,136 INFO  L226             Difference]: Without dead ends: 78
[2025-05-07 17:26:05,136 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-05-07 17:26:05,137 INFO  L437           NwaCegarLoop]: 82 mSDtfsCounter, 0 mSDsluCounter, 157 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 239 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:05,137 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 239 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:26:05,137 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 78 states.
[2025-05-07 17:26:05,140 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 78 to 78.
[2025-05-07 17:26:05,141 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 34 states have (on average 1.0588235294117647) internal successors, (36), 36 states have internal predecessors, (36), 22 states have call successors, (23), 19 states have call predecessors, (23), 21 states have return successors, (25), 22 states have call predecessors, (25), 22 states have call successors, (25)
[2025-05-07 17:26:05,141 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 84 transitions.
[2025-05-07 17:26:05,141 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 84 transitions. Word has length 59
[2025-05-07 17:26:05,142 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:05,142 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 84 transitions.
[2025-05-07 17:26:05,142 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 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-05-07 17:26:05,142 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 84 transitions.
[2025-05-07 17:26:05,143 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 63
[2025-05-07 17:26:05,143 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:05,143 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, 1, 1, 1, 1]
[2025-05-07 17:26:05,143 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:26:05,143 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:05,143 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:05,143 INFO  L85        PathProgramCache]: Analyzing trace with hash -547910967, now seen corresponding path program 1 times
[2025-05-07 17:26:05,144 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:05,144 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1224078546]
[2025-05-07 17:26:05,144 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:05,144 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:05,167 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 62 statements into 1 equivalence classes.
[2025-05-07 17:26:05,179 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 62 of 62 statements.
[2025-05-07 17:26:05,179 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:05,179 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:05,381 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:26:05,381 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:05,382 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1224078546]
[2025-05-07 17:26:05,382 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1224078546] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:05,382 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:05,382 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-05-07 17:26:05,382 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [164107267]
[2025-05-07 17:26:05,382 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:05,382 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-05-07 17:26:05,382 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:05,383 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-05-07 17:26:05,383 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:26:05,383 INFO  L87              Difference]: Start difference. First operand 78 states and 84 transitions. Second operand  has 11 states, 9 states have (on average 3.111111111111111) internal successors, (28), 11 states have internal predecessors, (28), 4 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 10 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:26:05,525 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:05,525 INFO  L93              Difference]: Finished difference Result 86 states and 92 transitions.
[2025-05-07 17:26:05,525 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-05-07 17:26:05,525 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 9 states have (on average 3.111111111111111) internal successors, (28), 11 states have internal predecessors, (28), 4 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 10 states have call predecessors, (17), 4 states have call successors, (17) Word has length 62
[2025-05-07 17:26:05,526 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:05,526 INFO  L225             Difference]: With dead ends: 86
[2025-05-07 17:26:05,526 INFO  L226             Difference]: Without dead ends: 86
[2025-05-07 17:26:05,526 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=109, Unknown=0, NotChecked=0, Total=132
[2025-05-07 17:26:05,527 INFO  L437           NwaCegarLoop]: 75 mSDtfsCounter, 3 mSDsluCounter, 647 mSDsCounter, 0 mSdLazyCounter, 98 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 722 SdHoareTripleChecker+Invalid, 99 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 98 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:05,527 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 722 Invalid, 99 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 98 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:26:05,528 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 86 states.
[2025-05-07 17:26:05,530 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 86 to 82.
[2025-05-07 17:26:05,531 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 36 states have (on average 1.0555555555555556) internal successors, (38), 38 states have internal predecessors, (38), 22 states have call successors, (23), 19 states have call predecessors, (23), 23 states have return successors, (27), 24 states have call predecessors, (27), 22 states have call successors, (27)
[2025-05-07 17:26:05,531 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 88 transitions.
[2025-05-07 17:26:05,531 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 88 transitions. Word has length 62
[2025-05-07 17:26:05,531 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:05,531 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 88 transitions.
[2025-05-07 17:26:05,532 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 9 states have (on average 3.111111111111111) internal successors, (28), 11 states have internal predecessors, (28), 4 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 10 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:26:05,532 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 88 transitions.
[2025-05-07 17:26:05,532 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 63
[2025-05-07 17:26:05,532 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:05,532 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, 1, 1, 1, 1]
[2025-05-07 17:26:05,532 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:26:05,533 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:05,533 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:05,533 INFO  L85        PathProgramCache]: Analyzing trace with hash 1095018076, now seen corresponding path program 1 times
[2025-05-07 17:26:05,533 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:05,533 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1085419800]
[2025-05-07 17:26:05,533 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:05,533 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:05,553 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 62 statements into 1 equivalence classes.
[2025-05-07 17:26:05,565 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 62 of 62 statements.
[2025-05-07 17:26:05,565 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:05,565 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:05,700 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:26:05,700 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:05,701 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1085419800]
[2025-05-07 17:26:05,701 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1085419800] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:05,701 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:05,701 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-05-07 17:26:05,701 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1915441025]
[2025-05-07 17:26:05,701 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:05,701 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-05-07 17:26:05,701 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:05,702 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-05-07 17:26:05,702 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:26:05,702 INFO  L87              Difference]: Start difference. First operand 82 states and 88 transitions. Second operand  has 11 states, 9 states have (on average 3.111111111111111) internal successors, (28), 11 states have internal predecessors, (28), 4 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 10 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:26:05,821 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:05,821 INFO  L93              Difference]: Finished difference Result 76 states and 82 transitions.
[2025-05-07 17:26:05,821 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-05-07 17:26:05,821 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 9 states have (on average 3.111111111111111) internal successors, (28), 11 states have internal predecessors, (28), 4 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 10 states have call predecessors, (17), 4 states have call successors, (17) Word has length 62
[2025-05-07 17:26:05,822 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:05,822 INFO  L225             Difference]: With dead ends: 76
[2025-05-07 17:26:05,822 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:26:05,822 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=109, Unknown=0, NotChecked=0, Total=132
[2025-05-07 17:26:05,823 INFO  L437           NwaCegarLoop]: 73 mSDtfsCounter, 1 mSDsluCounter, 628 mSDsCounter, 0 mSdLazyCounter, 96 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 701 SdHoareTripleChecker+Invalid, 97 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 96 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:05,823 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 701 Invalid, 97 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 96 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:26:05,824 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:26:05,824 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:26:05,824 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-05-07 17:26:05,824 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:26:05,824 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 62
[2025-05-07 17:26:05,824 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:05,824 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:26:05,824 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 9 states have (on average 3.111111111111111) internal successors, (28), 11 states have internal predecessors, (28), 4 states have call successors, (17), 1 states have call predecessors, (17), 9 states have return successors, (17), 10 states have call predecessors, (17), 4 states have call successors, (17)
[2025-05-07 17:26:05,825 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:26:05,825 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:26:05,827 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:26:05,827 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:26:05,829 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1]
[2025-05-07 17:26:05,831 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:26:05,833 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:26:05 BoogieIcfgContainer
[2025-05-07 17:26:05,833 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:26:05,834 INFO  L158              Benchmark]: Toolchain (without parser) took 2085.87ms. Allocated memory is still 234.9MB. Free memory was 156.9MB in the beginning and 88.2MB in the end (delta: 68.7MB). Peak memory consumption was 78.0MB. Max. memory is 33.6GB.
[2025-05-07 17:26:05,834 INFO  L158              Benchmark]: SmtParser took 0.24ms. Allocated memory is still 234.9MB. Free memory is still 174.5MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:05,834 INFO  L158              Benchmark]: ChcToBoogie took 28.93ms. Allocated memory is still 234.9MB. Free memory was 156.8MB in the beginning and 154.6MB in the end (delta: 2.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:26:05,834 INFO  L158              Benchmark]: Boogie Preprocessor took 49.90ms. Allocated memory is still 234.9MB. Free memory was 154.5MB in the beginning and 151.6MB in the end (delta: 2.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:26:05,834 INFO  L158              Benchmark]: RCFGBuilder took 331.89ms. Allocated memory is still 234.9MB. Free memory was 151.5MB in the beginning and 123.9MB in the end (delta: 27.6MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:26:05,835 INFO  L158              Benchmark]: TraceAbstraction took 1671.47ms. Allocated memory is still 234.9MB. Free memory was 123.4MB in the beginning and 88.2MB in the end (delta: 35.2MB). Peak memory consumption was 44.5MB. Max. memory is 33.6GB.
[2025-05-07 17:26:05,835 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.24ms. Allocated memory is still 234.9MB. Free memory is still 174.5MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 28.93ms. Allocated memory is still 234.9MB. Free memory was 156.8MB in the beginning and 154.6MB in the end (delta: 2.2MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 49.90ms. Allocated memory is still 234.9MB. Free memory was 154.5MB in the beginning and 151.6MB in the end (delta: 2.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 331.89ms. Allocated memory is still 234.9MB. Free memory was 151.5MB in the beginning and 123.9MB in the end (delta: 27.6MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 1671.47ms. Allocated memory is still 234.9MB. Free memory was 123.4MB in the beginning and 88.2MB in the end (delta: 35.2MB). Peak memory consumption was 44.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 21 procedures, 82 locations, 120 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 1.6s, OverallIterations: 5, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.4s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 13 SdHoareTripleChecker+Valid, 0.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 6 mSDsluCounter, 2363 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 1953 mSDsCounter, 2 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 219 IncrementalHoareTripleChecker+Invalid, 221 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 2 mSolverCounterUnsat, 410 mSDtfsCounter, 219 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 38 GetRequests, 10 SyntacticMatches, 0 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=84occurred in iteration=1, InterpolantAutomatonStates: 36, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.0s AutomataMinimizationTime, 5 MinimizatonAttempts, 6 StatesRemovedByMinimization, 2 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 0.8s InterpolantComputationTime, 301 NumberOfCodeBlocks, 301 NumberOfCodeBlocksAsserted, 5 NumberOfCheckSat, 296 ConstructedInterpolants, 0 QuantifiedInterpolants, 404 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 5 InterpolantComputations, 5 PerfectInterpolantSequences, 0/0 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-05-07 17:26:05,846 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
