./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol_2_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:24:03,496 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:24:03,544 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c9d9cd3a-0953-43ce-affc-8836280f1138/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:24:03,548 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:24:03,549 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:24:03,567 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:24:03,568 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:24:03,568 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:24:03,568 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:24:03,568 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:24:03,569 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:24:03,569 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:24:03,569 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:24:03,569 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:24:03,569 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:24:03,569 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:24:03,569 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:24:03,569 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:24:03,569 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:24:03,570 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:24:03,570 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:24:03,570 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:24:03,570 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:24:03,570 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:24:03,570 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:24:03,571 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:24:03,571 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:24:03,781 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:24:03,789 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:24:03,792 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:24:03,793 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:24:03,793 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:24:03,794 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c9d9cd3a-0953-43ce-affc-8836280f1138/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol_2_no_adts_000.smt2
[2025-05-07 17:24:03,795 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:24:03,798 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:24:04,129 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c9d9cd3a-0953-43ce-affc-8836280f1138/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol_2_no_adts_000.smt2
[2025-05-07 17:24:04,132 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:24:04,134 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:24:04,134 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:24:04,135 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:24:04,135 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:24:04,137 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,184 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04 Unit
[2025-05-07 17:24:04,185 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:24:04,185 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:24:04,186 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:24:04,186 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:24:04,199 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,199 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,224 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,225 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,237 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,239 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,242 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,248 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,252 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,266 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:24:04,267 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:24:04,267 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:24:04,267 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:24:04,268 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (1/1) ...
[2025-05-07 17:24:04,271 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:24:04,283 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:24:04,293 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:24:04,295 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:24:04,303 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:24:04,303 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:24:04,303 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:24:04,303 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_5_0 given in one single declaration
[2025-05-07 17:24:04,303 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_5_0
[2025-05-07 17:24:04,303 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_5_0
[2025-05-07 17:24:04,303 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_17_C_90_0 given in one single declaration
[2025-05-07 17:24:04,303 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_17_C_90_0
[2025-05-07 17:24:04,304 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_17_C_90_0
[2025-05-07 17:24:04,304 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_71_C_90_0 given in one single declaration
[2025-05-07 17:24:04,304 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_71_C_90_0
[2025-05-07 17:24:04,304 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_71_C_90_0
[2025-05-07 17:24:04,304 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_22_constructor_89_90_0 given in one single declaration
[2025-05-07 17:24:04,304 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_22_constructor_89_90_0
[2025-05-07 17:24:04,304 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_22_constructor_89_90_0
[2025-05-07 17:24:04,304 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_69_constructor_89_90_0 given in one single declaration
[2025-05-07 17:24:04,304 INFO  L130     BoogieDeclarations]: Found specification of procedure block_69_constructor_89_90_0
[2025-05-07 17:24:04,304 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_69_constructor_89_90_0
[2025-05-07 17:24:04,304 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_66__88_90_0 given in one single declaration
[2025-05-07 17:24:04,304 INFO  L130     BoogieDeclarations]: Found specification of procedure block_66__88_90_0
[2025-05-07 17:24:04,305 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_66__88_90_0
[2025-05-07 17:24:04,305 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_65_constructor_89_90_0 given in one single declaration
[2025-05-07 17:24:04,305 INFO  L130     BoogieDeclarations]: Found specification of procedure block_65_constructor_89_90_0
[2025-05-07 17:24:04,305 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_65_constructor_89_90_0
[2025-05-07 17:24:04,305 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_70_constructor_89_90_0 given in one single declaration
[2025-05-07 17:24:04,305 INFO  L130     BoogieDeclarations]: Found specification of procedure block_70_constructor_89_90_0
[2025-05-07 17:24:04,305 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_70_constructor_89_90_0
[2025-05-07 17:24:04,305 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_68_constructor_89_90_0 given in one single declaration
[2025-05-07 17:24:04,305 INFO  L130     BoogieDeclarations]: Found specification of procedure block_68_constructor_89_90_0
[2025-05-07 17:24:04,305 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_68_constructor_89_90_0
[2025-05-07 17:24:04,305 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_67_return_constructor_89_90_0 given in one single declaration
[2025-05-07 17:24:04,305 INFO  L130     BoogieDeclarations]: Found specification of procedure block_67_return_constructor_89_90_0
[2025-05-07 17:24:04,305 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_67_return_constructor_89_90_0
[2025-05-07 17:24:04,305 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_73_C_90_0 given in one single declaration
[2025-05-07 17:24:04,305 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_73_C_90_0
[2025-05-07 17:24:04,305 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_73_C_90_0
[2025-05-07 17:24:04,306 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_72_C_90_0 given in one single declaration
[2025-05-07 17:24:04,306 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_72_C_90_0
[2025-05-07 17:24:04,306 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_72_C_90_0
[2025-05-07 17:24:04,306 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_77_B_42_0 given in one single declaration
[2025-05-07 17:24:04,306 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_77_B_42_0
[2025-05-07 17:24:04,306 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_77_B_42_0
[2025-05-07 17:24:04,306 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_constructor_27_90_0 given in one single declaration
[2025-05-07 17:24:04,306 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_constructor_27_90_0
[2025-05-07 17:24:04,306 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_constructor_27_90_0
[2025-05-07 17:24:04,306 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_76_return_constructor_27_90_0 given in one single declaration
[2025-05-07 17:24:04,306 INFO  L130     BoogieDeclarations]: Found specification of procedure block_76_return_constructor_27_90_0
[2025-05-07 17:24:04,306 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_76_return_constructor_27_90_0
[2025-05-07 17:24:04,306 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_75__26_90_0 given in one single declaration
[2025-05-07 17:24:04,307 INFO  L130     BoogieDeclarations]: Found specification of procedure block_75__26_90_0
[2025-05-07 17:24:04,307 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_75__26_90_0
[2025-05-07 17:24:04,307 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_74_constructor_27_90_0 given in one single declaration
[2025-05-07 17:24:04,307 INFO  L130     BoogieDeclarations]: Found specification of procedure block_74_constructor_27_90_0
[2025-05-07 17:24:04,307 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_74_constructor_27_90_0
[2025-05-07 17:24:04,307 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_79_B_42_0 given in one single declaration
[2025-05-07 17:24:04,307 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_79_B_42_0
[2025-05-07 17:24:04,307 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_79_B_42_0
[2025-05-07 17:24:04,307 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_78_B_42_0 given in one single declaration
[2025-05-07 17:24:04,307 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_78_B_42_0
[2025-05-07 17:24:04,307 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_78_B_42_0
[2025-05-07 17:24:04,307 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_83_Z_57_0 given in one single declaration
[2025-05-07 17:24:04,307 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_83_Z_57_0
[2025-05-07 17:24:04,307 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_83_Z_57_0
[2025-05-07 17:24:04,307 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_21_constructor_56_90_0 given in one single declaration
[2025-05-07 17:24:04,308 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_21_constructor_56_90_0
[2025-05-07 17:24:04,308 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_21_constructor_56_90_0
[2025-05-07 17:24:04,308 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_82_return_constructor_56_90_0 given in one single declaration
[2025-05-07 17:24:04,308 INFO  L130     BoogieDeclarations]: Found specification of procedure block_82_return_constructor_56_90_0
[2025-05-07 17:24:04,308 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_82_return_constructor_56_90_0
[2025-05-07 17:24:04,308 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_81__55_90_0 given in one single declaration
[2025-05-07 17:24:04,308 INFO  L130     BoogieDeclarations]: Found specification of procedure block_81__55_90_0
[2025-05-07 17:24:04,308 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_81__55_90_0
[2025-05-07 17:24:04,308 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_80_constructor_56_90_0 given in one single declaration
[2025-05-07 17:24:04,308 INFO  L130     BoogieDeclarations]: Found specification of procedure block_80_constructor_56_90_0
[2025-05-07 17:24:04,308 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_80_constructor_56_90_0
[2025-05-07 17:24:04,308 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_85_Z_57_0 given in one single declaration
[2025-05-07 17:24:04,308 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_85_Z_57_0
[2025-05-07 17:24:04,308 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_85_Z_57_0
[2025-05-07 17:24:04,309 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_84_Z_57_0 given in one single declaration
[2025-05-07 17:24:04,309 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_84_Z_57_0
[2025-05-07 17:24:04,309 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_84_Z_57_0
[2025-05-07 17:24:04,309 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_89_A_13_0 given in one single declaration
[2025-05-07 17:24:04,309 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_89_A_13_0
[2025-05-07 17:24:04,309 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_89_A_13_0
[2025-05-07 17:24:04,309 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_91_A_13_0 given in one single declaration
[2025-05-07 17:24:04,309 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_91_A_13_0
[2025-05-07 17:24:04,309 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_91_A_13_0
[2025-05-07 17:24:04,309 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_90_A_13_0 given in one single declaration
[2025-05-07 17:24:04,309 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_90_A_13_0
[2025-05-07 17:24:04,309 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_90_A_13_0
[2025-05-07 17:24:04,309 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_constructor_12_90_0 given in one single declaration
[2025-05-07 17:24:04,309 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_constructor_12_90_0
[2025-05-07 17:24:04,309 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_constructor_12_90_0
[2025-05-07 17:24:04,309 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_88_return_constructor_12_90_0 given in one single declaration
[2025-05-07 17:24:04,309 INFO  L130     BoogieDeclarations]: Found specification of procedure block_88_return_constructor_12_90_0
[2025-05-07 17:24:04,309 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_88_return_constructor_12_90_0
[2025-05-07 17:24:04,309 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_87__11_90_0 given in one single declaration
[2025-05-07 17:24:04,309 INFO  L130     BoogieDeclarations]: Found specification of procedure block_87__11_90_0
[2025-05-07 17:24:04,309 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_87__11_90_0
[2025-05-07 17:24:04,309 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_86_constructor_12_90_0 given in one single declaration
[2025-05-07 17:24:04,310 INFO  L130     BoogieDeclarations]: Found specification of procedure block_86_constructor_12_90_0
[2025-05-07 17:24:04,310 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_86_constructor_12_90_0
[2025-05-07 17:24:04,310 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_93_function_f__41_90_0 given in one single declaration
[2025-05-07 17:24:04,310 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_93_function_f__41_90_0
[2025-05-07 17:24:04,310 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_93_function_f__41_90_0
[2025-05-07 17:24:04,310 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_20_function_f__41_90_0 given in one single declaration
[2025-05-07 17:24:04,310 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_20_function_f__41_90_0
[2025-05-07 17:24:04,310 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_20_function_f__41_90_0
[2025-05-07 17:24:04,310 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_63_return_function_f__41_90_0 given in one single declaration
[2025-05-07 17:24:04,310 INFO  L130     BoogieDeclarations]: Found specification of procedure block_63_return_function_f__41_90_0
[2025-05-07 17:24:04,310 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_63_return_function_f__41_90_0
[2025-05-07 17:24:04,310 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_62_f_40_90_0 given in one single declaration
[2025-05-07 17:24:04,310 INFO  L130     BoogieDeclarations]: Found specification of procedure block_62_f_40_90_0
[2025-05-07 17:24:04,310 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_62_f_40_90_0
[2025-05-07 17:24:04,310 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_61_function_f__41_90_0 given in one single declaration
[2025-05-07 17:24:04,310 INFO  L130     BoogieDeclarations]: Found specification of procedure block_61_function_f__41_90_0
[2025-05-07 17:24:04,310 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_61_function_f__41_90_0
[2025-05-07 17:24:04,310 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_92_C_90_0 given in one single declaration
[2025-05-07 17:24:04,310 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_92_C_90_0
[2025-05-07 17:24:04,310 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_92_C_90_0
[2025-05-07 17:24:04,310 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:24:04,310 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:24:04,311 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:24:04,529 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:24:04,532 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:24:04,818 INFO  L?                        ?]: Removed 407 outVars from TransFormulas that were not future-live.
[2025-05-07 17:24:04,818 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:24:04,828 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:24:04,829 INFO  L312             CfgBuilder]: Removed 19 assume(true) statements.
[2025-05-07 17:24:04,829 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:24:04 BoogieIcfgContainer
[2025-05-07 17:24:04,829 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:24:04,830 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:24:04,830 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:24:04,833 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:24:04,833 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:24:04" (1/3) ...
[2025-05-07 17:24:04,834 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@291833bf and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:24:04, skipping insertion in model container
[2025-05-07 17:24:04,834 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:24:04" (2/3) ...
[2025-05-07 17:24:04,834 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@291833bf and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:24:04, skipping insertion in model container
[2025-05-07 17:24:04,834 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:24:04" (3/3) ...
[2025-05-07 17:24:04,835 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:24:04,845 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:24:04,847 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 41 procedures, 176 locations, 289 edges, 41 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:24:04,878 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:24:04,886 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;@49621764, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:24:04,886 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:24:04,889 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 176 states, 66 states have (on average 1.1515151515151516) internal successors, (76), 76 states have internal predecessors, (76), 68 states have call successors, (71), 40 states have call predecessors, (71), 40 states have return successors, (71), 59 states have call predecessors, (71), 68 states have call successors, (71)
[2025-05-07 17:24:04,898 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-05-07 17:24:04,898 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:04,898 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]
[2025-05-07 17:24:04,899 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:04,902 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:04,902 INFO  L85        PathProgramCache]: Analyzing trace with hash -1563801670, now seen corresponding path program 1 times
[2025-05-07 17:24:04,907 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:04,908 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2094359164]
[2025-05-07 17:24:04,908 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:04,908 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:04,941 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-05-07 17:24:04,986 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-05-07 17:24:04,987 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:04,987 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:05,192 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:24:05,192 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:05,192 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2094359164]
[2025-05-07 17:24:05,193 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2094359164] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:05,193 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:05,195 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:24:05,196 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1138233883]
[2025-05-07 17:24:05,197 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:05,199 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:24:05,199 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:05,230 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:24:05,230 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:24:05,233 INFO  L87              Difference]: Start difference. First operand  has 176 states, 66 states have (on average 1.1515151515151516) internal successors, (76), 76 states have internal predecessors, (76), 68 states have call successors, (71), 40 states have call predecessors, (71), 40 states have return successors, (71), 59 states have call predecessors, (71), 68 states have call successors, (71) Second operand  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-05-07 17:24:05,375 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:05,375 INFO  L93              Difference]: Finished difference Result 176 states and 217 transitions.
[2025-05-07 17:24:05,376 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:24:05,378 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9) Word has length 33
[2025-05-07 17:24:05,378 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:05,384 INFO  L225             Difference]: With dead ends: 176
[2025-05-07 17:24:05,384 INFO  L226             Difference]: Without dead ends: 174
[2025-05-07 17:24:05,385 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:24:05,387 INFO  L437           NwaCegarLoop]: 206 mSDtfsCounter, 1 mSDsluCounter, 993 mSDsCounter, 0 mSdLazyCounter, 58 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 1199 SdHoareTripleChecker+Invalid, 62 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 58 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:05,388 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 1199 Invalid, 62 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 58 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:24:05,398 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 174 states.
[2025-05-07 17:24:05,417 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 174 to 172.
[2025-05-07 17:24:05,418 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 172 states, 65 states have (on average 1.123076923076923) internal successors, (73), 73 states have internal predecessors, (73), 66 states have call successors, (69), 40 states have call predecessors, (69), 40 states have return successors, (69), 58 states have call predecessors, (69), 66 states have call successors, (69)
[2025-05-07 17:24:05,421 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 172 states to 172 states and 211 transitions.
[2025-05-07 17:24:05,422 INFO  L79                 Accepts]: Start accepts. Automaton has 172 states and 211 transitions. Word has length 33
[2025-05-07 17:24:05,423 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:05,423 INFO  L485      AbstractCegarLoop]: Abstraction has 172 states and 211 transitions.
[2025-05-07 17:24:05,423 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.5) internal successors, (15), 7 states have internal predecessors, (15), 3 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 3 states have call successors, (9)
[2025-05-07 17:24:05,423 INFO  L278                IsEmpty]: Start isEmpty. Operand 172 states and 211 transitions.
[2025-05-07 17:24:05,424 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:24:05,425 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:05,425 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:24:05,425 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:24:05,425 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:05,426 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:05,426 INFO  L85        PathProgramCache]: Analyzing trace with hash 1287439724, now seen corresponding path program 1 times
[2025-05-07 17:24:05,426 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:05,426 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1099032628]
[2025-05-07 17:24:05,426 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:05,426 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:05,452 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:24:05,479 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:24:05,479 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:05,479 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:05,582 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:24:05,582 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:05,582 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1099032628]
[2025-05-07 17:24:05,582 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1099032628] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:05,582 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:05,582 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:24:05,582 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [246428029]
[2025-05-07 17:24:05,582 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:05,583 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:24:05,583 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:05,584 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:24:05,584 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:24:05,584 INFO  L87              Difference]: Start difference. First operand 172 states and 211 transitions. Second operand  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:24:05,631 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:05,631 INFO  L93              Difference]: Finished difference Result 171 states and 208 transitions.
[2025-05-07 17:24:05,631 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:24:05,631 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 4 states have call successors, (16) Word has length 58
[2025-05-07 17:24:05,631 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:05,633 INFO  L225             Difference]: With dead ends: 171
[2025-05-07 17:24:05,633 INFO  L226             Difference]: Without dead ends: 170
[2025-05-07 17:24:05,633 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:24:05,633 INFO  L437           NwaCegarLoop]: 205 mSDtfsCounter, 0 mSDsluCounter, 804 mSDsCounter, 0 mSdLazyCounter, 23 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1009 SdHoareTripleChecker+Invalid, 23 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 23 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:05,633 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1009 Invalid, 23 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 23 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:05,634 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 170 states.
[2025-05-07 17:24:05,641 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 170 to 170.
[2025-05-07 17:24:05,641 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 170 states, 65 states have (on average 1.1076923076923078) internal successors, (72), 72 states have internal predecessors, (72), 64 states have call successors, (67), 40 states have call predecessors, (67), 40 states have return successors, (67), 57 states have call predecessors, (67), 64 states have call successors, (67)
[2025-05-07 17:24:05,643 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 170 states to 170 states and 206 transitions.
[2025-05-07 17:24:05,643 INFO  L79                 Accepts]: Start accepts. Automaton has 170 states and 206 transitions. Word has length 58
[2025-05-07 17:24:05,643 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:05,644 INFO  L485      AbstractCegarLoop]: Abstraction has 170 states and 206 transitions.
[2025-05-07 17:24:05,644 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 5.2) internal successors, (26), 6 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 5 states have return successors, (16), 5 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:24:05,644 INFO  L278                IsEmpty]: Start isEmpty. Operand 170 states and 206 transitions.
[2025-05-07 17:24:05,645 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:24:05,645 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:05,645 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:24:05,645 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:24:05,645 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:05,645 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:05,645 INFO  L85        PathProgramCache]: Analyzing trace with hash -1098423960, now seen corresponding path program 1 times
[2025-05-07 17:24:05,645 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:05,645 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2096507621]
[2025-05-07 17:24:05,646 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:05,646 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:05,668 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:24:05,675 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:24:05,675 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:05,676 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:05,734 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:24:05,734 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:05,734 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2096507621]
[2025-05-07 17:24:05,734 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2096507621] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:05,734 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:05,734 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:24:05,734 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1021952365]
[2025-05-07 17:24:05,734 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:05,734 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:24:05,734 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:05,735 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:24:05,735 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:24:05,735 INFO  L87              Difference]: Start difference. First operand 170 states and 206 transitions. Second operand  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 4 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:24:05,789 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:05,789 INFO  L93              Difference]: Finished difference Result 171 states and 205 transitions.
[2025-05-07 17:24:05,789 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:24:05,789 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 4 states have call predecessors, (16), 4 states have call successors, (16) Word has length 58
[2025-05-07 17:24:05,790 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:05,790 INFO  L225             Difference]: With dead ends: 171
[2025-05-07 17:24:05,791 INFO  L226             Difference]: Without dead ends: 169
[2025-05-07 17:24:05,791 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:24:05,792 INFO  L437           NwaCegarLoop]: 198 mSDtfsCounter, 1 mSDsluCounter, 368 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 566 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:05,792 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 566 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:05,793 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 169 states.
[2025-05-07 17:24:05,798 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 169 to 167.
[2025-05-07 17:24:05,799 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 167 states, 65 states have (on average 1.0923076923076922) internal successors, (71), 71 states have internal predecessors, (71), 61 states have call successors, (64), 40 states have call predecessors, (64), 40 states have return successors, (64), 55 states have call predecessors, (64), 61 states have call successors, (64)
[2025-05-07 17:24:05,800 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 167 states to 167 states and 199 transitions.
[2025-05-07 17:24:05,800 INFO  L79                 Accepts]: Start accepts. Automaton has 167 states and 199 transitions. Word has length 58
[2025-05-07 17:24:05,800 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:05,800 INFO  L485      AbstractCegarLoop]: Abstraction has 167 states and 199 transitions.
[2025-05-07 17:24:05,800 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 8.666666666666666) internal successors, (26), 4 states have internal predecessors, (26), 4 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 4 states have call predecessors, (16), 4 states have call successors, (16)
[2025-05-07 17:24:05,800 INFO  L278                IsEmpty]: Start isEmpty. Operand 167 states and 199 transitions.
[2025-05-07 17:24:05,802 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:24:05,802 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:05,802 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:24:05,802 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:24:05,802 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:05,803 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:05,803 INFO  L85        PathProgramCache]: Analyzing trace with hash -809932781, now seen corresponding path program 1 times
[2025-05-07 17:24:05,803 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:05,803 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [76106836]
[2025-05-07 17:24:05,803 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:05,803 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:05,835 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:24:05,855 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:24:05,856 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:05,856 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:05,986 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:24:05,986 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:05,986 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [76106836]
[2025-05-07 17:24:05,986 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [76106836] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:05,986 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:05,986 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:24:05,986 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [719558467]
[2025-05-07 17:24:05,986 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:05,987 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:24:05,987 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:05,988 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:24:05,988 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:24:05,988 INFO  L87              Difference]: Start difference. First operand 167 states and 199 transitions. Second operand  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 3 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 3 states have call successors, (23)
[2025-05-07 17:24:06,034 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:06,034 INFO  L93              Difference]: Finished difference Result 167 states and 198 transitions.
[2025-05-07 17:24:06,034 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:24:06,034 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 3 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 3 states have call successors, (23) Word has length 83
[2025-05-07 17:24:06,035 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:06,037 INFO  L225             Difference]: With dead ends: 167
[2025-05-07 17:24:06,037 INFO  L226             Difference]: Without dead ends: 165
[2025-05-07 17:24:06,037 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:24:06,038 INFO  L437           NwaCegarLoop]: 195 mSDtfsCounter, 0 mSDsluCounter, 764 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 959 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 22 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:06,039 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 959 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:06,040 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 165 states.
[2025-05-07 17:24:06,051 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 165 to 165.
[2025-05-07 17:24:06,051 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 165 states, 65 states have (on average 1.0769230769230769) internal successors, (70), 70 states have internal predecessors, (70), 59 states have call successors, (62), 40 states have call predecessors, (62), 40 states have return successors, (62), 54 states have call predecessors, (62), 59 states have call successors, (62)
[2025-05-07 17:24:06,053 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 165 states to 165 states and 194 transitions.
[2025-05-07 17:24:06,054 INFO  L79                 Accepts]: Start accepts. Automaton has 165 states and 194 transitions. Word has length 83
[2025-05-07 17:24:06,054 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:06,054 INFO  L485      AbstractCegarLoop]: Abstraction has 165 states and 194 transitions.
[2025-05-07 17:24:06,054 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 7.4) internal successors, (37), 6 states have internal predecessors, (37), 3 states have call successors, (23), 1 states have call predecessors, (23), 5 states have return successors, (23), 6 states have call predecessors, (23), 3 states have call successors, (23)
[2025-05-07 17:24:06,054 INFO  L278                IsEmpty]: Start isEmpty. Operand 165 states and 194 transitions.
[2025-05-07 17:24:06,056 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:24:06,056 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:06,056 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:24:06,056 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:24:06,057 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:06,057 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:06,057 INFO  L85        PathProgramCache]: Analyzing trace with hash 268541071, now seen corresponding path program 1 times
[2025-05-07 17:24:06,057 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:06,057 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [749626399]
[2025-05-07 17:24:06,057 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:06,057 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:06,086 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:24:06,100 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:24:06,100 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:06,100 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:06,176 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:24:06,176 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:06,176 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [749626399]
[2025-05-07 17:24:06,177 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [749626399] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:06,177 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:06,177 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:24:06,177 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1127702136]
[2025-05-07 17:24:06,177 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:06,177 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:24:06,177 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:06,178 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:24:06,178 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:24:06,178 INFO  L87              Difference]: Start difference. First operand 165 states and 194 transitions. Second operand  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 3 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 4 states have call predecessors, (23), 3 states have call successors, (23)
[2025-05-07 17:24:06,218 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:06,218 INFO  L93              Difference]: Finished difference Result 167 states and 195 transitions.
[2025-05-07 17:24:06,218 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:24:06,219 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 3 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 4 states have call predecessors, (23), 3 states have call successors, (23) Word has length 83
[2025-05-07 17:24:06,219 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:06,221 INFO  L225             Difference]: With dead ends: 167
[2025-05-07 17:24:06,221 INFO  L226             Difference]: Without dead ends: 163
[2025-05-07 17:24:06,221 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:24:06,222 INFO  L437           NwaCegarLoop]: 189 mSDtfsCounter, 1 mSDsluCounter, 353 mSDsCounter, 0 mSdLazyCounter, 16 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 542 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 16 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:06,222 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 542 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 16 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:06,223 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 163 states.
[2025-05-07 17:24:06,228 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 163 to 161.
[2025-05-07 17:24:06,228 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 161 states, 65 states have (on average 1.0615384615384615) internal successors, (69), 69 states have internal predecessors, (69), 55 states have call successors, (58), 40 states have call predecessors, (58), 40 states have return successors, (58), 51 states have call predecessors, (58), 55 states have call successors, (58)
[2025-05-07 17:24:06,229 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 161 states to 161 states and 185 transitions.
[2025-05-07 17:24:06,229 INFO  L79                 Accepts]: Start accepts. Automaton has 161 states and 185 transitions. Word has length 83
[2025-05-07 17:24:06,229 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:06,229 INFO  L485      AbstractCegarLoop]: Abstraction has 161 states and 185 transitions.
[2025-05-07 17:24:06,229 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 12.333333333333334) internal successors, (37), 4 states have internal predecessors, (37), 3 states have call successors, (23), 1 states have call predecessors, (23), 3 states have return successors, (23), 4 states have call predecessors, (23), 3 states have call successors, (23)
[2025-05-07 17:24:06,229 INFO  L278                IsEmpty]: Start isEmpty. Operand 161 states and 185 transitions.
[2025-05-07 17:24:06,230 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 109
[2025-05-07 17:24:06,230 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:06,230 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:24:06,230 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:24:06,230 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:06,231 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:06,231 INFO  L85        PathProgramCache]: Analyzing trace with hash 61174942, now seen corresponding path program 1 times
[2025-05-07 17:24:06,231 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:06,231 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [3917251]
[2025-05-07 17:24:06,231 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:06,231 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:06,267 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 108 statements into 1 equivalence classes.
[2025-05-07 17:24:06,300 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 108 of 108 statements.
[2025-05-07 17:24:06,301 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:06,301 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:06,465 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:24:06,465 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:06,466 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [3917251]
[2025-05-07 17:24:06,466 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [3917251] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:06,466 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:06,466 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:24:06,466 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1380806823]
[2025-05-07 17:24:06,466 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:06,466 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:24:06,466 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:06,467 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:24:06,467 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:24:06,467 INFO  L87              Difference]: Start difference. First operand 161 states and 185 transitions. Second operand  has 6 states, 5 states have (on average 9.6) internal successors, (48), 6 states have internal predecessors, (48), 3 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 6 states have call predecessors, (30), 3 states have call successors, (30)
[2025-05-07 17:24:06,508 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:06,508 INFO  L93              Difference]: Finished difference Result 161 states and 184 transitions.
[2025-05-07 17:24:06,508 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:24:06,509 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 9.6) internal successors, (48), 6 states have internal predecessors, (48), 3 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 6 states have call predecessors, (30), 3 states have call successors, (30) Word has length 108
[2025-05-07 17:24:06,509 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:06,510 INFO  L225             Difference]: With dead ends: 161
[2025-05-07 17:24:06,510 INFO  L226             Difference]: Without dead ends: 159
[2025-05-07 17:24:06,510 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:24:06,511 INFO  L437           NwaCegarLoop]: 181 mSDtfsCounter, 0 mSDsluCounter, 709 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 890 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:06,511 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 890 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:06,512 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 159 states.
[2025-05-07 17:24:06,518 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 159 to 159.
[2025-05-07 17:24:06,519 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 159 states, 65 states have (on average 1.0461538461538462) internal successors, (68), 68 states have internal predecessors, (68), 53 states have call successors, (56), 40 states have call predecessors, (56), 40 states have return successors, (56), 50 states have call predecessors, (56), 53 states have call successors, (56)
[2025-05-07 17:24:06,520 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 159 states to 159 states and 180 transitions.
[2025-05-07 17:24:06,520 INFO  L79                 Accepts]: Start accepts. Automaton has 159 states and 180 transitions. Word has length 108
[2025-05-07 17:24:06,520 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:06,520 INFO  L485      AbstractCegarLoop]: Abstraction has 159 states and 180 transitions.
[2025-05-07 17:24:06,521 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 9.6) internal successors, (48), 6 states have internal predecessors, (48), 3 states have call successors, (30), 1 states have call predecessors, (30), 5 states have return successors, (30), 6 states have call predecessors, (30), 3 states have call successors, (30)
[2025-05-07 17:24:06,521 INFO  L278                IsEmpty]: Start isEmpty. Operand 159 states and 180 transitions.
[2025-05-07 17:24:06,522 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 109
[2025-05-07 17:24:06,522 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:06,522 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:24:06,523 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:24:06,523 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:06,523 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:06,523 INFO  L85        PathProgramCache]: Analyzing trace with hash -1017298910, now seen corresponding path program 1 times
[2025-05-07 17:24:06,523 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:06,523 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1159453456]
[2025-05-07 17:24:06,523 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:06,523 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:06,565 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 108 statements into 1 equivalence classes.
[2025-05-07 17:24:06,587 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 108 of 108 statements.
[2025-05-07 17:24:06,587 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:06,587 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:06,656 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:24:06,656 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:06,656 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1159453456]
[2025-05-07 17:24:06,656 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1159453456] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:06,656 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:06,656 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:24:06,656 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [884401444]
[2025-05-07 17:24:06,656 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:06,657 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:24:06,657 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:06,657 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:24:06,657 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:24:06,658 INFO  L87              Difference]: Start difference. First operand 159 states and 180 transitions. Second operand  has 4 states, 3 states have (on average 16.0) internal successors, (48), 4 states have internal predecessors, (48), 3 states have call successors, (30), 1 states have call predecessors, (30), 3 states have return successors, (30), 4 states have call predecessors, (30), 3 states have call successors, (30)
[2025-05-07 17:24:06,691 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:06,692 INFO  L93              Difference]: Finished difference Result 161 states and 181 transitions.
[2025-05-07 17:24:06,692 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:24:06,692 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 16.0) internal successors, (48), 4 states have internal predecessors, (48), 3 states have call successors, (30), 1 states have call predecessors, (30), 3 states have return successors, (30), 4 states have call predecessors, (30), 3 states have call successors, (30) Word has length 108
[2025-05-07 17:24:06,693 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:06,693 INFO  L225             Difference]: With dead ends: 161
[2025-05-07 17:24:06,693 INFO  L226             Difference]: Without dead ends: 156
[2025-05-07 17:24:06,693 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:24:06,694 INFO  L437           NwaCegarLoop]: 178 mSDtfsCounter, 1 mSDsluCounter, 335 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 513 SdHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:06,694 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 513 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:06,694 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 156 states.
[2025-05-07 17:24:06,697 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 156 to 154.
[2025-05-07 17:24:06,698 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 154 states, 65 states have (on average 1.0307692307692307) internal successors, (67), 67 states have internal predecessors, (67), 48 states have call successors, (51), 40 states have call predecessors, (51), 40 states have return successors, (51), 46 states have call predecessors, (51), 48 states have call successors, (51)
[2025-05-07 17:24:06,698 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 154 states to 154 states and 169 transitions.
[2025-05-07 17:24:06,699 INFO  L79                 Accepts]: Start accepts. Automaton has 154 states and 169 transitions. Word has length 108
[2025-05-07 17:24:06,699 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:06,699 INFO  L485      AbstractCegarLoop]: Abstraction has 154 states and 169 transitions.
[2025-05-07 17:24:06,699 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 16.0) internal successors, (48), 4 states have internal predecessors, (48), 3 states have call successors, (30), 1 states have call predecessors, (30), 3 states have return successors, (30), 4 states have call predecessors, (30), 3 states have call successors, (30)
[2025-05-07 17:24:06,699 INFO  L278                IsEmpty]: Start isEmpty. Operand 154 states and 169 transitions.
[2025-05-07 17:24:06,700 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:24:06,700 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:06,700 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:24:06,700 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:24:06,700 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:06,701 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:06,701 INFO  L85        PathProgramCache]: Analyzing trace with hash -2001374079, now seen corresponding path program 1 times
[2025-05-07 17:24:06,701 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:06,701 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1219541296]
[2025-05-07 17:24:06,701 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:06,701 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:06,746 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:24:06,774 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:24:06,775 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:06,775 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:06,940 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:24:06,940 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:06,940 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1219541296]
[2025-05-07 17:24:06,940 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1219541296] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:06,940 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:06,940 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:24:06,940 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [820703564]
[2025-05-07 17:24:06,940 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:06,941 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:24:06,941 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:06,941 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:24:06,942 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:24:06,942 INFO  L87              Difference]: Start difference. First operand 154 states and 169 transitions. Second operand  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:24:06,994 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:06,994 INFO  L93              Difference]: Finished difference Result 162 states and 180 transitions.
[2025-05-07 17:24:06,995 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:24:06,995 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37) Word has length 133
[2025-05-07 17:24:06,996 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:06,997 INFO  L225             Difference]: With dead ends: 162
[2025-05-07 17:24:06,997 INFO  L226             Difference]: Without dead ends: 150
[2025-05-07 17:24:06,997 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:24:06,998 INFO  L437           NwaCegarLoop]: 175 mSDtfsCounter, 1 mSDsluCounter, 854 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1029 SdHoareTripleChecker+Invalid, 37 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:06,998 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1029 Invalid, 37 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:06,999 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 150 states.
[2025-05-07 17:24:07,003 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 150 to 150.
[2025-05-07 17:24:07,004 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 150 states, 63 states have (on average 1.0317460317460319) internal successors, (65), 65 states have internal predecessors, (65), 47 states have call successors, (49), 39 states have call predecessors, (49), 39 states have return successors, (49), 45 states have call predecessors, (49), 47 states have call successors, (49)
[2025-05-07 17:24:07,005 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 150 states to 150 states and 163 transitions.
[2025-05-07 17:24:07,005 INFO  L79                 Accepts]: Start accepts. Automaton has 150 states and 163 transitions. Word has length 133
[2025-05-07 17:24:07,006 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:07,006 INFO  L485      AbstractCegarLoop]: Abstraction has 150 states and 163 transitions.
[2025-05-07 17:24:07,006 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:24:07,006 INFO  L278                IsEmpty]: Start isEmpty. Operand 150 states and 163 transitions.
[2025-05-07 17:24:07,008 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:24:07,008 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:07,008 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:24:07,008 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:24:07,008 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:07,009 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:07,009 INFO  L85        PathProgramCache]: Analyzing trace with hash -521195942, now seen corresponding path program 1 times
[2025-05-07 17:24:07,009 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:07,009 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1025130278]
[2025-05-07 17:24:07,009 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:07,009 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:07,054 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:24:07,057 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:24:07,057 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:07,057 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:07,140 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:24:07,140 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:07,140 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1025130278]
[2025-05-07 17:24:07,140 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1025130278] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:07,140 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:07,140 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:24:07,140 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [243675205]
[2025-05-07 17:24:07,140 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:07,141 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:24:07,141 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:07,141 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:24:07,142 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:24:07,142 INFO  L87              Difference]: Start difference. First operand 150 states and 163 transitions. Second operand  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 3 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 3 states have call predecessors, (37), 3 states have call successors, (37)
[2025-05-07 17:24:07,151 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:07,151 INFO  L93              Difference]: Finished difference Result 152 states and 164 transitions.
[2025-05-07 17:24:07,152 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:24:07,152 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 3 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 3 states have call predecessors, (37), 3 states have call successors, (37) Word has length 133
[2025-05-07 17:24:07,152 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:07,153 INFO  L225             Difference]: With dead ends: 152
[2025-05-07 17:24:07,153 INFO  L226             Difference]: Without dead ends: 144
[2025-05-07 17:24:07,153 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:24:07,154 INFO  L437           NwaCegarLoop]: 164 mSDtfsCounter, 1 mSDsluCounter, 315 mSDsCounter, 0 mSdLazyCounter, 2 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 479 SdHoareTripleChecker+Invalid, 2 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 2 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:07,154 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 479 Invalid, 2 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 2 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:07,155 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 144 states.
[2025-05-07 17:24:07,159 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 144 to 144.
[2025-05-07 17:24:07,160 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 144 states, 63 states have (on average 1.0158730158730158) internal successors, (64), 64 states have internal predecessors, (64), 41 states have call successors, (43), 39 states have call predecessors, (43), 39 states have return successors, (43), 40 states have call predecessors, (43), 41 states have call successors, (43)
[2025-05-07 17:24:07,161 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 144 states to 144 states and 150 transitions.
[2025-05-07 17:24:07,161 INFO  L79                 Accepts]: Start accepts. Automaton has 144 states and 150 transitions. Word has length 133
[2025-05-07 17:24:07,161 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:07,162 INFO  L485      AbstractCegarLoop]: Abstraction has 144 states and 150 transitions.
[2025-05-07 17:24:07,162 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 3 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 3 states have call predecessors, (37), 3 states have call successors, (37)
[2025-05-07 17:24:07,162 INFO  L278                IsEmpty]: Start isEmpty. Operand 144 states and 150 transitions.
[2025-05-07 17:24:07,163 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:24:07,164 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:07,164 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:24:07,164 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:24:07,164 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:07,164 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:07,165 INFO  L85        PathProgramCache]: Analyzing trace with hash -1120583003, now seen corresponding path program 1 times
[2025-05-07 17:24:07,165 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:07,165 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [375153598]
[2025-05-07 17:24:07,165 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:07,165 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:07,211 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:24:07,239 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:24:07,239 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:07,239 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:08,126 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:24:08,126 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:08,126 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [375153598]
[2025-05-07 17:24:08,127 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [375153598] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:08,127 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:08,127 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [22] imperfect sequences [] total 22
[2025-05-07 17:24:08,127 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1209053733]
[2025-05-07 17:24:08,127 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:08,127 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-05-07 17:24:08,127 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:08,128 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-05-07 17:24:08,128 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=44, Invalid=418, Unknown=0, NotChecked=0, Total=462
[2025-05-07 17:24:08,129 INFO  L87              Difference]: Start difference. First operand 144 states and 150 transitions. Second operand  has 22 states, 15 states have (on average 3.933333333333333) internal successors, (59), 18 states have internal predecessors, (59), 10 states have call successors, (37), 1 states have call predecessors, (37), 15 states have return successors, (37), 17 states have call predecessors, (37), 10 states have call successors, (37)
[2025-05-07 17:24:08,465 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:08,465 INFO  L93              Difference]: Finished difference Result 149 states and 156 transitions.
[2025-05-07 17:24:08,466 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 22 states. 
[2025-05-07 17:24:08,466 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 15 states have (on average 3.933333333333333) internal successors, (59), 18 states have internal predecessors, (59), 10 states have call successors, (37), 1 states have call predecessors, (37), 15 states have return successors, (37), 17 states have call predecessors, (37), 10 states have call successors, (37) Word has length 133
[2025-05-07 17:24:08,466 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:08,467 INFO  L225             Difference]: With dead ends: 149
[2025-05-07 17:24:08,467 INFO  L226             Difference]: Without dead ends: 140
[2025-05-07 17:24:08,467 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 26 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 27 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=61, Invalid=589, Unknown=0, NotChecked=0, Total=650
[2025-05-07 17:24:08,468 INFO  L437           NwaCegarLoop]: 133 mSDtfsCounter, 6 mSDsluCounter, 2342 mSDsCounter, 0 mSdLazyCounter, 331 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 2475 SdHoareTripleChecker+Invalid, 338 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 331 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:08,468 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 2475 Invalid, 338 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 331 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-05-07 17:24:08,469 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 140 states.
[2025-05-07 17:24:08,472 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 140 to 140.
[2025-05-07 17:24:08,472 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 140 states, 61 states have (on average 1.0163934426229508) internal successors, (62), 62 states have internal predecessors, (62), 40 states have call successors, (41), 38 states have call predecessors, (41), 38 states have return successors, (41), 39 states have call predecessors, (41), 40 states have call successors, (41)
[2025-05-07 17:24:08,472 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 140 states to 140 states and 144 transitions.
[2025-05-07 17:24:08,473 INFO  L79                 Accepts]: Start accepts. Automaton has 140 states and 144 transitions. Word has length 133
[2025-05-07 17:24:08,473 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:08,473 INFO  L485      AbstractCegarLoop]: Abstraction has 140 states and 144 transitions.
[2025-05-07 17:24:08,473 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 15 states have (on average 3.933333333333333) internal successors, (59), 18 states have internal predecessors, (59), 10 states have call successors, (37), 1 states have call predecessors, (37), 15 states have return successors, (37), 17 states have call predecessors, (37), 10 states have call successors, (37)
[2025-05-07 17:24:08,473 INFO  L278                IsEmpty]: Start isEmpty. Operand 140 states and 144 transitions.
[2025-05-07 17:24:08,475 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:24:08,475 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:08,475 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:24:08,475 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:24:08,475 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:08,475 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:08,475 INFO  L85        PathProgramCache]: Analyzing trace with hash 1446380799, now seen corresponding path program 1 times
[2025-05-07 17:24:08,475 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:08,475 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [932019623]
[2025-05-07 17:24:08,475 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:08,475 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:08,527 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:24:08,553 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:24:08,553 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:08,553 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:08,652 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:24:08,653 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:08,653 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [932019623]
[2025-05-07 17:24:08,653 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [932019623] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:08,653 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:08,653 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:24:08,653 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [274300648]
[2025-05-07 17:24:08,653 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:08,653 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:24:08,653 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:08,654 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:24:08,654 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:24:08,654 INFO  L87              Difference]: Start difference. First operand 140 states and 144 transitions. Second operand  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 4 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:24:08,667 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:08,667 INFO  L93              Difference]: Finished difference Result 142 states and 145 transitions.
[2025-05-07 17:24:08,667 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:24:08,667 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 4 states have call predecessors, (37), 4 states have call successors, (37) Word has length 133
[2025-05-07 17:24:08,668 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:08,668 INFO  L225             Difference]: With dead ends: 142
[2025-05-07 17:24:08,668 INFO  L226             Difference]: Without dead ends: 138
[2025-05-07 17:24:08,668 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:24:08,669 INFO  L437           NwaCegarLoop]: 144 mSDtfsCounter, 1 mSDsluCounter, 273 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 417 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:08,669 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 417 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:08,669 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 138 states.
[2025-05-07 17:24:08,671 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 138 to 138.
[2025-05-07 17:24:08,671 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 138 states, 61 states have (on average 1.0) internal successors, (61), 61 states have internal predecessors, (61), 38 states have call successors, (39), 38 states have call predecessors, (39), 38 states have return successors, (39), 38 states have call predecessors, (39), 38 states have call successors, (39)
[2025-05-07 17:24:08,672 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 138 states to 138 states and 139 transitions.
[2025-05-07 17:24:08,672 INFO  L79                 Accepts]: Start accepts. Automaton has 138 states and 139 transitions. Word has length 133
[2025-05-07 17:24:08,672 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:08,672 INFO  L485      AbstractCegarLoop]: Abstraction has 138 states and 139 transitions.
[2025-05-07 17:24:08,672 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 19.666666666666668) internal successors, (59), 4 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 3 states have return successors, (37), 4 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:24:08,673 INFO  L278                IsEmpty]: Start isEmpty. Operand 138 states and 139 transitions.
[2025-05-07 17:24:08,673 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:24:08,673 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:08,674 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:24:08,674 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:24:08,674 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:08,674 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:08,674 INFO  L85        PathProgramCache]: Analyzing trace with hash 506106057, now seen corresponding path program 1 times
[2025-05-07 17:24:08,674 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:08,674 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1952284277]
[2025-05-07 17:24:08,674 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:08,675 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:08,716 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:24:08,737 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:24:08,738 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:08,738 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:08,858 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:24:08,858 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:08,858 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1952284277]
[2025-05-07 17:24:08,858 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1952284277] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:08,858 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:08,858 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:24:08,858 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1815849518]
[2025-05-07 17:24:08,858 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:08,859 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:24:08,859 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:08,859 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:24:08,860 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:24:08,860 INFO  L87              Difference]: Start difference. First operand 138 states and 139 transitions. Second operand  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:24:08,891 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:08,891 INFO  L93              Difference]: Finished difference Result 145 states and 146 transitions.
[2025-05-07 17:24:08,891 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:24:08,891 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37) Word has length 133
[2025-05-07 17:24:08,892 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:08,893 INFO  L225             Difference]: With dead ends: 145
[2025-05-07 17:24:08,893 INFO  L226             Difference]: Without dead ends: 134
[2025-05-07 17:24:08,893 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:24:08,893 INFO  L437           NwaCegarLoop]: 138 mSDtfsCounter, 1 mSDsluCounter, 678 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 816 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:08,893 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 816 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:08,894 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-05-07 17:24:08,896 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 134.
[2025-05-07 17:24:08,896 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 134 states, 59 states have (on average 1.0) internal successors, (59), 59 states have internal predecessors, (59), 37 states have call successors, (37), 37 states have call predecessors, (37), 37 states have return successors, (37), 37 states have call predecessors, (37), 37 states have call successors, (37)
[2025-05-07 17:24:08,896 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 134 states to 134 states and 133 transitions.
[2025-05-07 17:24:08,897 INFO  L79                 Accepts]: Start accepts. Automaton has 134 states and 133 transitions. Word has length 133
[2025-05-07 17:24:08,897 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:08,897 INFO  L485      AbstractCegarLoop]: Abstraction has 134 states and 133 transitions.
[2025-05-07 17:24:08,897 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 9.833333333333334) internal successors, (59), 7 states have internal predecessors, (59), 4 states have call successors, (37), 1 states have call predecessors, (37), 6 states have return successors, (37), 6 states have call predecessors, (37), 4 states have call successors, (37)
[2025-05-07 17:24:08,897 INFO  L278                IsEmpty]: Start isEmpty. Operand 134 states and 133 transitions.
[2025-05-07 17:24:08,898 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:24:08,898 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:24:08,898 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:24:08,898 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:24:08,898 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:24:08,899 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:24:08,899 INFO  L85        PathProgramCache]: Analyzing trace with hash 370645883, now seen corresponding path program 1 times
[2025-05-07 17:24:08,899 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:24:08,899 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1767781599]
[2025-05-07 17:24:08,899 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:24:08,899 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:24:08,942 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:24:08,962 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:24:08,962 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:24:08,962 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:24:09,175 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:24:09,175 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:24:09,175 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1767781599]
[2025-05-07 17:24:09,176 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1767781599] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:24:09,176 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:24:09,176 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:24:09,176 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [609440446]
[2025-05-07 17:24:09,176 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:24:09,176 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:24:09,176 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:24:09,177 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:24:09,177 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:24:09,177 INFO  L87              Difference]: Start difference. First operand 134 states and 133 transitions. Second operand  has 7 states, 5 states have (on average 11.8) internal successors, (59), 7 states have internal predecessors, (59), 5 states have call successors, (37), 1 states have call predecessors, (37), 5 states have return successors, (37), 6 states have call predecessors, (37), 5 states have call successors, (37)
[2025-05-07 17:24:09,199 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:24:09,199 INFO  L93              Difference]: Finished difference Result 120 states and 119 transitions.
[2025-05-07 17:24:09,199 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:24:09,199 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 11.8) internal successors, (59), 7 states have internal predecessors, (59), 5 states have call successors, (37), 1 states have call predecessors, (37), 5 states have return successors, (37), 6 states have call predecessors, (37), 5 states have call successors, (37) Word has length 133
[2025-05-07 17:24:09,199 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:24:09,200 INFO  L225             Difference]: With dead ends: 120
[2025-05-07 17:24:09,200 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:24:09,200 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:24:09,200 INFO  L437           NwaCegarLoop]: 117 mSDtfsCounter, 0 mSDsluCounter, 456 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 573 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:24:09,200 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 573 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:24:09,200 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:24:09,201 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:24:09,201 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:24:09,201 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:24:09,201 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 133
[2025-05-07 17:24:09,201 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:24:09,201 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:24:09,201 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 11.8) internal successors, (59), 7 states have internal predecessors, (59), 5 states have call successors, (37), 1 states have call predecessors, (37), 5 states have return successors, (37), 6 states have call predecessors, (37), 5 states have call successors, (37)
[2025-05-07 17:24:09,201 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:24:09,201 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:24:09,203 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:24:09,204 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:24:09,206 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:24:09,207 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:24:09,210 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:24:09 BoogieIcfgContainer
[2025-05-07 17:24:09,210 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:24:09,210 INFO  L158              Benchmark]: Toolchain (without parser) took 5076.79ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 133.9MB in the beginning and 85.0MB in the end (delta: 49.0MB). Peak memory consumption was 104.3MB. Max. memory is 33.6GB.
[2025-05-07 17:24:09,210 INFO  L158              Benchmark]: SmtParser took 0.25ms. Allocated memory is still 234.9MB. Free memory is still 173.1MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:24:09,211 INFO  L158              Benchmark]: ChcToBoogie took 50.50ms. Allocated memory is still 234.9MB. Free memory was 133.9MB in the beginning and 129.9MB in the end (delta: 4.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:24:09,211 INFO  L158              Benchmark]: Boogie Preprocessor took 80.90ms. Allocated memory is still 234.9MB. Free memory was 129.9MB in the beginning and 125.8MB in the end (delta: 4.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:24:09,211 INFO  L158              Benchmark]: RCFGBuilder took 562.04ms. Allocated memory is still 234.9MB. Free memory was 125.8MB in the beginning and 133.8MB in the end (delta: -8.0MB). Peak memory consumption was 24.7MB. Max. memory is 33.6GB.
[2025-05-07 17:24:09,211 INFO  L158              Benchmark]: TraceAbstraction took 4379.36ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 133.0MB in the beginning and 85.0MB in the end (delta: 48.0MB). Peak memory consumption was 96.4MB. Max. memory is 33.6GB.
[2025-05-07 17:24:09,212 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.25ms. Allocated memory is still 234.9MB. Free memory is still 173.1MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 50.50ms. Allocated memory is still 234.9MB. Free memory was 133.9MB in the beginning and 129.9MB in the end (delta: 4.0MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 80.90ms. Allocated memory is still 234.9MB. Free memory was 129.9MB in the beginning and 125.8MB in the end (delta: 4.1MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 562.04ms. Allocated memory is still 234.9MB. Free memory was 125.8MB in the beginning and 133.8MB in the end (delta: -8.0MB). Peak memory consumption was 24.7MB. Max. memory is 33.6GB.
 * TraceAbstraction took 4379.36ms. Allocated memory was 234.9MB in the beginning and 285.2MB in the end (delta: 50.3MB). Free memory was 133.0MB in the beginning and 85.0MB in the end (delta: 48.0MB). Peak memory consumption was 96.4MB. 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 41 procedures, 176 locations, 289 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 4.3s, OverallIterations: 13, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 77 SdHoareTripleChecker+Valid, 0.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 14 mSDsluCounter, 11467 SdHoareTripleChecker+Invalid, 0.6s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 9244 mSDsCounter, 19 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 580 IncrementalHoareTripleChecker+Invalid, 599 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 19 mSolverCounterUnsat, 2223 mSDtfsCounter, 580 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 92 GetRequests, 26 SyntacticMatches, 0 SemanticMatches, 66 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 28 ImplicationChecksByTransitivity, 0.4s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=176occurred in iteration=0, InterpolantAutomatonStates: 88, 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, 13 MinimizatonAttempts, 8 StatesRemovedByMinimization, 4 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.3s SatisfiabilityAnalysisTime, 2.4s InterpolantComputationTime, 1329 NumberOfCodeBlocks, 1329 NumberOfCodeBlocksAsserted, 13 NumberOfCheckSat, 1316 ConstructedInterpolants, 0 QuantifiedInterpolants, 1651 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 13 InterpolantComputations, 13 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-05-07 17:24:09,223 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
