./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/blockchain_state/balance_receive.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:27:58,937 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:27:58,973 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_de81a05b-e6a7-424d-ab8b-85fab2286f03/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:27:58,976 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:27:58,977 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:27:58,989 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:27:58,990 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:27:58,990 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:27:58,990 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:27:58,990 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:27:58,990 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:27:58,991 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:27:58,991 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:58,991 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:27:58,991 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:27:58,992 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:27:58,992 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:27:59,169 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:27:59,175 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:27:59,177 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:27:59,178 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:27:59,178 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:27:59,179 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_de81a05b-e6a7-424d-ab8b-85fab2286f03/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/blockchain_state/balance_receive.sol_0_no_adts_000.smt2
[2025-05-07 17:27:59,180 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:27:59,182 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:27:59,418 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_de81a05b-e6a7-424d-ab8b-85fab2286f03/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/blockchain_state/balance_receive.sol_0_no_adts_000.smt2
[2025-05-07 17:27:59,421 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:27:59,423 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:27:59,423 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:27:59,423 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:27:59,424 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:27:59,426 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,466 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59 Unit
[2025-05-07 17:27:59,466 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:27:59,467 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:27:59,467 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:27:59,467 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:27:59,483 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,483 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,508 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,508 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,512 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,513 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,515 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,517 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,518 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,528 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:27:59,528 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:27:59,528 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:27:59,528 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:27:59,529 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (1/1) ...
[2025-05-07 17:27:59,531 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:27:59,539 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:59,548 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:27:59,551 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:27:59,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:27:59,559 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:27:59,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:27:59,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_7_0 given in one single declaration
[2025-05-07 17:27:59,559 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_7_0
[2025-05-07 17:27:59,559 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_7_0
[2025-05-07 17:27:59,559 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_5_function_f__65_66_0 given in one single declaration
[2025-05-07 17:27:59,560 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_5_function_f__65_66_0
[2025-05-07 17:27:59,560 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_5_function_f__65_66_0
[2025-05-07 17:27:59,560 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_4_function_f__65_66_0 given in one single declaration
[2025-05-07 17:27:59,560 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_4_function_f__65_66_0
[2025-05-07 17:27:59,560 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_4_function_f__65_66_0
[2025-05-07 17:27:59,560 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_9_function_f__65_66_0 given in one single declaration
[2025-05-07 17:27:59,560 INFO  L130     BoogieDeclarations]: Found specification of procedure block_9_function_f__65_66_0
[2025-05-07 17:27:59,560 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_9_function_f__65_66_0
[2025-05-07 17:27:59,560 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_7_f_64_66_0 given in one single declaration
[2025-05-07 17:27:59,560 INFO  L130     BoogieDeclarations]: Found specification of procedure block_7_f_64_66_0
[2025-05-07 17:27:59,560 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_7_f_64_66_0
[2025-05-07 17:27:59,560 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_6_function_f__65_66_0 given in one single declaration
[2025-05-07 17:27:59,561 INFO  L130     BoogieDeclarations]: Found specification of procedure block_6_function_f__65_66_0
[2025-05-07 17:27:59,561 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_6_function_f__65_66_0
[2025-05-07 17:27:59,561 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_8_return_function_f__65_66_0 given in one single declaration
[2025-05-07 17:27:59,561 INFO  L130     BoogieDeclarations]: Found specification of procedure block_8_return_function_f__65_66_0
[2025-05-07 17:27:59,561 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_8_return_function_f__65_66_0
[2025-05-07 17:27:59,561 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_11_function_f__65_66_0 given in one single declaration
[2025-05-07 17:27:59,561 INFO  L130     BoogieDeclarations]: Found specification of procedure block_11_function_f__65_66_0
[2025-05-07 17:27:59,561 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_11_function_f__65_66_0
[2025-05-07 17:27:59,561 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_10_function_f__65_66_0 given in one single declaration
[2025-05-07 17:27:59,561 INFO  L130     BoogieDeclarations]: Found specification of procedure block_10_function_f__65_66_0
[2025-05-07 17:27:59,561 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_10_function_f__65_66_0
[2025-05-07 17:27:59,562 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_12_function_f__65_66_0 given in one single declaration
[2025-05-07 17:27:59,562 INFO  L130     BoogieDeclarations]: Found specification of procedure block_12_function_f__65_66_0
[2025-05-07 17:27:59,562 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_12_function_f__65_66_0
[2025-05-07 17:27:59,562 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure interface_0_C_66_0 given in one single declaration
[2025-05-07 17:27:59,562 INFO  L130     BoogieDeclarations]: Found specification of procedure interface_0_C_66_0
[2025-05-07 17:27:59,562 INFO  L138     BoogieDeclarations]: Found implementation of procedure interface_0_C_66_0
[2025-05-07 17:27:59,562 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_2_C_66_0 given in one single declaration
[2025-05-07 17:27:59,562 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_2_C_66_0
[2025-05-07 17:27:59,562 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_2_C_66_0
[2025-05-07 17:27:59,562 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_19_C_66_0 given in one single declaration
[2025-05-07 17:27:59,563 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_19_C_66_0
[2025-05-07 17:27:59,563 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_19_C_66_0
[2025-05-07 17:27:59,563 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_16_C_66_0 given in one single declaration
[2025-05-07 17:27:59,563 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_16_C_66_0
[2025-05-07 17:27:59,563 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_16_C_66_0
[2025-05-07 17:27:59,563 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_18_C_66_0 given in one single declaration
[2025-05-07 17:27:59,563 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_18_C_66_0
[2025-05-07 17:27:59,563 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_18_C_66_0
[2025-05-07 17:27:59,563 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_17_C_66_0 given in one single declaration
[2025-05-07 17:27:59,563 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_17_C_66_0
[2025-05-07 17:27:59,563 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_17_C_66_0
[2025-05-07 17:27:59,563 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_3_constructor_14_66_0 given in one single declaration
[2025-05-07 17:27:59,564 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_3_constructor_14_66_0
[2025-05-07 17:27:59,564 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_3_constructor_14_66_0
[2025-05-07 17:27:59,564 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_15_return_constructor_14_66_0 given in one single declaration
[2025-05-07 17:27:59,564 INFO  L130     BoogieDeclarations]: Found specification of procedure block_15_return_constructor_14_66_0
[2025-05-07 17:27:59,564 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_15_return_constructor_14_66_0
[2025-05-07 17:27:59,564 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_14__13_66_0 given in one single declaration
[2025-05-07 17:27:59,564 INFO  L130     BoogieDeclarations]: Found specification of procedure block_14__13_66_0
[2025-05-07 17:27:59,564 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_14__13_66_0
[2025-05-07 17:27:59,564 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_13_constructor_14_66_0 given in one single declaration
[2025-05-07 17:27:59,564 INFO  L130     BoogieDeclarations]: Found specification of procedure block_13_constructor_14_66_0
[2025-05-07 17:27:59,564 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_13_constructor_14_66_0
[2025-05-07 17:27:59,564 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:27:59,565 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:27:59,565 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:27:59,688 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:27:59,691 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:27:59,916 INFO  L?                        ?]: Removed 210 outVars from TransFormulas that were not future-live.
[2025-05-07 17:27:59,916 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:27:59,926 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:27:59,926 INFO  L312             CfgBuilder]: Removed 10 assume(true) statements.
[2025-05-07 17:27:59,927 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:59 BoogieIcfgContainer
[2025-05-07 17:27:59,927 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:27:59,929 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:27:59,929 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:27:59,931 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:27:59,931 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:27:59" (1/3) ...
[2025-05-07 17:27:59,932 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@e49162e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:27:59, skipping insertion in model container
[2025-05-07 17:27:59,932 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:27:59" (2/3) ...
[2025-05-07 17:27:59,932 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@e49162e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:27:59, skipping insertion in model container
[2025-05-07 17:27:59,932 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:27:59" (3/3) ...
[2025-05-07 17:27:59,933 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:27:59,943 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:27:59,945 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 22 procedures, 87 locations, 131 edges, 22 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:27:59,980 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:27:59,992 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;@61bf1921, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:27:59,992 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:27:59,995 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 87 states, 37 states have (on average 1.1081081081081081) internal successors, (41), 41 states have internal predecessors, (41), 27 states have call successors, (30), 21 states have call predecessors, (30), 21 states have return successors, (30), 24 states have call predecessors, (30), 27 states have call successors, (30)
[2025-05-07 17:28:00,003 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:28:00,003 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,004 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, 1, 1, 1, 1]
[2025-05-07 17:28:00,004 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,008 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,008 INFO  L85        PathProgramCache]: Analyzing trace with hash 189296433, now seen corresponding path program 1 times
[2025-05-07 17:28:00,013 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,014 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2059237621]
[2025-05-07 17:28:00,014 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,014 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,066 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:28:00,107 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:28:00,107 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,108 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:00,284 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:28:00,284 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:00,284 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2059237621]
[2025-05-07 17:28:00,285 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2059237621] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:00,285 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:00,287 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:00,288 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1208440664]
[2025-05-07 17:28:00,288 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:00,291 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:00,291 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:00,319 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:00,319 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:00,321 INFO  L87              Difference]: Start difference. First operand  has 87 states, 37 states have (on average 1.1081081081081081) internal successors, (41), 41 states have internal predecessors, (41), 27 states have call successors, (30), 21 states have call predecessors, (30), 21 states have return successors, (30), 24 states have call predecessors, (30), 27 states have call successors, (30) Second operand  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:00,385 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,385 INFO  L93              Difference]: Finished difference Result 89 states and 103 transitions.
[2025-05-07 17:28:00,387 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:00,388 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18) Word has length 66
[2025-05-07 17:28:00,388 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,393 INFO  L225             Difference]: With dead ends: 89
[2025-05-07 17:28:00,394 INFO  L226             Difference]: Without dead ends: 89
[2025-05-07 17:28:00,395 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:28:00,397 INFO  L437           NwaCegarLoop]: 97 mSDtfsCounter, 1 mSDsluCounter, 183 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 280 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:00,398 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 280 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:00,408 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 89 states.
[2025-05-07 17:28:00,424 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 89 to 87.
[2025-05-07 17:28:00,425 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 87 states, 37 states have (on average 1.0810810810810811) internal successors, (40), 40 states have internal predecessors, (40), 27 states have call successors, (30), 21 states have call predecessors, (30), 22 states have return successors, (31), 25 states have call predecessors, (31), 27 states have call successors, (31)
[2025-05-07 17:28:00,429 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 87 states to 87 states and 101 transitions.
[2025-05-07 17:28:00,429 INFO  L79                 Accepts]: Start accepts. Automaton has 87 states and 101 transitions. Word has length 66
[2025-05-07 17:28:00,430 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,430 INFO  L485      AbstractCegarLoop]: Abstraction has 87 states and 101 transitions.
[2025-05-07 17:28:00,430 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:00,430 INFO  L278                IsEmpty]: Start isEmpty. Operand 87 states and 101 transitions.
[2025-05-07 17:28:00,432 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:28:00,432 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,432 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, 1, 1, 1, 1]
[2025-05-07 17:28:00,432 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:28:00,432 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,433 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,433 INFO  L85        PathProgramCache]: Analyzing trace with hash 51326777, now seen corresponding path program 1 times
[2025-05-07 17:28:00,433 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,433 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [280397879]
[2025-05-07 17:28:00,433 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,433 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,472 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:28:00,477 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:28:00,477 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,477 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:00,571 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:28:00,572 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:00,572 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [280397879]
[2025-05-07 17:28:00,572 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [280397879] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:00,572 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:00,572 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:28:00,572 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [712180656]
[2025-05-07 17:28:00,572 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:00,573 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:28:00,573 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:00,574 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:28:00,574 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:28:00,575 INFO  L87              Difference]: Start difference. First operand 87 states and 101 transitions. Second operand  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:00,587 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:00,587 INFO  L93              Difference]: Finished difference Result 89 states and 102 transitions.
[2025-05-07 17:28:00,587 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:28:00,588 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18) Word has length 66
[2025-05-07 17:28:00,588 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:00,588 INFO  L225             Difference]: With dead ends: 89
[2025-05-07 17:28:00,589 INFO  L226             Difference]: Without dead ends: 81
[2025-05-07 17:28:00,589 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:28:00,589 INFO  L437           NwaCegarLoop]: 99 mSDtfsCounter, 1 mSDsluCounter, 187 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 286 SdHoareTripleChecker+Invalid, 3 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:00,589 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 286 Invalid, 3 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:00,590 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 81 states.
[2025-05-07 17:28:00,594 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 81 to 81.
[2025-05-07 17:28:00,594 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 81 states, 36 states have (on average 1.0277777777777777) internal successors, (37), 37 states have internal predecessors, (37), 23 states have call successors, (26), 21 states have call predecessors, (26), 21 states have return successors, (26), 22 states have call predecessors, (26), 23 states have call successors, (26)
[2025-05-07 17:28:00,595 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 81 states to 81 states and 89 transitions.
[2025-05-07 17:28:00,595 INFO  L79                 Accepts]: Start accepts. Automaton has 81 states and 89 transitions. Word has length 66
[2025-05-07 17:28:00,595 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:00,595 INFO  L485      AbstractCegarLoop]: Abstraction has 81 states and 89 transitions.
[2025-05-07 17:28:00,595 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 10.0) internal successors, (30), 4 states have internal predecessors, (30), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:28:00,595 INFO  L278                IsEmpty]: Start isEmpty. Operand 81 states and 89 transitions.
[2025-05-07 17:28:00,596 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:28:00,596 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:00,596 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, 1, 1, 1, 1]
[2025-05-07 17:28:00,596 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:28:00,596 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:00,597 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:00,597 INFO  L85        PathProgramCache]: Analyzing trace with hash 57784089, now seen corresponding path program 1 times
[2025-05-07 17:28:00,597 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:00,597 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1846302730]
[2025-05-07 17:28:00,597 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:00,597 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:00,627 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:28:00,661 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:28:00,661 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:00,661 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:01,756 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:28:01,757 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:01,757 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1846302730]
[2025-05-07 17:28:01,757 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1846302730] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:01,757 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:01,757 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [15] imperfect sequences [] total 15
[2025-05-07 17:28:01,757 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1379615312]
[2025-05-07 17:28:01,757 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:01,757 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-05-07 17:28:01,757 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:01,758 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-05-07 17:28:01,758 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=182, Unknown=0, NotChecked=0, Total=210
[2025-05-07 17:28:01,758 INFO  L87              Difference]: Start difference. First operand 81 states and 89 transitions. Second operand  has 15 states, 11 states have (on average 2.727272727272727) internal successors, (30), 13 states have internal predecessors, (30), 9 states have call successors, (18), 1 states have call predecessors, (18), 11 states have return successors, (18), 13 states have call predecessors, (18), 9 states have call successors, (18)
[2025-05-07 17:28:02,064 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:02,065 INFO  L93              Difference]: Finished difference Result 90 states and 101 transitions.
[2025-05-07 17:28:02,065 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-05-07 17:28:02,065 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 11 states have (on average 2.727272727272727) internal successors, (30), 13 states have internal predecessors, (30), 9 states have call successors, (18), 1 states have call predecessors, (18), 11 states have return successors, (18), 13 states have call predecessors, (18), 9 states have call successors, (18) Word has length 66
[2025-05-07 17:28:02,065 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:02,066 INFO  L225             Difference]: With dead ends: 90
[2025-05-07 17:28:02,066 INFO  L226             Difference]: Without dead ends: 90
[2025-05-07 17:28:02,066 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 17 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 6 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=37, Invalid=235, Unknown=0, NotChecked=0, Total=272
[2025-05-07 17:28:02,067 INFO  L437           NwaCegarLoop]: 78 mSDtfsCounter, 3 mSDsluCounter, 966 mSDsCounter, 0 mSdLazyCounter, 221 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 1044 SdHoareTripleChecker+Invalid, 221 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 221 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:02,067 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 1044 Invalid, 221 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 221 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-05-07 17:28:02,068 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-05-07 17:28:02,072 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 88.
[2025-05-07 17:28:02,073 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 88 states, 39 states have (on average 1.0256410256410255) internal successors, (40), 40 states have internal predecessors, (40), 24 states have call successors, (27), 21 states have call predecessors, (27), 24 states have return successors, (32), 26 states have call predecessors, (32), 24 states have call successors, (32)
[2025-05-07 17:28:02,074 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 88 states to 88 states and 99 transitions.
[2025-05-07 17:28:02,074 INFO  L79                 Accepts]: Start accepts. Automaton has 88 states and 99 transitions. Word has length 66
[2025-05-07 17:28:02,074 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:02,074 INFO  L485      AbstractCegarLoop]: Abstraction has 88 states and 99 transitions.
[2025-05-07 17:28:02,074 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 11 states have (on average 2.727272727272727) internal successors, (30), 13 states have internal predecessors, (30), 9 states have call successors, (18), 1 states have call predecessors, (18), 11 states have return successors, (18), 13 states have call predecessors, (18), 9 states have call successors, (18)
[2025-05-07 17:28:02,075 INFO  L278                IsEmpty]: Start isEmpty. Operand 88 states and 99 transitions.
[2025-05-07 17:28:02,076 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:28:02,076 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:02,076 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, 1, 1, 1, 1]
[2025-05-07 17:28:02,076 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:28:02,076 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:02,076 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:02,076 INFO  L85        PathProgramCache]: Analyzing trace with hash -995910091, now seen corresponding path program 1 times
[2025-05-07 17:28:02,076 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:02,077 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2045866271]
[2025-05-07 17:28:02,077 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:02,077 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:02,097 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:28:02,108 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:28:02,109 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:02,109 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:02,427 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:28:02,427 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:02,428 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2045866271]
[2025-05-07 17:28:02,428 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2045866271] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:02,428 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:02,428 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [12] imperfect sequences [] total 12
[2025-05-07 17:28:02,428 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1447572181]
[2025-05-07 17:28:02,428 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:02,428 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-05-07 17:28:02,428 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:02,429 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-05-07 17:28:02,429 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=111, Unknown=0, NotChecked=0, Total=132
[2025-05-07 17:28:02,430 INFO  L87              Difference]: Start difference. First operand 88 states and 99 transitions. Second operand  has 12 states, 10 states have (on average 3.0) internal successors, (30), 12 states have internal predecessors, (30), 5 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 9 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:28:02,554 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:02,554 INFO  L93              Difference]: Finished difference Result 92 states and 103 transitions.
[2025-05-07 17:28:02,555 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-05-07 17:28:02,555 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 10 states have (on average 3.0) internal successors, (30), 12 states have internal predecessors, (30), 5 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 9 states have call predecessors, (18), 5 states have call successors, (18) Word has length 66
[2025-05-07 17:28:02,556 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:02,556 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:28:02,556 INFO  L226             Difference]: Without dead ends: 92
[2025-05-07 17:28:02,557 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 20 GetRequests, 9 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=25, Invalid=131, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:28:02,557 INFO  L437           NwaCegarLoop]: 81 mSDtfsCounter, 2 mSDsluCounter, 776 mSDsCounter, 0 mSdLazyCounter, 130 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 857 SdHoareTripleChecker+Invalid, 130 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 130 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:02,557 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 857 Invalid, 130 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 130 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:02,558 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-05-07 17:28:02,562 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 92.
[2025-05-07 17:28:02,563 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 41 states have (on average 1.024390243902439) internal successors, (42), 42 states have internal predecessors, (42), 24 states have call successors, (27), 21 states have call predecessors, (27), 26 states have return successors, (34), 28 states have call predecessors, (34), 24 states have call successors, (34)
[2025-05-07 17:28:02,563 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 103 transitions.
[2025-05-07 17:28:02,563 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 103 transitions. Word has length 66
[2025-05-07 17:28:02,564 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:02,564 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 103 transitions.
[2025-05-07 17:28:02,564 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 10 states have (on average 3.0) internal successors, (30), 12 states have internal predecessors, (30), 5 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 9 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:28:02,564 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 103 transitions.
[2025-05-07 17:28:02,565 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:28:02,565 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:02,565 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, 1, 1, 1, 1]
[2025-05-07 17:28:02,565 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:28:02,565 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:02,565 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:02,565 INFO  L85        PathProgramCache]: Analyzing trace with hash 363201955, now seen corresponding path program 1 times
[2025-05-07 17:28:02,566 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:02,566 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1147668383]
[2025-05-07 17:28:02,566 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:02,566 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:02,589 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:28:02,597 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:28:02,597 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:02,597 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:02,660 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:28:02,660 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:02,660 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1147668383]
[2025-05-07 17:28:02,660 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1147668383] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:02,660 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:02,660 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:02,660 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1438837226]
[2025-05-07 17:28:02,660 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:02,661 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:02,661 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:02,661 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:02,661 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:02,662 INFO  L87              Difference]: Start difference. First operand 92 states and 103 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:28:02,687 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:02,687 INFO  L93              Difference]: Finished difference Result 96 states and 107 transitions.
[2025-05-07 17:28:02,687 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:02,688 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18) Word has length 66
[2025-05-07 17:28:02,688 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:02,689 INFO  L225             Difference]: With dead ends: 96
[2025-05-07 17:28:02,689 INFO  L226             Difference]: Without dead ends: 96
[2025-05-07 17:28:02,689 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:28:02,689 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 1 mSDsluCounter, 338 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 425 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:28:02,689 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 425 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:02,690 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 96 states.
[2025-05-07 17:28:02,694 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 96 to 92.
[2025-05-07 17:28:02,694 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 41 states have (on average 1.024390243902439) internal successors, (42), 42 states have internal predecessors, (42), 24 states have call successors, (27), 21 states have call predecessors, (27), 26 states have return successors, (34), 28 states have call predecessors, (34), 24 states have call successors, (34)
[2025-05-07 17:28:02,695 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 103 transitions.
[2025-05-07 17:28:02,695 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 103 transitions. Word has length 66
[2025-05-07 17:28:02,695 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:02,695 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 103 transitions.
[2025-05-07 17:28:02,695 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:28:02,695 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 103 transitions.
[2025-05-07 17:28:02,696 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 67
[2025-05-07 17:28:02,696 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:02,696 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, 1, 1, 1, 1]
[2025-05-07 17:28:02,696 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:28:02,696 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:02,696 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:02,697 INFO  L85        PathProgramCache]: Analyzing trace with hash -66319397, now seen corresponding path program 1 times
[2025-05-07 17:28:02,697 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:02,697 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1786207813]
[2025-05-07 17:28:02,697 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:02,697 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:02,719 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 66 statements into 1 equivalence classes.
[2025-05-07 17:28:02,729 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 66 of 66 statements.
[2025-05-07 17:28:02,730 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:02,730 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:02,786 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:28:02,786 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:02,786 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1786207813]
[2025-05-07 17:28:02,786 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1786207813] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:02,786 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:28:02,786 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:28:02,786 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [257417601]
[2025-05-07 17:28:02,786 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:02,787 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:02,787 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:02,787 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:02,787 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:02,788 INFO  L87              Difference]: Start difference. First operand 92 states and 103 transitions. Second operand  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:28:02,813 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:02,813 INFO  L93              Difference]: Finished difference Result 92 states and 101 transitions.
[2025-05-07 17:28:02,813 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:02,813 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18) Word has length 66
[2025-05-07 17:28:02,813 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:02,814 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:28:02,814 INFO  L226             Difference]: Without dead ends: 91
[2025-05-07 17:28:02,814 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:28:02,815 INFO  L437           NwaCegarLoop]: 89 mSDtfsCounter, 1 mSDsluCounter, 343 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 432 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:28:02,815 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 432 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:02,815 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-05-07 17:28:02,818 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 87.
[2025-05-07 17:28:02,818 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 87 states, 39 states have (on average 1.0256410256410255) internal successors, (40), 40 states have internal predecessors, (40), 23 states have call successors, (26), 21 states have call predecessors, (26), 24 states have return successors, (29), 25 states have call predecessors, (29), 23 states have call successors, (29)
[2025-05-07 17:28:02,819 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 87 states to 87 states and 95 transitions.
[2025-05-07 17:28:02,819 INFO  L79                 Accepts]: Start accepts. Automaton has 87 states and 95 transitions. Word has length 66
[2025-05-07 17:28:02,819 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:02,819 INFO  L485      AbstractCegarLoop]: Abstraction has 87 states and 95 transitions.
[2025-05-07 17:28:02,819 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.0) internal successors, (30), 6 states have internal predecessors, (30), 3 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-05-07 17:28:02,819 INFO  L278                IsEmpty]: Start isEmpty. Operand 87 states and 95 transitions.
[2025-05-07 17:28:02,820 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 92
[2025-05-07 17:28:02,820 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:02,820 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 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]
[2025-05-07 17:28:02,820 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:28:02,821 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:02,821 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:02,821 INFO  L85        PathProgramCache]: Analyzing trace with hash -334145579, now seen corresponding path program 1 times
[2025-05-07 17:28:02,821 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:02,821 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [17376909]
[2025-05-07 17:28:02,821 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:02,821 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:02,851 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:28:02,862 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:28:02,862 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:02,862 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:02,955 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:28:02,955 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:02,955 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [17376909]
[2025-05-07 17:28:02,955 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [17376909] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:02,955 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [789324299]
[2025-05-07 17:28:02,955 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:02,955 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:02,958 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:02,960 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:02,961 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:28:03,183 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:28:03,310 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:28:03,310 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:03,310 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:03,315 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1327 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:03,325 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:03,367 INFO  L134       CoverageAnalysis]: Checked inductivity of 23 backedges. 22 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:28:03,367 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:28:03,367 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [789324299] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:03,367 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:28:03,368 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6] total 6
[2025-05-07 17:28:03,368 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1259591822]
[2025-05-07 17:28:03,368 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:03,368 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:03,368 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:03,369 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:03,369 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:03,369 INFO  L87              Difference]: Start difference. First operand 87 states and 95 transitions. Second operand  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (25), 2 states have call predecessors, (25), 5 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:28:03,397 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:03,397 INFO  L93              Difference]: Finished difference Result 87 states and 94 transitions.
[2025-05-07 17:28:03,397 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:03,397 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (25), 2 states have call predecessors, (25), 5 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25) Word has length 91
[2025-05-07 17:28:03,398 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:03,398 INFO  L225             Difference]: With dead ends: 87
[2025-05-07 17:28:03,398 INFO  L226             Difference]: Without dead ends: 87
[2025-05-07 17:28:03,399 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 96 GetRequests, 92 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:28:03,399 INFO  L437           NwaCegarLoop]: 89 mSDtfsCounter, 1 mSDsluCounter, 341 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 430 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:03,399 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 430 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:03,400 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 87 states.
[2025-05-07 17:28:03,405 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 87 to 87.
[2025-05-07 17:28:03,405 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 87 states, 39 states have (on average 1.0256410256410255) internal successors, (40), 40 states have internal predecessors, (40), 23 states have call successors, (26), 21 states have call predecessors, (26), 24 states have return successors, (28), 25 states have call predecessors, (28), 23 states have call successors, (28)
[2025-05-07 17:28:03,406 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 87 states to 87 states and 94 transitions.
[2025-05-07 17:28:03,406 INFO  L79                 Accepts]: Start accepts. Automaton has 87 states and 94 transitions. Word has length 91
[2025-05-07 17:28:03,406 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:03,406 INFO  L485      AbstractCegarLoop]: Abstraction has 87 states and 94 transitions.
[2025-05-07 17:28:03,407 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (25), 2 states have call predecessors, (25), 5 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:28:03,407 INFO  L278                IsEmpty]: Start isEmpty. Operand 87 states and 94 transitions.
[2025-05-07 17:28:03,408 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 92
[2025-05-07 17:28:03,408 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:03,408 INFO  L218           NwaCegarLoop]: trace histogram [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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:03,413 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:28:03,609 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable7
[2025-05-07 17:28:03,609 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:03,609 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:03,610 INFO  L85        PathProgramCache]: Analyzing trace with hash 1649068243, now seen corresponding path program 1 times
[2025-05-07 17:28:03,610 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:03,610 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [440007968]
[2025-05-07 17:28:03,610 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:03,610 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:03,662 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:28:03,684 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:28:03,685 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:03,685 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:03,770 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:28:03,770 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:03,770 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [440007968]
[2025-05-07 17:28:03,770 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [440007968] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:03,770 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1097207092]
[2025-05-07 17:28:03,770 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:03,770 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:03,773 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:03,774 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:03,775 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:28:03,994 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:28:04,132 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:28:04,132 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:04,132 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:04,138 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1276 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:04,142 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:04,169 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 18 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:28:04,169 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:28:04,169 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1097207092] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:04,169 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:28:04,169 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6] total 6
[2025-05-07 17:28:04,169 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2000250780]
[2025-05-07 17:28:04,169 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:04,170 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:04,170 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:04,170 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:04,170 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:04,171 INFO  L87              Difference]: Start difference. First operand 87 states and 94 transitions. Second operand  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (25), 2 states have call predecessors, (25), 5 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:28:04,195 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:04,195 INFO  L93              Difference]: Finished difference Result 91 states and 97 transitions.
[2025-05-07 17:28:04,195 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:04,195 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (25), 2 states have call predecessors, (25), 5 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25) Word has length 91
[2025-05-07 17:28:04,196 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:04,196 INFO  L225             Difference]: With dead ends: 91
[2025-05-07 17:28:04,196 INFO  L226             Difference]: Without dead ends: 83
[2025-05-07 17:28:04,197 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 96 GetRequests, 92 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:28:04,197 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 1 mSDsluCounter, 336 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 423 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:04,197 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 423 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:04,198 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 83 states.
[2025-05-07 17:28:04,202 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 83 to 83.
[2025-05-07 17:28:04,202 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 83 states, 37 states have (on average 1.027027027027027) internal successors, (38), 38 states have internal predecessors, (38), 22 states have call successors, (24), 20 states have call predecessors, (24), 23 states have return successors, (26), 24 states have call predecessors, (26), 22 states have call successors, (26)
[2025-05-07 17:28:04,203 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 83 states to 83 states and 88 transitions.
[2025-05-07 17:28:04,203 INFO  L79                 Accepts]: Start accepts. Automaton has 83 states and 88 transitions. Word has length 91
[2025-05-07 17:28:04,203 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:04,203 INFO  L485      AbstractCegarLoop]: Abstraction has 83 states and 88 transitions.
[2025-05-07 17:28:04,203 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (25), 2 states have call predecessors, (25), 5 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:28:04,203 INFO  L278                IsEmpty]: Start isEmpty. Operand 83 states and 88 transitions.
[2025-05-07 17:28:04,204 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 92
[2025-05-07 17:28:04,204 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:04,204 INFO  L218           NwaCegarLoop]: trace histogram [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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:04,211 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:28:04,405 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:04,406 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:04,407 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:04,407 INFO  L85        PathProgramCache]: Analyzing trace with hash -239055349, now seen corresponding path program 1 times
[2025-05-07 17:28:04,407 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:04,408 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1858520215]
[2025-05-07 17:28:04,408 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:04,408 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:04,535 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:28:04,556 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:28:04,556 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:04,556 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:04,633 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-05-07 17:28:04,633 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:04,633 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1858520215]
[2025-05-07 17:28:04,633 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1858520215] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:04,633 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [137069322]
[2025-05-07 17:28:04,633 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:04,633 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:04,636 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:04,637 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:04,638 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:28:04,860 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:28:04,998 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:28:04,999 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:04,999 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:05,003 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1302 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:05,007 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:05,029 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 18 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:28:05,029 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-05-07 17:28:05,029 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [137069322] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:28:05,029 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-05-07 17:28:05,029 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6] total 6
[2025-05-07 17:28:05,029 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1855277880]
[2025-05-07 17:28:05,029 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:28:05,030 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:05,030 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:05,030 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:05,030 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:05,030 INFO  L87              Difference]: Start difference. First operand 83 states and 88 transitions. Second operand  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (25), 2 states have call predecessors, (25), 5 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:28:05,050 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:05,050 INFO  L93              Difference]: Finished difference Result 87 states and 91 transitions.
[2025-05-07 17:28:05,051 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:05,051 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (25), 2 states have call predecessors, (25), 5 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25) Word has length 91
[2025-05-07 17:28:05,051 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:05,052 INFO  L225             Difference]: With dead ends: 87
[2025-05-07 17:28:05,052 INFO  L226             Difference]: Without dead ends: 79
[2025-05-07 17:28:05,052 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 96 GetRequests, 92 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:28:05,052 INFO  L437           NwaCegarLoop]: 84 mSDtfsCounter, 1 mSDsluCounter, 321 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 405 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:05,052 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 405 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:28:05,053 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 79 states.
[2025-05-07 17:28:05,056 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 79 to 79.
[2025-05-07 17:28:05,056 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 35 states have (on average 1.0285714285714285) internal successors, (36), 36 states have internal predecessors, (36), 21 states have call successors, (22), 19 states have call predecessors, (22), 22 states have return successors, (24), 23 states have call predecessors, (24), 21 states have call successors, (24)
[2025-05-07 17:28:05,057 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 82 transitions.
[2025-05-07 17:28:05,057 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 82 transitions. Word has length 91
[2025-05-07 17:28:05,057 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:05,057 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 82 transitions.
[2025-05-07 17:28:05,058 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 8.2) internal successors, (41), 6 states have internal predecessors, (41), 4 states have call successors, (25), 2 states have call predecessors, (25), 5 states have return successors, (25), 6 states have call predecessors, (25), 4 states have call successors, (25)
[2025-05-07 17:28:05,058 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 82 transitions.
[2025-05-07 17:28:05,058 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 92
[2025-05-07 17:28:05,059 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:05,059 INFO  L218           NwaCegarLoop]: trace histogram [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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:05,064 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:28:05,259 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:05,260 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:05,261 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:05,261 INFO  L85        PathProgramCache]: Analyzing trace with hash 1541091641, now seen corresponding path program 1 times
[2025-05-07 17:28:05,261 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:05,261 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [460398099]
[2025-05-07 17:28:05,261 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:05,261 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:05,360 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:28:05,389 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:28:05,389 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:05,389 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,305 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 7 proven. 4 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:28:06,305 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:06,305 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [460398099]
[2025-05-07 17:28:06,305 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [460398099] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:06,305 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [909011921]
[2025-05-07 17:28:06,305 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:28:06,305 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:06,308 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:06,310 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:06,311 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-05-07 17:28:06,512 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 91 statements into 1 equivalence classes.
[2025-05-07 17:28:06,621 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 91 of 91 statements.
[2025-05-07 17:28:06,621 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:28:06,621 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:06,627 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1346 conjuncts, 64 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:06,632 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:06,655 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-05-07 17:28:06,863 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 7 proven. 4 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:28:06,863 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:10,557 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 7 proven. 4 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:28:10,557 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [909011921] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:10,557 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:10,557 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 15, 15] total 23
[2025-05-07 17:28:10,557 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [384642044]
[2025-05-07 17:28:10,558 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:10,558 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-05-07 17:28:10,558 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:10,559 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-05-07 17:28:10,559 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=59, Invalid=447, Unknown=0, NotChecked=0, Total=506
[2025-05-07 17:28:10,560 INFO  L87              Difference]: Start difference. First operand 79 states and 82 transitions. Second operand  has 23 states, 15 states have (on average 3.3333333333333335) internal successors, (50), 21 states have internal predecessors, (50), 13 states have call successors, (33), 1 states have call predecessors, (33), 15 states have return successors, (38), 19 states have call predecessors, (38), 13 states have call successors, (38)
[2025-05-07 17:28:10,774 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:10,774 INFO  L93              Difference]: Finished difference Result 73 states and 76 transitions.
[2025-05-07 17:28:10,775 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-05-07 17:28:10,775 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 15 states have (on average 3.3333333333333335) internal successors, (50), 21 states have internal predecessors, (50), 13 states have call successors, (33), 1 states have call predecessors, (33), 15 states have return successors, (38), 19 states have call predecessors, (38), 13 states have call successors, (38) Word has length 91
[2025-05-07 17:28:10,775 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:10,775 INFO  L225             Difference]: With dead ends: 73
[2025-05-07 17:28:10,775 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:28:10,776 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 205 GetRequests, 172 SyntacticMatches, 8 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 92 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=87, Invalid=615, Unknown=0, NotChecked=0, Total=702
[2025-05-07 17:28:10,776 INFO  L437           NwaCegarLoop]: 67 mSDtfsCounter, 7 mSDsluCounter, 1013 mSDsCounter, 0 mSdLazyCounter, 165 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 1080 SdHoareTripleChecker+Invalid, 172 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 165 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:10,776 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 1080 Invalid, 172 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 165 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:28:10,776 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:28:10,776 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:28:10,776 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:28:10,777 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:28:10,777 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 91
[2025-05-07 17:28:10,777 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:10,777 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:28:10,777 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 15 states have (on average 3.3333333333333335) internal successors, (50), 21 states have internal predecessors, (50), 13 states have call successors, (33), 1 states have call predecessors, (33), 15 states have return successors, (38), 19 states have call predecessors, (38), 13 states have call successors, (38)
[2025-05-07 17:28:10,777 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:28:10,777 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:28:10,779 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:28:10,784 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-05-07 17:28:10,980 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable10
[2025-05-07 17:28:10,988 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:10,994 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:28:11,001 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:28:11 BoogieIcfgContainer
[2025-05-07 17:28:11,001 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:28:11,003 INFO  L158              Benchmark]: Toolchain (without parser) took 11579.63ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 148.8MB in the beginning and 271.0MB in the end (delta: -122.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:11,004 INFO  L158              Benchmark]: SmtParser took 0.19ms. Allocated memory is still 234.9MB. Free memory is still 172.8MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:11,004 INFO  L158              Benchmark]: ChcToBoogie took 43.26ms. Allocated memory is still 234.9MB. Free memory was 148.8MB in the beginning and 145.9MB in the end (delta: 2.9MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:11,005 INFO  L158              Benchmark]: Boogie Preprocessor took 60.57ms. Allocated memory is still 234.9MB. Free memory was 145.9MB in the beginning and 142.6MB in the end (delta: 3.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:28:11,006 INFO  L158              Benchmark]: RCFGBuilder took 398.59ms. Allocated memory is still 234.9MB. Free memory was 142.6MB in the beginning and 181.3MB in the end (delta: -38.7MB). Peak memory consumption was 42.1MB. Max. memory is 33.6GB.
[2025-05-07 17:28:11,007 INFO  L158              Benchmark]: TraceAbstraction took 11072.95ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 180.8MB in the beginning and 271.0MB in the end (delta: -90.2MB). Peak memory consumption was 25.7MB. Max. memory is 33.6GB.
[2025-05-07 17:28:11,010 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.19ms. Allocated memory is still 234.9MB. Free memory is still 172.8MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 43.26ms. Allocated memory is still 234.9MB. Free memory was 148.8MB in the beginning and 145.9MB in the end (delta: 2.9MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 60.57ms. Allocated memory is still 234.9MB. Free memory was 145.9MB in the beginning and 142.6MB in the end (delta: 3.2MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 398.59ms. Allocated memory is still 234.9MB. Free memory was 142.6MB in the beginning and 181.3MB in the end (delta: -38.7MB). Peak memory consumption was 42.1MB. Max. memory is 33.6GB.
 * TraceAbstraction took 11072.95ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 180.8MB in the beginning and 271.0MB in the end (delta: -90.2MB). Peak memory consumption was 25.7MB. 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 22 procedures, 87 locations, 131 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 11.0s, OverallIterations: 10, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.9s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 39 SdHoareTripleChecker+Valid, 0.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 19 mSDsluCounter, 5662 SdHoareTripleChecker+Invalid, 0.5s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 4804 mSDsCounter, 11 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 604 IncrementalHoareTripleChecker+Invalid, 615 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 11 mSolverCounterUnsat, 858 mSDtfsCounter, 604 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 550 GetRequests, 467 SyntacticMatches, 8 SemanticMatches, 75 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 98 ImplicationChecksByTransitivity, 0.7s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=92occurred in iteration=4, InterpolantAutomatonStates: 78, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 10 MinimizatonAttempts, 12 StatesRemovedByMinimization, 4 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.4s SsaConstructionTime, 0.7s SatisfiabilityAnalysisTime, 7.0s InterpolantComputationTime, 1124 NumberOfCodeBlocks, 1124 NumberOfCodeBlocksAsserted, 14 NumberOfCheckSat, 1200 ConstructedInterpolants, 0 QuantifiedInterpolants, 2041 SizeOfPredicates, 26 NumberOfNonLiveVariables, 5251 ConjunctsInSsa, 79 ConjunctsInUnsatCore, 15 InterpolantComputations, 9 PerfectInterpolantSequences, 152/179 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:28:11,029 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
