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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:25:09,594 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:25:09,631 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_113e181a-7dd3-42ff-8897-ea0d5601037b/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:25:09,634 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:25:09,634 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:25:09,647 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:25:09,648 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:25:09,648 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:25:09,648 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:25:09,648 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:25:09,648 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:25:09,648 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:25:09,648 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:25:09,649 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:25:09,649 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:25:09,649 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:25:09,649 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:25:09,649 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:25:09,649 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:09,649 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:25:09,649 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:25:09,649 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:25:09,649 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:25:09,649 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:25:09,649 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:25:09,650 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:25:09,650 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:25:09,830 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:25:09,836 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:25:09,837 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:25:09,838 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:25:09,839 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:25:09,839 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_113e181a-7dd3-42ff-8897-ea0d5601037b/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol_0_no_adts_000.smt2
[2025-05-07 17:25:09,840 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:25:09,843 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:25:10,138 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_113e181a-7dd3-42ff-8897-ea0d5601037b/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/inheritance/constructor_hierarchy_base_calls_with_side_effects_1.sol_0_no_adts_000.smt2
[2025-05-07 17:25:10,141 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:25:10,141 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:25:10,142 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:25:10,142 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:25:10,142 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:25:10,145 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,193 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10 Unit
[2025-05-07 17:25:10,193 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:25:10,194 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:25:10,194 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:25:10,194 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:25:10,205 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,205 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,228 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,228 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,234 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,235 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,237 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,239 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,241 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,253 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:25:10,254 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:25:10,254 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:25:10,254 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:25:10,255 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (1/1) ...
[2025-05-07 17:25:10,257 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:10,266 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:10,274 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:25:10,276 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:25:10,284 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:25:10,284 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:25:10,284 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:25:10,284 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_4_0 given in one single declaration
[2025-05-07 17:25:10,284 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_4_0
[2025-05-07 17:25:10,284 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_4_0
[2025-05-07 17:25:10,284 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_17_C_90_0 given in one single declaration
[2025-05-07 17:25:10,284 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_17_C_90_0
[2025-05-07 17:25:10,284 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_17_C_90_0
[2025-05-07 17:25:10,284 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_71_C_90_0 given in one single declaration
[2025-05-07 17:25:10,284 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_71_C_90_0
[2025-05-07 17:25:10,284 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_71_C_90_0
[2025-05-07 17:25:10,285 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_22_constructor_89_90_0 given in one single declaration
[2025-05-07 17:25:10,285 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_22_constructor_89_90_0
[2025-05-07 17:25:10,285 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_22_constructor_89_90_0
[2025-05-07 17:25:10,285 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_69_constructor_89_90_0 given in one single declaration
[2025-05-07 17:25:10,285 INFO  L130     BoogieDeclarations]: Found specification of procedure block_69_constructor_89_90_0
[2025-05-07 17:25:10,285 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_69_constructor_89_90_0
[2025-05-07 17:25:10,285 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_66__88_90_0 given in one single declaration
[2025-05-07 17:25:10,285 INFO  L130     BoogieDeclarations]: Found specification of procedure block_66__88_90_0
[2025-05-07 17:25:10,285 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_66__88_90_0
[2025-05-07 17:25:10,285 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_65_constructor_89_90_0 given in one single declaration
[2025-05-07 17:25:10,285 INFO  L130     BoogieDeclarations]: Found specification of procedure block_65_constructor_89_90_0
[2025-05-07 17:25:10,286 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_65_constructor_89_90_0
[2025-05-07 17:25:10,286 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_70_constructor_89_90_0 given in one single declaration
[2025-05-07 17:25:10,286 INFO  L130     BoogieDeclarations]: Found specification of procedure block_70_constructor_89_90_0
[2025-05-07 17:25:10,286 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_70_constructor_89_90_0
[2025-05-07 17:25:10,286 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_68_constructor_89_90_0 given in one single declaration
[2025-05-07 17:25:10,286 INFO  L130     BoogieDeclarations]: Found specification of procedure block_68_constructor_89_90_0
[2025-05-07 17:25:10,286 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_68_constructor_89_90_0
[2025-05-07 17:25:10,286 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_67_return_constructor_89_90_0 given in one single declaration
[2025-05-07 17:25:10,286 INFO  L130     BoogieDeclarations]: Found specification of procedure block_67_return_constructor_89_90_0
[2025-05-07 17:25:10,286 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_67_return_constructor_89_90_0
[2025-05-07 17:25:10,287 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:25:10,287 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_73_C_90_0
[2025-05-07 17:25:10,287 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_73_C_90_0
[2025-05-07 17:25:10,287 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_72_C_90_0 given in one single declaration
[2025-05-07 17:25:10,287 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_72_C_90_0
[2025-05-07 17:25:10,287 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_72_C_90_0
[2025-05-07 17:25:10,287 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_77_B_42_0 given in one single declaration
[2025-05-07 17:25:10,287 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_77_B_42_0
[2025-05-07 17:25:10,287 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_77_B_42_0
[2025-05-07 17:25:10,287 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_19_constructor_27_90_0 given in one single declaration
[2025-05-07 17:25:10,287 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_19_constructor_27_90_0
[2025-05-07 17:25:10,287 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_19_constructor_27_90_0
[2025-05-07 17:25:10,288 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_76_return_constructor_27_90_0 given in one single declaration
[2025-05-07 17:25:10,288 INFO  L130     BoogieDeclarations]: Found specification of procedure block_76_return_constructor_27_90_0
[2025-05-07 17:25:10,288 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_76_return_constructor_27_90_0
[2025-05-07 17:25:10,288 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_75__26_90_0 given in one single declaration
[2025-05-07 17:25:10,288 INFO  L130     BoogieDeclarations]: Found specification of procedure block_75__26_90_0
[2025-05-07 17:25:10,288 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_75__26_90_0
[2025-05-07 17:25:10,288 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_74_constructor_27_90_0 given in one single declaration
[2025-05-07 17:25:10,288 INFO  L130     BoogieDeclarations]: Found specification of procedure block_74_constructor_27_90_0
[2025-05-07 17:25:10,288 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_74_constructor_27_90_0
[2025-05-07 17:25:10,288 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:25:10,288 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_79_B_42_0
[2025-05-07 17:25:10,288 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_79_B_42_0
[2025-05-07 17:25:10,289 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_78_B_42_0 given in one single declaration
[2025-05-07 17:25:10,289 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_78_B_42_0
[2025-05-07 17:25:10,289 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_78_B_42_0
[2025-05-07 17:25:10,289 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_83_Z_57_0 given in one single declaration
[2025-05-07 17:25:10,289 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_83_Z_57_0
[2025-05-07 17:25:10,289 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_83_Z_57_0
[2025-05-07 17:25:10,289 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_21_constructor_56_90_0 given in one single declaration
[2025-05-07 17:25:10,289 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_21_constructor_56_90_0
[2025-05-07 17:25:10,289 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_21_constructor_56_90_0
[2025-05-07 17:25:10,289 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_82_return_constructor_56_90_0 given in one single declaration
[2025-05-07 17:25:10,289 INFO  L130     BoogieDeclarations]: Found specification of procedure block_82_return_constructor_56_90_0
[2025-05-07 17:25:10,289 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_82_return_constructor_56_90_0
[2025-05-07 17:25:10,289 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_81__55_90_0 given in one single declaration
[2025-05-07 17:25:10,289 INFO  L130     BoogieDeclarations]: Found specification of procedure block_81__55_90_0
[2025-05-07 17:25:10,290 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_81__55_90_0
[2025-05-07 17:25:10,290 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_80_constructor_56_90_0 given in one single declaration
[2025-05-07 17:25:10,290 INFO  L130     BoogieDeclarations]: Found specification of procedure block_80_constructor_56_90_0
[2025-05-07 17:25:10,290 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_80_constructor_56_90_0
[2025-05-07 17:25:10,290 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:25:10,290 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_85_Z_57_0
[2025-05-07 17:25:10,290 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_85_Z_57_0
[2025-05-07 17:25:10,290 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_84_Z_57_0 given in one single declaration
[2025-05-07 17:25:10,290 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_84_Z_57_0
[2025-05-07 17:25:10,290 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_84_Z_57_0
[2025-05-07 17:25:10,290 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_89_A_13_0 given in one single declaration
[2025-05-07 17:25:10,290 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_89_A_13_0
[2025-05-07 17:25:10,290 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_89_A_13_0
[2025-05-07 17:25:10,290 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:25:10,290 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_91_A_13_0
[2025-05-07 17:25:10,291 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_91_A_13_0
[2025-05-07 17:25:10,291 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_90_A_13_0 given in one single declaration
[2025-05-07 17:25:10,291 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_90_A_13_0
[2025-05-07 17:25:10,291 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_90_A_13_0
[2025-05-07 17:25:10,291 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_18_constructor_12_90_0 given in one single declaration
[2025-05-07 17:25:10,291 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_18_constructor_12_90_0
[2025-05-07 17:25:10,291 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_18_constructor_12_90_0
[2025-05-07 17:25:10,291 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_88_return_constructor_12_90_0 given in one single declaration
[2025-05-07 17:25:10,291 INFO  L130     BoogieDeclarations]: Found specification of procedure block_88_return_constructor_12_90_0
[2025-05-07 17:25:10,291 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_88_return_constructor_12_90_0
[2025-05-07 17:25:10,291 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_87__11_90_0 given in one single declaration
[2025-05-07 17:25:10,291 INFO  L130     BoogieDeclarations]: Found specification of procedure block_87__11_90_0
[2025-05-07 17:25:10,291 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_87__11_90_0
[2025-05-07 17:25:10,291 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_86_constructor_12_90_0 given in one single declaration
[2025-05-07 17:25:10,291 INFO  L130     BoogieDeclarations]: Found specification of procedure block_86_constructor_12_90_0
[2025-05-07 17:25:10,291 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_86_constructor_12_90_0
[2025-05-07 17:25:10,291 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_93_function_f__41_90_0 given in one single declaration
[2025-05-07 17:25:10,291 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_93_function_f__41_90_0
[2025-05-07 17:25:10,291 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_93_function_f__41_90_0
[2025-05-07 17:25:10,291 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_20_function_f__41_90_0 given in one single declaration
[2025-05-07 17:25:10,291 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_20_function_f__41_90_0
[2025-05-07 17:25:10,291 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_20_function_f__41_90_0
[2025-05-07 17:25:10,292 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:25:10,292 INFO  L130     BoogieDeclarations]: Found specification of procedure block_63_return_function_f__41_90_0
[2025-05-07 17:25:10,292 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_63_return_function_f__41_90_0
[2025-05-07 17:25:10,292 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_62_f_40_90_0 given in one single declaration
[2025-05-07 17:25:10,292 INFO  L130     BoogieDeclarations]: Found specification of procedure block_62_f_40_90_0
[2025-05-07 17:25:10,292 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_62_f_40_90_0
[2025-05-07 17:25:10,292 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_61_function_f__41_90_0 given in one single declaration
[2025-05-07 17:25:10,292 INFO  L130     BoogieDeclarations]: Found specification of procedure block_61_function_f__41_90_0
[2025-05-07 17:25:10,292 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_61_function_f__41_90_0
[2025-05-07 17:25:10,292 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_92_C_90_0 given in one single declaration
[2025-05-07 17:25:10,292 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_92_C_90_0
[2025-05-07 17:25:10,292 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_92_C_90_0
[2025-05-07 17:25:10,292 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:25:10,292 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:25:10,292 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:25:10,501 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:25:10,503 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:25:10,790 INFO  L?                        ?]: Removed 407 outVars from TransFormulas that were not future-live.
[2025-05-07 17:25:10,790 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:25:10,799 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:25:10,800 INFO  L312             CfgBuilder]: Removed 19 assume(true) statements.
[2025-05-07 17:25:10,800 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:10 BoogieIcfgContainer
[2025-05-07 17:25:10,800 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:25:10,801 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:25:10,802 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:25:10,804 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:25:10,804 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:10" (1/3) ...
[2025-05-07 17:25:10,805 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4597efc3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:25:10, skipping insertion in model container
[2025-05-07 17:25:10,805 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:10" (2/3) ...
[2025-05-07 17:25:10,805 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4597efc3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:25:10, skipping insertion in model container
[2025-05-07 17:25:10,805 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:10" (3/3) ...
[2025-05-07 17:25:10,806 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:25:10,816 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:25:10,818 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:25:10,848 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:25:10,855 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;@4d038171, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:25:10,855 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:25:10,859 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:25:10,867 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-05-07 17:25:10,867 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:10,867 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:25:10,868 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:10,871 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:10,871 INFO  L85        PathProgramCache]: Analyzing trace with hash -1457354636, now seen corresponding path program 1 times
[2025-05-07 17:25:10,876 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:10,876 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1252945925]
[2025-05-07 17:25:10,877 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:10,877 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:10,920 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-05-07 17:25:10,969 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-05-07 17:25:10,970 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:10,970 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:11,171 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:25:11,171 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:11,171 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1252945925]
[2025-05-07 17:25:11,172 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1252945925] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:11,172 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:11,175 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:25:11,176 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2061170584]
[2025-05-07 17:25:11,177 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:11,181 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:25:11,181 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:11,211 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:25:11,211 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:11,214 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:25:11,365 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:11,366 INFO  L93              Difference]: Finished difference Result 176 states and 217 transitions.
[2025-05-07 17:25:11,367 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:25:11,368 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:25:11,369 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:11,377 INFO  L225             Difference]: With dead ends: 176
[2025-05-07 17:25:11,377 INFO  L226             Difference]: Without dead ends: 174
[2025-05-07 17:25:11,379 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:25:11,381 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:25:11,383 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:25:11,393 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 174 states.
[2025-05-07 17:25:11,415 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 174 to 172.
[2025-05-07 17:25:11,416 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:25:11,422 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 172 states to 172 states and 211 transitions.
[2025-05-07 17:25:11,423 INFO  L79                 Accepts]: Start accepts. Automaton has 172 states and 211 transitions. Word has length 33
[2025-05-07 17:25:11,424 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:11,424 INFO  L485      AbstractCegarLoop]: Abstraction has 172 states and 211 transitions.
[2025-05-07 17:25:11,424 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:25:11,424 INFO  L278                IsEmpty]: Start isEmpty. Operand 172 states and 211 transitions.
[2025-05-07 17:25:11,426 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:25:11,427 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:11,427 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:25:11,427 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:25:11,427 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:11,428 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:11,428 INFO  L85        PathProgramCache]: Analyzing trace with hash -427637684, now seen corresponding path program 1 times
[2025-05-07 17:25:11,428 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:11,428 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2090945749]
[2025-05-07 17:25:11,428 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:11,428 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:11,467 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:25:11,499 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:25:11,500 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:11,500 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:11,602 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:25:11,602 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:11,603 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2090945749]
[2025-05-07 17:25:11,603 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2090945749] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:11,603 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:11,603 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:11,603 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [369385349]
[2025-05-07 17:25:11,603 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:11,604 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:11,604 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:11,604 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:11,605 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:11,605 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:25:11,653 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:11,653 INFO  L93              Difference]: Finished difference Result 171 states and 208 transitions.
[2025-05-07 17:25:11,654 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:11,654 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:25:11,654 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:11,655 INFO  L225             Difference]: With dead ends: 171
[2025-05-07 17:25:11,655 INFO  L226             Difference]: Without dead ends: 170
[2025-05-07 17:25:11,656 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:25:11,656 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:25:11,656 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:25:11,657 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 170 states.
[2025-05-07 17:25:11,663 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 170 to 170.
[2025-05-07 17:25:11,664 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:25:11,665 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 170 states to 170 states and 206 transitions.
[2025-05-07 17:25:11,665 INFO  L79                 Accepts]: Start accepts. Automaton has 170 states and 206 transitions. Word has length 58
[2025-05-07 17:25:11,666 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:11,666 INFO  L485      AbstractCegarLoop]: Abstraction has 170 states and 206 transitions.
[2025-05-07 17:25:11,666 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:25:11,666 INFO  L278                IsEmpty]: Start isEmpty. Operand 170 states and 206 transitions.
[2025-05-07 17:25:11,667 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 59
[2025-05-07 17:25:11,667 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:11,667 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:25:11,668 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:25:11,668 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:11,668 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:11,668 INFO  L85        PathProgramCache]: Analyzing trace with hash 1481465928, now seen corresponding path program 1 times
[2025-05-07 17:25:11,668 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:11,668 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1596851049]
[2025-05-07 17:25:11,668 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:11,668 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:11,690 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 58 statements into 1 equivalence classes.
[2025-05-07 17:25:11,697 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 58 of 58 statements.
[2025-05-07 17:25:11,697 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:11,697 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:11,767 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:25:11,767 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:11,767 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1596851049]
[2025-05-07 17:25:11,767 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1596851049] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:11,767 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:11,767 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:11,767 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2068965404]
[2025-05-07 17:25:11,767 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:11,768 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:11,768 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:11,768 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:11,768 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:11,769 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:25:11,822 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:11,822 INFO  L93              Difference]: Finished difference Result 171 states and 205 transitions.
[2025-05-07 17:25:11,822 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:11,823 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:25:11,823 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:11,824 INFO  L225             Difference]: With dead ends: 171
[2025-05-07 17:25:11,824 INFO  L226             Difference]: Without dead ends: 169
[2025-05-07 17:25:11,825 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:25:11,825 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:25:11,825 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:25:11,826 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 169 states.
[2025-05-07 17:25:11,835 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 169 to 167.
[2025-05-07 17:25:11,836 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:25:11,838 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 167 states to 167 states and 199 transitions.
[2025-05-07 17:25:11,838 INFO  L79                 Accepts]: Start accepts. Automaton has 167 states and 199 transitions. Word has length 58
[2025-05-07 17:25:11,838 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:11,838 INFO  L485      AbstractCegarLoop]: Abstraction has 167 states and 199 transitions.
[2025-05-07 17:25:11,839 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:25:11,839 INFO  L278                IsEmpty]: Start isEmpty. Operand 167 states and 199 transitions.
[2025-05-07 17:25:11,841 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:25:11,841 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:11,841 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:25:11,841 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:25:11,842 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:11,842 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:11,842 INFO  L85        PathProgramCache]: Analyzing trace with hash -1635782897, now seen corresponding path program 1 times
[2025-05-07 17:25:11,842 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:11,842 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1977767790]
[2025-05-07 17:25:11,842 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:11,842 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:11,880 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:25:11,912 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:25:11,912 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:11,912 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:12,032 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:25:12,032 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:12,032 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1977767790]
[2025-05-07 17:25:12,032 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1977767790] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:12,032 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:12,032 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:12,032 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [692562299]
[2025-05-07 17:25:12,032 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:12,033 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:12,033 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:12,034 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:12,034 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:12,034 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:25:12,074 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:12,074 INFO  L93              Difference]: Finished difference Result 167 states and 198 transitions.
[2025-05-07 17:25:12,074 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:12,074 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:25:12,075 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:12,076 INFO  L225             Difference]: With dead ends: 167
[2025-05-07 17:25:12,076 INFO  L226             Difference]: Without dead ends: 165
[2025-05-07 17:25:12,076 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:25:12,076 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:25:12,076 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:25:12,077 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 165 states.
[2025-05-07 17:25:12,082 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 165 to 165.
[2025-05-07 17:25:12,082 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:25:12,083 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 165 states to 165 states and 194 transitions.
[2025-05-07 17:25:12,083 INFO  L79                 Accepts]: Start accepts. Automaton has 165 states and 194 transitions. Word has length 83
[2025-05-07 17:25:12,084 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:12,084 INFO  L485      AbstractCegarLoop]: Abstraction has 165 states and 194 transitions.
[2025-05-07 17:25:12,084 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:25:12,084 INFO  L278                IsEmpty]: Start isEmpty. Operand 165 states and 194 transitions.
[2025-05-07 17:25:12,085 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 84
[2025-05-07 17:25:12,085 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:12,085 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:25:12,085 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:25:12,085 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:12,085 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:12,086 INFO  L85        PathProgramCache]: Analyzing trace with hash -557309045, now seen corresponding path program 1 times
[2025-05-07 17:25:12,086 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:12,086 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1586897988]
[2025-05-07 17:25:12,086 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:12,086 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:12,118 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 83 statements into 1 equivalence classes.
[2025-05-07 17:25:12,134 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 83 of 83 statements.
[2025-05-07 17:25:12,134 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:12,134 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:12,195 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:25:12,195 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:12,195 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1586897988]
[2025-05-07 17:25:12,195 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1586897988] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:12,195 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:12,195 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:12,195 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2061424519]
[2025-05-07 17:25:12,195 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:12,196 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:12,196 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:12,196 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:12,196 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:12,196 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:25:12,240 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:12,241 INFO  L93              Difference]: Finished difference Result 167 states and 195 transitions.
[2025-05-07 17:25:12,241 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:12,241 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:25:12,242 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:12,243 INFO  L225             Difference]: With dead ends: 167
[2025-05-07 17:25:12,243 INFO  L226             Difference]: Without dead ends: 163
[2025-05-07 17:25:12,243 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:25:12,244 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:25:12,244 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:25:12,245 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 163 states.
[2025-05-07 17:25:12,252 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 163 to 161.
[2025-05-07 17:25:12,252 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:25:12,253 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 161 states to 161 states and 185 transitions.
[2025-05-07 17:25:12,254 INFO  L79                 Accepts]: Start accepts. Automaton has 161 states and 185 transitions. Word has length 83
[2025-05-07 17:25:12,254 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:12,254 INFO  L485      AbstractCegarLoop]: Abstraction has 161 states and 185 transitions.
[2025-05-07 17:25:12,254 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:25:12,254 INFO  L278                IsEmpty]: Start isEmpty. Operand 161 states and 185 transitions.
[2025-05-07 17:25:12,256 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 109
[2025-05-07 17:25:12,256 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:12,256 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:25:12,256 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:25:12,256 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:12,256 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:12,257 INFO  L85        PathProgramCache]: Analyzing trace with hash 1937726332, now seen corresponding path program 1 times
[2025-05-07 17:25:12,257 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:12,257 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [343644388]
[2025-05-07 17:25:12,257 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:12,257 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:12,290 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 108 statements into 1 equivalence classes.
[2025-05-07 17:25:12,311 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 108 of 108 statements.
[2025-05-07 17:25:12,311 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:12,312 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:12,440 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:25:12,440 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:12,440 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [343644388]
[2025-05-07 17:25:12,440 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [343644388] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:12,440 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:12,441 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-05-07 17:25:12,441 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [929455794]
[2025-05-07 17:25:12,441 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:12,441 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:12,441 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:12,442 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:12,442 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:12,442 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:25:12,482 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:12,482 INFO  L93              Difference]: Finished difference Result 161 states and 184 transitions.
[2025-05-07 17:25:12,482 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:12,482 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:25:12,483 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:12,484 INFO  L225             Difference]: With dead ends: 161
[2025-05-07 17:25:12,484 INFO  L226             Difference]: Without dead ends: 159
[2025-05-07 17:25:12,484 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:25:12,485 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:25:12,485 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:25:12,486 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 159 states.
[2025-05-07 17:25:12,491 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 159 to 159.
[2025-05-07 17:25:12,492 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:25:12,493 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 159 states to 159 states and 180 transitions.
[2025-05-07 17:25:12,493 INFO  L79                 Accepts]: Start accepts. Automaton has 159 states and 180 transitions. Word has length 108
[2025-05-07 17:25:12,493 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:12,493 INFO  L485      AbstractCegarLoop]: Abstraction has 159 states and 180 transitions.
[2025-05-07 17:25:12,493 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:25:12,493 INFO  L278                IsEmpty]: Start isEmpty. Operand 159 states and 180 transitions.
[2025-05-07 17:25:12,495 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 109
[2025-05-07 17:25:12,495 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:12,495 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:25:12,495 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:25:12,495 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:12,496 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:12,496 INFO  L85        PathProgramCache]: Analyzing trace with hash 859252480, now seen corresponding path program 1 times
[2025-05-07 17:25:12,496 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:12,496 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1994017015]
[2025-05-07 17:25:12,496 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:12,496 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:12,527 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 108 statements into 1 equivalence classes.
[2025-05-07 17:25:12,541 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 108 of 108 statements.
[2025-05-07 17:25:12,541 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:12,541 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:12,610 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:25:12,610 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:12,610 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1994017015]
[2025-05-07 17:25:12,610 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1994017015] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:12,610 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:12,610 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:12,610 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1985542403]
[2025-05-07 17:25:12,610 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:12,611 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:12,611 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:12,611 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:12,611 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:12,612 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:25:12,644 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:12,645 INFO  L93              Difference]: Finished difference Result 161 states and 181 transitions.
[2025-05-07 17:25:12,645 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:12,645 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:25:12,646 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:12,647 INFO  L225             Difference]: With dead ends: 161
[2025-05-07 17:25:12,647 INFO  L226             Difference]: Without dead ends: 156
[2025-05-07 17:25:12,647 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:25:12,647 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:25:12,648 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:25:12,649 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 156 states.
[2025-05-07 17:25:12,653 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 156 to 154.
[2025-05-07 17:25:12,654 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:25:12,655 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 154 states to 154 states and 169 transitions.
[2025-05-07 17:25:12,655 INFO  L79                 Accepts]: Start accepts. Automaton has 154 states and 169 transitions. Word has length 108
[2025-05-07 17:25:12,655 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:12,655 INFO  L485      AbstractCegarLoop]: Abstraction has 154 states and 169 transitions.
[2025-05-07 17:25:12,655 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:25:12,655 INFO  L278                IsEmpty]: Start isEmpty. Operand 154 states and 169 transitions.
[2025-05-07 17:25:12,656 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:25:12,657 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:12,657 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:25:12,657 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:25:12,657 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:12,657 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:12,657 INFO  L85        PathProgramCache]: Analyzing trace with hash 1324281021, now seen corresponding path program 1 times
[2025-05-07 17:25:12,657 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:12,657 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1680172137]
[2025-05-07 17:25:12,657 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:12,657 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:12,696 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:25:12,723 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:25:12,724 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:12,724 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:12,872 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:25:12,872 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:12,872 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1680172137]
[2025-05-07 17:25:12,872 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1680172137] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:12,872 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:12,872 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:25:12,872 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [537445692]
[2025-05-07 17:25:12,872 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:12,872 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:25:12,873 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:12,873 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:25:12,873 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:12,873 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:25:12,926 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:12,926 INFO  L93              Difference]: Finished difference Result 162 states and 180 transitions.
[2025-05-07 17:25:12,927 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:25:12,927 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:25:12,927 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:12,928 INFO  L225             Difference]: With dead ends: 162
[2025-05-07 17:25:12,928 INFO  L226             Difference]: Without dead ends: 150
[2025-05-07 17:25:12,929 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:25:12,929 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:25:12,929 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:25:12,930 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 150 states.
[2025-05-07 17:25:12,935 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 150 to 150.
[2025-05-07 17:25:12,935 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:25:12,936 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 150 states to 150 states and 163 transitions.
[2025-05-07 17:25:12,936 INFO  L79                 Accepts]: Start accepts. Automaton has 150 states and 163 transitions. Word has length 133
[2025-05-07 17:25:12,937 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:12,937 INFO  L485      AbstractCegarLoop]: Abstraction has 150 states and 163 transitions.
[2025-05-07 17:25:12,938 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:25:12,938 INFO  L278                IsEmpty]: Start isEmpty. Operand 150 states and 163 transitions.
[2025-05-07 17:25:12,939 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:25:12,939 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:12,939 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:25:12,940 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:25:12,940 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:12,940 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:12,940 INFO  L85        PathProgramCache]: Analyzing trace with hash 237495356, now seen corresponding path program 1 times
[2025-05-07 17:25:12,940 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:12,940 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [991022809]
[2025-05-07 17:25:12,940 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:12,941 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:12,994 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:25:12,998 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:25:12,998 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:12,998 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:13,090 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:25:13,090 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:13,090 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [991022809]
[2025-05-07 17:25:13,090 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [991022809] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:13,090 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:13,090 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:13,090 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1277719642]
[2025-05-07 17:25:13,090 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:13,091 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:13,091 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:13,091 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:13,091 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:13,091 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:25:13,099 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:13,099 INFO  L93              Difference]: Finished difference Result 152 states and 164 transitions.
[2025-05-07 17:25:13,100 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:13,100 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:25:13,100 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:13,101 INFO  L225             Difference]: With dead ends: 152
[2025-05-07 17:25:13,101 INFO  L226             Difference]: Without dead ends: 144
[2025-05-07 17:25:13,101 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:25:13,101 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:25:13,101 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:25:13,102 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 144 states.
[2025-05-07 17:25:13,105 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 144 to 144.
[2025-05-07 17:25:13,105 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:25:13,106 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 144 states to 144 states and 150 transitions.
[2025-05-07 17:25:13,106 INFO  L79                 Accepts]: Start accepts. Automaton has 144 states and 150 transitions. Word has length 133
[2025-05-07 17:25:13,106 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:13,106 INFO  L485      AbstractCegarLoop]: Abstraction has 144 states and 150 transitions.
[2025-05-07 17:25:13,106 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:25:13,106 INFO  L278                IsEmpty]: Start isEmpty. Operand 144 states and 150 transitions.
[2025-05-07 17:25:13,107 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:25:13,107 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:13,107 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:25:13,107 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:25:13,107 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:13,108 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:13,108 INFO  L85        PathProgramCache]: Analyzing trace with hash -598666313, now seen corresponding path program 1 times
[2025-05-07 17:25:13,108 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:13,108 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1905284144]
[2025-05-07 17:25:13,108 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:13,108 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:13,157 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:25:13,191 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:25:13,191 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:13,191 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:13,402 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:25:13,402 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:13,403 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1905284144]
[2025-05-07 17:25:13,403 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1905284144] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:13,403 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:13,403 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:25:13,403 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1144541858]
[2025-05-07 17:25:13,403 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:13,403 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:25:13,403 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:13,403 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:25:13,403 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:13,404 INFO  L87              Difference]: Start difference. First operand 144 states and 150 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:25:13,462 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:13,462 INFO  L93              Difference]: Finished difference Result 148 states and 154 transitions.
[2025-05-07 17:25:13,462 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:25:13,462 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:25:13,463 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:13,463 INFO  L225             Difference]: With dead ends: 148
[2025-05-07 17:25:13,463 INFO  L226             Difference]: Without dead ends: 148
[2025-05-07 17:25:13,463 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:25:13,464 INFO  L437           NwaCegarLoop]: 146 mSDtfsCounter, 1 mSDsluCounter, 710 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 856 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:13,464 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 856 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:25:13,464 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 148 states.
[2025-05-07 17:25:13,467 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 148 to 146.
[2025-05-07 17:25:13,467 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 146 states, 64 states have (on average 1.015625) internal successors, (65), 65 states have internal predecessors, (65), 41 states have call successors, (43), 39 states have call predecessors, (43), 40 states have return successors, (44), 41 states have call predecessors, (44), 41 states have call successors, (44)
[2025-05-07 17:25:13,468 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 146 states to 146 states and 152 transitions.
[2025-05-07 17:25:13,468 INFO  L79                 Accepts]: Start accepts. Automaton has 146 states and 152 transitions. Word has length 133
[2025-05-07 17:25:13,468 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:13,468 INFO  L485      AbstractCegarLoop]: Abstraction has 146 states and 152 transitions.
[2025-05-07 17:25:13,468 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:25:13,468 INFO  L278                IsEmpty]: Start isEmpty. Operand 146 states and 152 transitions.
[2025-05-07 17:25:13,469 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:25:13,469 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:13,469 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:25:13,469 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:25:13,469 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:13,470 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:13,470 INFO  L85        PathProgramCache]: Analyzing trace with hash -463206139, now seen corresponding path program 1 times
[2025-05-07 17:25:13,470 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:13,470 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [385939351]
[2025-05-07 17:25:13,470 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:13,470 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:13,514 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:25:13,538 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:25:13,538 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:13,538 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:15,699 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:15,699 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:15,699 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [385939351]
[2025-05-07 17:25:15,699 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [385939351] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:15,699 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:15,700 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [44] imperfect sequences [] total 44
[2025-05-07 17:25:15,700 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1592216537]
[2025-05-07 17:25:15,700 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:15,700 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 44 states
[2025-05-07 17:25:15,700 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:15,700 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 44 interpolants.
[2025-05-07 17:25:15,701 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=91, Invalid=1801, Unknown=0, NotChecked=0, Total=1892
[2025-05-07 17:25:15,701 INFO  L87              Difference]: Start difference. First operand 146 states and 152 transitions. Second operand  has 44 states, 31 states have (on average 1.903225806451613) internal successors, (59), 35 states have internal predecessors, (59), 19 states have call successors, (37), 1 states have call predecessors, (37), 31 states have return successors, (37), 34 states have call predecessors, (37), 19 states have call successors, (37)
[2025-05-07 17:25:16,756 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:16,756 INFO  L93              Difference]: Finished difference Result 151 states and 158 transitions.
[2025-05-07 17:25:16,757 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 44 states. 
[2025-05-07 17:25:16,757 INFO  L79                 Accepts]: Start accepts. Automaton has  has 44 states, 31 states have (on average 1.903225806451613) internal successors, (59), 35 states have internal predecessors, (59), 19 states have call successors, (37), 1 states have call predecessors, (37), 31 states have return successors, (37), 34 states have call predecessors, (37), 19 states have call successors, (37) Word has length 133
[2025-05-07 17:25:16,757 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:16,758 INFO  L225             Difference]: With dead ends: 151
[2025-05-07 17:25:16,759 INFO  L226             Difference]: Without dead ends: 142
[2025-05-07 17:25:16,759 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 52 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 91 ImplicationChecksByTransitivity, 1.0s TimeCoverageRelationStatistics Valid=147, Invalid=2715, Unknown=0, NotChecked=0, Total=2862
[2025-05-07 17:25:16,760 INFO  L437           NwaCegarLoop]: 122 mSDtfsCounter, 11 mSDsluCounter, 4891 mSDsCounter, 0 mSdLazyCounter, 1418 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 5013 SdHoareTripleChecker+Invalid, 1439 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 1418 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:16,760 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 5013 Invalid, 1439 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 1418 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:25:16,761 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-05-07 17:25:16,765 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 142.
[2025-05-07 17:25:16,765 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 62 states have (on average 1.0161290322580645) internal successors, (63), 63 states have internal predecessors, (63), 40 states have call successors, (41), 38 states have call predecessors, (41), 39 states have return successors, (42), 40 states have call predecessors, (42), 40 states have call successors, (42)
[2025-05-07 17:25:16,766 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 146 transitions.
[2025-05-07 17:25:16,766 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 146 transitions. Word has length 133
[2025-05-07 17:25:16,766 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:16,766 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 146 transitions.
[2025-05-07 17:25:16,766 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 44 states, 31 states have (on average 1.903225806451613) internal successors, (59), 35 states have internal predecessors, (59), 19 states have call successors, (37), 1 states have call predecessors, (37), 31 states have return successors, (37), 34 states have call predecessors, (37), 19 states have call successors, (37)
[2025-05-07 17:25:16,767 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 146 transitions.
[2025-05-07 17:25:16,768 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:25:16,768 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:16,768 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:25:16,768 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:25:16,768 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:16,769 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:16,769 INFO  L85        PathProgramCache]: Analyzing trace with hash -1014160283, now seen corresponding path program 1 times
[2025-05-07 17:25:16,769 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:16,769 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1954545300]
[2025-05-07 17:25:16,769 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:16,769 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:16,818 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:25:16,843 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:25:16,843 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:16,843 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:16,922 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:25:16,923 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:16,923 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1954545300]
[2025-05-07 17:25:16,923 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1954545300] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:16,923 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:16,923 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:16,923 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [410012186]
[2025-05-07 17:25:16,923 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:16,923 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:16,923 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:16,923 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:16,923 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:16,924 INFO  L87              Difference]: Start difference. First operand 142 states and 146 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:25:16,935 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:16,935 INFO  L93              Difference]: Finished difference Result 144 states and 147 transitions.
[2025-05-07 17:25:16,935 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:16,935 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:25:16,935 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:16,936 INFO  L225             Difference]: With dead ends: 144
[2025-05-07 17:25:16,936 INFO  L226             Difference]: Without dead ends: 134
[2025-05-07 17:25:16,936 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:25:16,936 INFO  L437           NwaCegarLoop]: 143 mSDtfsCounter, 1 mSDsluCounter, 272 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 415 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:25:16,936 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 415 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:16,937 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-05-07 17:25:16,939 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 134.
[2025-05-07 17:25:16,940 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:25:16,940 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 134 states to 134 states and 133 transitions.
[2025-05-07 17:25:16,941 INFO  L79                 Accepts]: Start accepts. Automaton has 134 states and 133 transitions. Word has length 133
[2025-05-07 17:25:16,941 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:16,941 INFO  L485      AbstractCegarLoop]: Abstraction has 134 states and 133 transitions.
[2025-05-07 17:25:16,941 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:25:16,941 INFO  L278                IsEmpty]: Start isEmpty. Operand 134 states and 133 transitions.
[2025-05-07 17:25:16,942 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 134
[2025-05-07 17:25:16,942 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:16,942 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:25:16,942 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:25:16,942 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:16,943 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:16,943 INFO  L85        PathProgramCache]: Analyzing trace with hash -2089895199, now seen corresponding path program 1 times
[2025-05-07 17:25:16,943 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:16,943 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [151831182]
[2025-05-07 17:25:16,943 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:16,943 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:16,975 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 133 statements into 1 equivalence classes.
[2025-05-07 17:25:16,994 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 133 of 133 statements.
[2025-05-07 17:25:16,994 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:16,995 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:17,123 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:25:17,123 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:17,123 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [151831182]
[2025-05-07 17:25:17,123 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [151831182] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:17,123 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:17,123 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:25:17,123 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [408414041]
[2025-05-07 17:25:17,123 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:17,124 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:25:17,124 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:17,124 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:25:17,124 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:25:17,124 INFO  L87              Difference]: Start difference. First operand 134 states and 133 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:25:17,154 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:17,154 INFO  L93              Difference]: Finished difference Result 128 states and 127 transitions.
[2025-05-07 17:25:17,155 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:25:17,155 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:25:17,155 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:17,155 INFO  L225             Difference]: With dead ends: 128
[2025-05-07 17:25:17,155 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:25:17,156 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:25:17,156 INFO  L437           NwaCegarLoop]: 124 mSDtfsCounter, 0 mSDsluCounter, 606 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 730 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:25:17,156 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 730 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:17,156 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:25:17,157 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:25:17,157 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:25:17,157 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:25:17,157 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 133
[2025-05-07 17:25:17,157 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:17,157 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:25:17,157 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:25:17,157 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:25:17,157 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:25:17,159 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:25:17,159 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:25:17,162 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:17,164 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:25:17,166 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:25:17 BoogieIcfgContainer
[2025-05-07 17:25:17,166 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:25:17,167 INFO  L158              Benchmark]: Toolchain (without parser) took 7025.29ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 134.6MB in the beginning and 228.6MB in the end (delta: -94.0MB). Peak memory consumption was 39.0MB. Max. memory is 33.6GB.
[2025-05-07 17:25:17,167 INFO  L158              Benchmark]: SmtParser took 0.18ms. Allocated memory is still 234.9MB. Free memory is still 174.6MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:17,167 INFO  L158              Benchmark]: ChcToBoogie took 51.57ms. Allocated memory is still 234.9MB. Free memory was 134.6MB in the beginning and 130.6MB in the end (delta: 4.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:17,167 INFO  L158              Benchmark]: Boogie Preprocessor took 59.51ms. Allocated memory is still 234.9MB. Free memory was 130.6MB in the beginning and 126.6MB in the end (delta: 4.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:25:17,167 INFO  L158              Benchmark]: RCFGBuilder took 546.23ms. Allocated memory is still 234.9MB. Free memory was 126.5MB in the beginning and 132.3MB in the end (delta: -5.8MB). Peak memory consumption was 25.8MB. Max. memory is 33.6GB.
[2025-05-07 17:25:17,168 INFO  L158              Benchmark]: TraceAbstraction took 6364.76ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 131.4MB in the beginning and 228.6MB in the end (delta: -97.2MB). Peak memory consumption was 30.0MB. Max. memory is 33.6GB.
[2025-05-07 17:25:17,168 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.18ms. Allocated memory is still 234.9MB. Free memory is still 174.6MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 51.57ms. Allocated memory is still 234.9MB. Free memory was 134.6MB in the beginning and 130.6MB in the end (delta: 4.0MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 59.51ms. Allocated memory is still 234.9MB. Free memory was 130.6MB in the beginning and 126.6MB in the end (delta: 4.0MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 546.23ms. Allocated memory is still 234.9MB. Free memory was 126.5MB in the beginning and 132.3MB in the end (delta: -5.8MB). Peak memory consumption was 25.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 6364.76ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 131.4MB in the beginning and 228.6MB in the end (delta: -97.2MB). Peak memory consumption was 30.0MB. 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: 6.3s, OverallIterations: 13, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 1.7s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 83 SdHoareTripleChecker+Valid, 1.2s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 19 mSDsluCounter, 14200 SdHoareTripleChecker+Invalid, 1.1s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 11974 mSDsCounter, 33 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 1697 IncrementalHoareTripleChecker+Invalid, 1730 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 33 mSolverCounterUnsat, 2226 mSDtfsCounter, 1697 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 120 GetRequests, 26 SyntacticMatches, 0 SemanticMatches, 94 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 92 ImplicationChecksByTransitivity, 1.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=176occurred in iteration=0, InterpolantAutomatonStates: 110, 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, 10 StatesRemovedByMinimization, 5 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.3s SatisfiabilityAnalysisTime, 3.6s InterpolantComputationTime, 1329 NumberOfCodeBlocks, 1329 NumberOfCodeBlocksAsserted, 13 NumberOfCheckSat, 1316 ConstructedInterpolants, 0 QuantifiedInterpolants, 1776 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:25:17,181 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
