./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-262.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:47,335 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:47,408 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_17e61fa9-2c4f-4f4f-aafb-4b74f8de6d16/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:47,413 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:47,413 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:47,435 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:47,436 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:47,436 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:47,436 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:47,436 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:47,437 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:47,437 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:47,437 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:47,437 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:47,437 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:47,437 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:47,437 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:47,438 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:47,438 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:47,438 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:47,438 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:47,438 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:47,438 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:47,438 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:47,439 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:47,439 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:47,439 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:47,781 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:47,792 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:47,795 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:47,797 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:47,798 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:47,799 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_17e61fa9-2c4f-4f4f-aafb-4b74f8de6d16/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-262.smt2
[2025-04-28 21:21:47,801 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:47,805 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:48,326 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_17e61fa9-2c4f-4f4f-aafb-4b74f8de6d16/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-262.smt2
[2025-04-28 21:21:48,330 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:48,332 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:48,333 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:48,333 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:48,333 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:48,337 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,384 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48 Unit
[2025-04-28 21:21:48,384 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:48,385 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:48,385 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:48,386 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:48,402 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,402 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,435 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,435 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,451 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,452 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,455 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,461 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,466 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,512 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:48,513 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:48,513 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:48,513 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:48,517 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,521 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:48,542 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,561 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:48,567 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,584 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:48,584 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:48,585 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:48,585 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:48,585 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:48,585 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:48,585 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH0.CLN Main.java, line 23 given in one single declaration
[2025-04-28 21:21:48,585 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH0.CLN Main.java, line 23
[2025-04-28 21:21:48,585 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH0.CLN Main.java, line 23
[2025-04-28 21:21:48,585 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_7 given in one single declaration
[2025-04-28 21:21:48,585 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_7
[2025-04-28 21:21:48,586 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_7
[2025-04-28 21:21:48,586 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_6 given in one single declaration
[2025-04-28 21:21:48,586 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_6
[2025-04-28 21:21:48,586 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_6
[2025-04-28 21:21:48,587 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_5 given in one single declaration
[2025-04-28 21:21:48,587 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_5
[2025-04-28 21:21:48,588 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_5
[2025-04-28 21:21:48,588 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_4 given in one single declaration
[2025-04-28 21:21:48,588 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_4
[2025-04-28 21:21:48,588 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_4
[2025-04-28 21:21:48,588 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_3 given in one single declaration
[2025-04-28 21:21:48,588 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_3
[2025-04-28 21:21:48,588 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_3
[2025-04-28 21:21:48,588 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_2 given in one single declaration
[2025-04-28 21:21:48,588 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_2
[2025-04-28 21:21:48,588 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_2
[2025-04-28 21:21:48,589 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_1 given in one single declaration
[2025-04-28 21:21:48,589 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_1
[2025-04-28 21:21:48,589 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_1
[2025-04-28 21:21:48,589 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20 given in one single declaration
[2025-04-28 21:21:48,589 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20
[2025-04-28 21:21:48,589 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20
[2025-04-28 21:21:48,590 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre given in one single declaration
[2025-04-28 21:21:48,590 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:48,590 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:48,590 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH1.CLN Main.java, line 24 given in one single declaration
[2025-04-28 21:21:48,590 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH1.CLN Main.java, line 24
[2025-04-28 21:21:48,590 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH1.CLN Main.java, line 24
[2025-04-28 21:21:48,591 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_11 given in one single declaration
[2025-04-28 21:21:48,591 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_11
[2025-04-28 21:21:48,591 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_11
[2025-04-28 21:21:48,591 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_10 given in one single declaration
[2025-04-28 21:21:48,591 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_10
[2025-04-28 21:21:48,591 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_10
[2025-04-28 21:21:48,591 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_9 given in one single declaration
[2025-04-28 21:21:48,591 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_9
[2025-04-28 21:21:48,591 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_9
[2025-04-28 21:21:48,592 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_8 given in one single declaration
[2025-04-28 21:21:48,592 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_8
[2025-04-28 21:21:48,592 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_8
[2025-04-28 21:21:48,592 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH3.CLN Main.java, line 29 given in one single declaration
[2025-04-28 21:21:48,592 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH3.CLN Main.java, line 29
[2025-04-28 21:21:48,592 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH3.CLN Main.java, line 29
[2025-04-28 21:21:48,592 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5 given in one single declaration
[2025-04-28 21:21:48,592 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5
[2025-04-28 21:21:48,592 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5
[2025-04-28 21:21:48,592 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block4 given in one single declaration
[2025-04-28 21:21:48,593 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block4
[2025-04-28 21:21:48,593 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block4
[2025-04-28 21:21:48,593 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3 given in one single declaration
[2025-04-28 21:21:48,593 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3
[2025-04-28 21:21:48,593 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3
[2025-04-28 21:21:48,594 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_4 given in one single declaration
[2025-04-28 21:21:48,595 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_4
[2025-04-28 21:21:48,595 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_4
[2025-04-28 21:21:48,596 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_3 given in one single declaration
[2025-04-28 21:21:48,596 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_3
[2025-04-28 21:21:48,596 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_3
[2025-04-28 21:21:48,596 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_2 given in one single declaration
[2025-04-28 21:21:48,596 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_2
[2025-04-28 21:21:48,596 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_2
[2025-04-28 21:21:48,596 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_1 given in one single declaration
[2025-04-28 21:21:48,596 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_1
[2025-04-28 21:21:48,596 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10_1
[2025-04-28 21:21:48,596 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10 given in one single declaration
[2025-04-28 21:21:48,597 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10
[2025-04-28 21:21:48,597 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block10
[2025-04-28 21:21:48,597 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18_1 given in one single declaration
[2025-04-28 21:21:48,597 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18_1
[2025-04-28 21:21:48,597 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18_1
[2025-04-28 21:21:48,597 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18 given in one single declaration
[2025-04-28 21:21:48,597 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18
[2025-04-28 21:21:48,597 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block18
[2025-04-28 21:21:48,597 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_3 given in one single declaration
[2025-04-28 21:21:48,597 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_3
[2025-04-28 21:21:48,597 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_3
[2025-04-28 21:21:48,599 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_2 given in one single declaration
[2025-04-28 21:21:48,599 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_2
[2025-04-28 21:21:48,599 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_2
[2025-04-28 21:21:48,600 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_1 given in one single declaration
[2025-04-28 21:21:48,600 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_1
[2025-04-28 21:21:48,600 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14_1
[2025-04-28 21:21:48,600 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14 given in one single declaration
[2025-04-28 21:21:48,600 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14
[2025-04-28 21:21:48,600 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block14
[2025-04-28 21:21:48,600 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block12 given in one single declaration
[2025-04-28 21:21:48,600 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block12
[2025-04-28 21:21:48,600 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block12
[2025-04-28 21:21:48,600 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_14 given in one single declaration
[2025-04-28 21:21:48,600 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_14
[2025-04-28 21:21:48,600 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_14
[2025-04-28 21:21:48,600 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_13 given in one single declaration
[2025-04-28 21:21:48,600 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_13
[2025-04-28 21:21:48,601 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_13
[2025-04-28 21:21:48,601 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_12 given in one single declaration
[2025-04-28 21:21:48,601 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_12
[2025-04-28 21:21:48,601 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block20_12
[2025-04-28 21:21:48,601 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_post given in one single declaration
[2025-04-28 21:21:48,601 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_post
[2025-04-28 21:21:48,601 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_post
[2025-04-28 21:21:48,601 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block0 given in one single declaration
[2025-04-28 21:21:48,601 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block0
[2025-04-28 21:21:48,601 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block0
[2025-04-28 21:21:48,601 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block6_1 given in one single declaration
[2025-04-28 21:21:48,602 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block6_1
[2025-04-28 21:21:48,602 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block6_1
[2025-04-28 21:21:48,603 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block6 given in one single declaration
[2025-04-28 21:21:48,603 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block6
[2025-04-28 21:21:48,603 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block6
[2025-04-28 21:21:48,603 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block5_3 given in one single declaration
[2025-04-28 21:21:48,603 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block5_3
[2025-04-28 21:21:48,603 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block5_3
[2025-04-28 21:21:48,603 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block5_2 given in one single declaration
[2025-04-28 21:21:48,603 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block5_2
[2025-04-28 21:21:48,603 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block5_2
[2025-04-28 21:21:48,603 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block5_1 given in one single declaration
[2025-04-28 21:21:48,604 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block5_1
[2025-04-28 21:21:48,604 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block5_1
[2025-04-28 21:21:48,605 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block5 given in one single declaration
[2025-04-28 21:21:48,605 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block5
[2025-04-28 21:21:48,605 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block5
[2025-04-28 21:21:48,605 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block2 given in one single declaration
[2025-04-28 21:21:48,605 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block2
[2025-04-28 21:21:48,605 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block2
[2025-04-28 21:21:48,605 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block1_3 given in one single declaration
[2025-04-28 21:21:48,605 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block1_3
[2025-04-28 21:21:48,605 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block1_3
[2025-04-28 21:21:48,605 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block1_2 given in one single declaration
[2025-04-28 21:21:48,605 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block1_2
[2025-04-28 21:21:48,605 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block1_2
[2025-04-28 21:21:48,606 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block1_1 given in one single declaration
[2025-04-28 21:21:48,606 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block1_1
[2025-04-28 21:21:48,606 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block1_1
[2025-04-28 21:21:48,606 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block1 given in one single declaration
[2025-04-28 21:21:48,606 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block1
[2025-04-28 21:21:48,606 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block1
[2025-04-28 21:21:48,606 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_pre given in one single declaration
[2025-04-28 21:21:48,606 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_pre
[2025-04-28 21:21:48,606 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_pre
[2025-04-28 21:21:48,606 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block4_2 given in one single declaration
[2025-04-28 21:21:48,606 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block4_2
[2025-04-28 21:21:48,606 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block4_2
[2025-04-28 21:21:48,606 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block4_1 given in one single declaration
[2025-04-28 21:21:48,606 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block4_1
[2025-04-28 21:21:48,608 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block4_1
[2025-04-28 21:21:48,608 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block4 given in one single declaration
[2025-04-28 21:21:48,608 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block4
[2025-04-28 21:21:48,608 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block4
[2025-04-28 21:21:48,608 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_2 given in one single declaration
[2025-04-28 21:21:48,608 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_2
[2025-04-28 21:21:48,608 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_2
[2025-04-28 21:21:48,608 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_1 given in one single declaration
[2025-04-28 21:21:48,608 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_1
[2025-04-28 21:21:48,608 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_1
[2025-04-28 21:21:48,608 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15 given in one single declaration
[2025-04-28 21:21:48,609 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15
[2025-04-28 21:21:48,609 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15
[2025-04-28 21:21:48,609 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block3_1 given in one single declaration
[2025-04-28 21:21:48,609 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block3_1
[2025-04-28 21:21:48,609 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block3_1
[2025-04-28 21:21:48,609 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block3 given in one single declaration
[2025-04-28 21:21:48,609 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block3
[2025-04-28 21:21:48,609 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block3
[2025-04-28 21:21:48,609 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block7_1 given in one single declaration
[2025-04-28 21:21:48,609 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block7_1
[2025-04-28 21:21:48,609 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block7_1
[2025-04-28 21:21:48,609 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block7 given in one single declaration
[2025-04-28 21:21:48,609 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block7
[2025-04-28 21:21:48,609 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block7
[2025-04-28 21:21:48,610 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block9_1 given in one single declaration
[2025-04-28 21:21:48,610 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block9_1
[2025-04-28 21:21:48,610 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block9_1
[2025-04-28 21:21:48,610 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block9 given in one single declaration
[2025-04-28 21:21:48,610 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block9
[2025-04-28 21:21:48,610 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block9
[2025-04-28 21:21:48,610 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block4_3 given in one single declaration
[2025-04-28 21:21:48,610 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block4_3
[2025-04-28 21:21:48,610 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block4_3
[2025-04-28 21:21:48,610 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block8_1 given in one single declaration
[2025-04-28 21:21:48,610 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block8_1
[2025-04-28 21:21:48,610 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block8_1
[2025-04-28 21:21:48,610 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN int addition(int,int)>_Block8 given in one single declaration
[2025-04-28 21:21:48,611 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block8
[2025-04-28 21:21:48,611 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block8
[2025-04-28 21:21:48,611 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16_1 given in one single declaration
[2025-04-28 21:21:48,611 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16_1
[2025-04-28 21:21:48,611 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16_1
[2025-04-28 21:21:48,611 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16 given in one single declaration
[2025-04-28 21:21:48,611 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16
[2025-04-28 21:21:48,611 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block16
[2025-04-28 21:21:48,611 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_3 given in one single declaration
[2025-04-28 21:21:48,611 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_3
[2025-04-28 21:21:48,611 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block15_3
[2025-04-28 21:21:48,611 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block19_1 given in one single declaration
[2025-04-28 21:21:48,611 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block19_1
[2025-04-28 21:21:48,611 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block19_1
[2025-04-28 21:21:48,611 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block19 given in one single declaration
[2025-04-28 21:21:48,611 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block19
[2025-04-28 21:21:48,612 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block19
[2025-04-28 21:21:48,613 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17_1 given in one single declaration
[2025-04-28 21:21:48,613 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17_1
[2025-04-28 21:21:48,613 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17_1
[2025-04-28 21:21:48,613 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17 given in one single declaration
[2025-04-28 21:21:48,613 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17
[2025-04-28 21:21:48,614 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block17
[2025-04-28 21:21:48,614 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13_1 given in one single declaration
[2025-04-28 21:21:48,614 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13_1
[2025-04-28 21:21:48,614 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13_1
[2025-04-28 21:21:48,614 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13 given in one single declaration
[2025-04-28 21:21:48,614 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13
[2025-04-28 21:21:48,614 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block13
[2025-04-28 21:21:48,614 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Assert .HSH2.CLN Main.java, line 25 given in one single declaration
[2025-04-28 21:21:48,614 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH2.CLN Main.java, line 25
[2025-04-28 21:21:48,614 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH2.CLN Main.java, line 25
[2025-04-28 21:21:48,614 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:48,614 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:48,615 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:48,908 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:48,912 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:49,442 INFO  L?                        ?]: Removed 28 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:49,443 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:49,470 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:49,470 INFO  L312             CfgBuilder]: Removed 36 assume(true) statements.
[2025-04-28 21:21:49,471 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:49 BoogieIcfgContainer
[2025-04-28 21:21:49,471 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:49,474 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:49,474 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:49,479 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:49,480 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:48" (1/3) ...
[2025-04-28 21:21:49,480 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2023625f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:49, skipping insertion in model container
[2025-04-28 21:21:49,480 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (2/3) ...
[2025-04-28 21:21:49,481 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2023625f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:49, skipping insertion in model container
[2025-04-28 21:21:49,481 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:49" (3/3) ...
[2025-04-28 21:21:49,482 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:49,508 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:49,511 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 76 procedures, 286 locations, 410 edges, 76 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:49,581 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:49,606 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;@4c2e01a2, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:49,609 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:49,613 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 286 states, 130 states have (on average 1.0076923076923077) internal successors, (131), 131 states have internal predecessors, (131), 79 states have call successors, (93), 75 states have call predecessors, (93), 75 states have return successors, (93), 79 states have call predecessors, (93), 79 states have call successors, (93)
[2025-04-28 21:21:49,632 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:21:49,633 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,634 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]
[2025-04-28 21:21:49,634 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,640 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,641 INFO  L85        PathProgramCache]: Analyzing trace with hash 1113851978, now seen corresponding path program 1 times
[2025-04-28 21:21:49,650 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,651 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1045711324]
[2025-04-28 21:21:49,651 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,652 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,762 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:49,844 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:49,844 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,844 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,114 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:50,115 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,115 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1045711324]
[2025-04-28 21:21:50,116 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1045711324] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,116 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,121 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,122 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [157849748]
[2025-04-28 21:21:50,123 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,128 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,128 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,158 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,159 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,163 INFO  L87              Difference]: Start difference. First operand  has 286 states, 130 states have (on average 1.0076923076923077) internal successors, (131), 131 states have internal predecessors, (131), 79 states have call successors, (93), 75 states have call predecessors, (93), 75 states have return successors, (93), 79 states have call predecessors, (93), 79 states have call successors, (93) Second operand  has 4 states, 3 states have (on average 7.0) internal successors, (21), 4 states have internal predecessors, (21), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:50,319 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,320 INFO  L93              Difference]: Finished difference Result 282 states and 312 transitions.
[2025-04-28 21:21:50,322 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:50,324 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.0) internal successors, (21), 4 states have internal predecessors, (21), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12) Word has length 45
[2025-04-28 21:21:50,325 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,341 INFO  L225             Difference]: With dead ends: 282
[2025-04-28 21:21:50,341 INFO  L226             Difference]: Without dead ends: 280
[2025-04-28 21:21:50,344 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,348 INFO  L437           NwaCegarLoop]: 311 mSDtfsCounter, 0 mSDsluCounter, 616 mSDsCounter, 0 mSdLazyCounter, 5 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 927 SdHoareTripleChecker+Invalid, 5 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 5 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,349 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 927 Invalid, 5 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 5 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:50,378 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 280 states.
[2025-04-28 21:21:50,453 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 280 to 280.
[2025-04-28 21:21:50,457 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 280 states, 127 states have (on average 1.0) internal successors, (127), 127 states have internal predecessors, (127), 78 states have call successors, (91), 74 states have call predecessors, (91), 74 states have return successors, (91), 78 states have call predecessors, (91), 78 states have call successors, (91)
[2025-04-28 21:21:50,468 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 280 states to 280 states and 309 transitions.
[2025-04-28 21:21:50,470 INFO  L79                 Accepts]: Start accepts. Automaton has 280 states and 309 transitions. Word has length 45
[2025-04-28 21:21:50,471 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,471 INFO  L485      AbstractCegarLoop]: Abstraction has 280 states and 309 transitions.
[2025-04-28 21:21:50,471 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.0) internal successors, (21), 4 states have internal predecessors, (21), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:50,471 INFO  L278                IsEmpty]: Start isEmpty. Operand 280 states and 309 transitions.
[2025-04-28 21:21:50,475 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-04-28 21:21:50,479 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,479 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,479 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:50,479 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,481 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,481 INFO  L85        PathProgramCache]: Analyzing trace with hash 772081543, now seen corresponding path program 1 times
[2025-04-28 21:21:50,481 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,482 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [566170601]
[2025-04-28 21:21:50,482 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,482 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,524 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-04-28 21:21:50,559 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:50,564 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,564 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,756 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:50,757 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,757 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [566170601]
[2025-04-28 21:21:50,757 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [566170601] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,757 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,757 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,758 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1135280244]
[2025-04-28 21:21:50,760 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,761 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,762 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,762 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,762 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,766 INFO  L87              Difference]: Start difference. First operand 280 states and 309 transitions. Second operand  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:50,826 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,829 INFO  L93              Difference]: Finished difference Result 278 states and 306 transitions.
[2025-04-28 21:21:50,830 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:50,830 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16) Word has length 59
[2025-04-28 21:21:50,830 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,834 INFO  L225             Difference]: With dead ends: 278
[2025-04-28 21:21:50,838 INFO  L226             Difference]: Without dead ends: 276
[2025-04-28 21:21:50,838 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,839 INFO  L437           NwaCegarLoop]: 305 mSDtfsCounter, 0 mSDsluCounter, 604 mSDsCounter, 0 mSdLazyCounter, 5 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 909 SdHoareTripleChecker+Invalid, 5 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 5 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,842 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 909 Invalid, 5 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 5 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:50,843 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 276 states.
[2025-04-28 21:21:50,866 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 276 to 276.
[2025-04-28 21:21:50,869 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 276 states, 125 states have (on average 1.0) internal successors, (125), 125 states have internal predecessors, (125), 77 states have call successors, (89), 73 states have call predecessors, (89), 73 states have return successors, (89), 77 states have call predecessors, (89), 77 states have call successors, (89)
[2025-04-28 21:21:50,872 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 276 states to 276 states and 303 transitions.
[2025-04-28 21:21:50,874 INFO  L79                 Accepts]: Start accepts. Automaton has 276 states and 303 transitions. Word has length 59
[2025-04-28 21:21:50,874 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,874 INFO  L485      AbstractCegarLoop]: Abstraction has 276 states and 303 transitions.
[2025-04-28 21:21:50,875 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 9.0) internal successors, (27), 4 states have internal predecessors, (27), 3 states have call successors, (16), 1 states have call predecessors, (16), 3 states have return successors, (16), 3 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:50,875 INFO  L278                IsEmpty]: Start isEmpty. Operand 276 states and 303 transitions.
[2025-04-28 21:21:50,877 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 93
[2025-04-28 21:21:50,877 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,878 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]
[2025-04-28 21:21:50,878 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:50,878 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,879 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,879 INFO  L85        PathProgramCache]: Analyzing trace with hash -1374559604, now seen corresponding path program 1 times
[2025-04-28 21:21:50,879 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,879 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2077268278]
[2025-04-28 21:21:50,879 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,879 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,916 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-04-28 21:21:50,945 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-04-28 21:21:50,945 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,945 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,616 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:51,616 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,616 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2077268278]
[2025-04-28 21:21:51,616 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2077268278] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,616 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,616 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-04-28 21:21:51,616 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [731189816]
[2025-04-28 21:21:51,617 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,617 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:51,617 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,618 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:51,618 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=131, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:51,618 INFO  L87              Difference]: Start difference. First operand 276 states and 303 transitions. Second operand  has 13 states, 10 states have (on average 4.2) internal successors, (42), 13 states have internal predecessors, (42), 5 states have call successors, (25), 1 states have call predecessors, (25), 10 states have return successors, (25), 10 states have call predecessors, (25), 5 states have call successors, (25)
[2025-04-28 21:21:51,847 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,848 INFO  L93              Difference]: Finished difference Result 284 states and 311 transitions.
[2025-04-28 21:21:51,848 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:51,848 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 4.2) internal successors, (42), 13 states have internal predecessors, (42), 5 states have call successors, (25), 1 states have call predecessors, (25), 10 states have return successors, (25), 10 states have call predecessors, (25), 5 states have call successors, (25) Word has length 92
[2025-04-28 21:21:51,849 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,852 INFO  L225             Difference]: With dead ends: 284
[2025-04-28 21:21:51,854 INFO  L226             Difference]: Without dead ends: 284
[2025-04-28 21:21:51,855 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=25, Invalid=131, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:51,856 INFO  L437           NwaCegarLoop]: 293 mSDtfsCounter, 3 mSDsluCounter, 2908 mSDsCounter, 0 mSdLazyCounter, 116 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 3201 SdHoareTripleChecker+Invalid, 116 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 116 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,857 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 3201 Invalid, 116 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 116 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:51,858 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 284 states.
[2025-04-28 21:21:51,886 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 284 to 284.
[2025-04-28 21:21:51,890 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 284 states, 129 states have (on average 1.0) internal successors, (129), 129 states have internal predecessors, (129), 77 states have call successors, (89), 73 states have call predecessors, (89), 77 states have return successors, (93), 81 states have call predecessors, (93), 77 states have call successors, (93)
[2025-04-28 21:21:51,892 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 284 states to 284 states and 311 transitions.
[2025-04-28 21:21:51,894 INFO  L79                 Accepts]: Start accepts. Automaton has 284 states and 311 transitions. Word has length 92
[2025-04-28 21:21:51,895 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,895 INFO  L485      AbstractCegarLoop]: Abstraction has 284 states and 311 transitions.
[2025-04-28 21:21:51,895 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 4.2) internal successors, (42), 13 states have internal predecessors, (42), 5 states have call successors, (25), 1 states have call predecessors, (25), 10 states have return successors, (25), 10 states have call predecessors, (25), 5 states have call successors, (25)
[2025-04-28 21:21:51,896 INFO  L278                IsEmpty]: Start isEmpty. Operand 284 states and 311 transitions.
[2025-04-28 21:21:51,898 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 107
[2025-04-28 21:21:51,899 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,900 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]
[2025-04-28 21:21:51,900 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:51,900 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,901 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,904 INFO  L85        PathProgramCache]: Analyzing trace with hash 1757534938, now seen corresponding path program 1 times
[2025-04-28 21:21:51,904 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,904 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [465997105]
[2025-04-28 21:21:51,904 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,904 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,940 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 106 statements into 1 equivalence classes.
[2025-04-28 21:21:51,956 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 106 of 106 statements.
[2025-04-28 21:21:51,956 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,957 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,369 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:52,371 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,371 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [465997105]
[2025-04-28 21:21:52,371 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [465997105] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,371 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,371 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:52,371 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1164880197]
[2025-04-28 21:21:52,371 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,372 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:52,372 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,373 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:52,374 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:52,375 INFO  L87              Difference]: Start difference. First operand 284 states and 311 transitions. Second operand  has 11 states, 10 states have (on average 4.8) internal successors, (48), 11 states have internal predecessors, (48), 3 states have call successors, (29), 1 states have call predecessors, (29), 10 states have return successors, (29), 10 states have call predecessors, (29), 3 states have call successors, (29)
[2025-04-28 21:21:52,528 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,529 INFO  L93              Difference]: Finished difference Result 288 states and 314 transitions.
[2025-04-28 21:21:52,529 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:52,530 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 10 states have (on average 4.8) internal successors, (48), 11 states have internal predecessors, (48), 3 states have call successors, (29), 1 states have call predecessors, (29), 10 states have return successors, (29), 10 states have call predecessors, (29), 3 states have call successors, (29) Word has length 106
[2025-04-28 21:21:52,530 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,532 INFO  L225             Difference]: With dead ends: 288
[2025-04-28 21:21:52,532 INFO  L226             Difference]: Without dead ends: 268
[2025-04-28 21:21:52,532 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:52,534 INFO  L437           NwaCegarLoop]: 295 mSDtfsCounter, 1 mSDsluCounter, 2643 mSDsCounter, 0 mSdLazyCounter, 83 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 2938 SdHoareTripleChecker+Invalid, 83 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 83 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,535 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 2938 Invalid, 83 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 83 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:52,536 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 268 states.
[2025-04-28 21:21:52,552 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 268 to 268.
[2025-04-28 21:21:52,554 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 268 states, 121 states have (on average 1.0) internal successors, (121), 121 states have internal predecessors, (121), 75 states have call successors, (86), 71 states have call predecessors, (86), 71 states have return successors, (86), 75 states have call predecessors, (86), 75 states have call successors, (86)
[2025-04-28 21:21:52,557 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 268 states to 268 states and 293 transitions.
[2025-04-28 21:21:52,557 INFO  L79                 Accepts]: Start accepts. Automaton has 268 states and 293 transitions. Word has length 106
[2025-04-28 21:21:52,557 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,558 INFO  L485      AbstractCegarLoop]: Abstraction has 268 states and 293 transitions.
[2025-04-28 21:21:52,558 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 10 states have (on average 4.8) internal successors, (48), 11 states have internal predecessors, (48), 3 states have call successors, (29), 1 states have call predecessors, (29), 10 states have return successors, (29), 10 states have call predecessors, (29), 3 states have call successors, (29)
[2025-04-28 21:21:52,558 INFO  L278                IsEmpty]: Start isEmpty. Operand 268 states and 293 transitions.
[2025-04-28 21:21:52,561 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 220
[2025-04-28 21:21:52,561 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,562 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,562 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:52,562 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,563 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,563 INFO  L85        PathProgramCache]: Analyzing trace with hash 766558789, now seen corresponding path program 1 times
[2025-04-28 21:21:52,563 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,563 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1007355145]
[2025-04-28 21:21:52,563 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,563 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,614 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 219 statements into 1 equivalence classes.
[2025-04-28 21:21:52,640 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 219 of 219 statements.
[2025-04-28 21:21:52,640 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,640 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,137 INFO  L134       CoverageAnalysis]: Checked inductivity of 74 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 74 trivial. 0 not checked.
[2025-04-28 21:21:53,137 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,138 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1007355145]
[2025-04-28 21:21:53,138 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1007355145] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,138 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,138 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:53,138 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1940805224]
[2025-04-28 21:21:53,138 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,139 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:53,139 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,139 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:53,139 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:53,143 INFO  L87              Difference]: Start difference. First operand 268 states and 293 transitions. Second operand  has 10 states, 9 states have (on average 7.333333333333333) internal successors, (66), 10 states have internal predecessors, (66), 3 states have call successors, (40), 1 states have call predecessors, (40), 9 states have return successors, (40), 9 states have call predecessors, (40), 3 states have call successors, (40)
[2025-04-28 21:21:53,325 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,325 INFO  L93              Difference]: Finished difference Result 274 states and 302 transitions.
[2025-04-28 21:21:53,326 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:53,326 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 7.333333333333333) internal successors, (66), 10 states have internal predecessors, (66), 3 states have call successors, (40), 1 states have call predecessors, (40), 9 states have return successors, (40), 9 states have call predecessors, (40), 3 states have call successors, (40) Word has length 219
[2025-04-28 21:21:53,327 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,328 INFO  L225             Difference]: With dead ends: 274
[2025-04-28 21:21:53,328 INFO  L226             Difference]: Without dead ends: 274
[2025-04-28 21:21:53,329 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:53,331 INFO  L437           NwaCegarLoop]: 281 mSDtfsCounter, 1 mSDsluCounter, 2228 mSDsCounter, 0 mSdLazyCounter, 115 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 2509 SdHoareTripleChecker+Invalid, 115 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 115 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,332 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 2509 Invalid, 115 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 115 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:53,333 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 274 states.
[2025-04-28 21:21:53,348 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 274 to 274.
[2025-04-28 21:21:53,351 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 274 states, 124 states have (on average 1.0) internal successors, (124), 124 states have internal predecessors, (124), 75 states have call successors, (86), 71 states have call predecessors, (86), 74 states have return successors, (92), 78 states have call predecessors, (92), 75 states have call successors, (92)
[2025-04-28 21:21:53,353 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 274 states to 274 states and 302 transitions.
[2025-04-28 21:21:53,353 INFO  L79                 Accepts]: Start accepts. Automaton has 274 states and 302 transitions. Word has length 219
[2025-04-28 21:21:53,354 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,354 INFO  L485      AbstractCegarLoop]: Abstraction has 274 states and 302 transitions.
[2025-04-28 21:21:53,354 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 7.333333333333333) internal successors, (66), 10 states have internal predecessors, (66), 3 states have call successors, (40), 1 states have call predecessors, (40), 9 states have return successors, (40), 9 states have call predecessors, (40), 3 states have call successors, (40)
[2025-04-28 21:21:53,354 INFO  L278                IsEmpty]: Start isEmpty. Operand 274 states and 302 transitions.
[2025-04-28 21:21:53,361 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 219
[2025-04-28 21:21:53,361 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,361 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,361 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:53,361 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,364 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,364 INFO  L85        PathProgramCache]: Analyzing trace with hash -255236041, now seen corresponding path program 1 times
[2025-04-28 21:21:53,364 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,364 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [944220826]
[2025-04-28 21:21:53,364 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,365 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,429 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 218 statements into 1 equivalence classes.
[2025-04-28 21:21:53,460 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 218 of 218 statements.
[2025-04-28 21:21:53,460 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,460 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,197 INFO  L134       CoverageAnalysis]: Checked inductivity of 74 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 74 trivial. 0 not checked.
[2025-04-28 21:21:54,198 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,198 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [944220826]
[2025-04-28 21:21:54,198 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [944220826] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,198 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,199 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:54,199 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1665604509]
[2025-04-28 21:21:54,199 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,200 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:54,201 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,202 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:54,202 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:54,203 INFO  L87              Difference]: Start difference. First operand 274 states and 302 transitions. Second operand  has 11 states, 8 states have (on average 8.125) internal successors, (65), 11 states have internal predecessors, (65), 5 states have call successors, (40), 1 states have call predecessors, (40), 8 states have return successors, (40), 8 states have call predecessors, (40), 5 states have call successors, (40)
[2025-04-28 21:21:54,321 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,321 INFO  L93              Difference]: Finished difference Result 282 states and 310 transitions.
[2025-04-28 21:21:54,322 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:54,322 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 8 states have (on average 8.125) internal successors, (65), 11 states have internal predecessors, (65), 5 states have call successors, (40), 1 states have call predecessors, (40), 8 states have return successors, (40), 8 states have call predecessors, (40), 5 states have call successors, (40) Word has length 218
[2025-04-28 21:21:54,323 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,325 INFO  L225             Difference]: With dead ends: 282
[2025-04-28 21:21:54,325 INFO  L226             Difference]: Without dead ends: 282
[2025-04-28 21:21:54,326 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:54,327 INFO  L437           NwaCegarLoop]: 286 mSDtfsCounter, 3 mSDsluCounter, 1988 mSDsCounter, 0 mSdLazyCounter, 61 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 2274 SdHoareTripleChecker+Invalid, 61 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 61 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,327 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 2274 Invalid, 61 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 61 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:54,328 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 282 states.
[2025-04-28 21:21:54,339 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 282 to 282.
[2025-04-28 21:21:54,340 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 282 states, 128 states have (on average 1.0) internal successors, (128), 128 states have internal predecessors, (128), 75 states have call successors, (86), 71 states have call predecessors, (86), 78 states have return successors, (96), 82 states have call predecessors, (96), 75 states have call successors, (96)
[2025-04-28 21:21:54,344 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 282 states to 282 states and 310 transitions.
[2025-04-28 21:21:54,344 INFO  L79                 Accepts]: Start accepts. Automaton has 282 states and 310 transitions. Word has length 218
[2025-04-28 21:21:54,345 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,347 INFO  L485      AbstractCegarLoop]: Abstraction has 282 states and 310 transitions.
[2025-04-28 21:21:54,347 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 8 states have (on average 8.125) internal successors, (65), 11 states have internal predecessors, (65), 5 states have call successors, (40), 1 states have call predecessors, (40), 8 states have return successors, (40), 8 states have call predecessors, (40), 5 states have call successors, (40)
[2025-04-28 21:21:54,347 INFO  L278                IsEmpty]: Start isEmpty. Operand 282 states and 310 transitions.
[2025-04-28 21:21:54,351 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 219
[2025-04-28 21:21:54,353 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,353 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,353 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:54,353 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,354 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,354 INFO  L85        PathProgramCache]: Analyzing trace with hash 753756854, now seen corresponding path program 1 times
[2025-04-28 21:21:54,354 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,354 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1272331299]
[2025-04-28 21:21:54,354 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,354 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,406 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 218 statements into 1 equivalence classes.
[2025-04-28 21:21:54,436 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 218 of 218 statements.
[2025-04-28 21:21:54,437 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,437 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,137 INFO  L134       CoverageAnalysis]: Checked inductivity of 62 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 62 trivial. 0 not checked.
[2025-04-28 21:21:55,138 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,139 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1272331299]
[2025-04-28 21:21:55,139 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1272331299] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,139 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,139 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:55,139 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1178271983]
[2025-04-28 21:21:55,139 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,140 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:55,140 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,141 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:55,141 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:55,142 INFO  L87              Difference]: Start difference. First operand 282 states and 310 transitions. Second operand  has 11 states, 8 states have (on average 8.875) internal successors, (71), 11 states have internal predecessors, (71), 5 states have call successors, (43), 1 states have call predecessors, (43), 8 states have return successors, (43), 8 states have call predecessors, (43), 5 states have call successors, (43)
[2025-04-28 21:21:55,303 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,304 INFO  L93              Difference]: Finished difference Result 290 states and 318 transitions.
[2025-04-28 21:21:55,305 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:55,305 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 8 states have (on average 8.875) internal successors, (71), 11 states have internal predecessors, (71), 5 states have call successors, (43), 1 states have call predecessors, (43), 8 states have return successors, (43), 8 states have call predecessors, (43), 5 states have call successors, (43) Word has length 218
[2025-04-28 21:21:55,306 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,309 INFO  L225             Difference]: With dead ends: 290
[2025-04-28 21:21:55,309 INFO  L226             Difference]: Without dead ends: 290
[2025-04-28 21:21:55,309 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:55,310 INFO  L437           NwaCegarLoop]: 292 mSDtfsCounter, 3 mSDsluCounter, 2598 mSDsCounter, 0 mSdLazyCounter, 94 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 2890 SdHoareTripleChecker+Invalid, 94 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 94 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,311 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 2890 Invalid, 94 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 94 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:55,312 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 290 states.
[2025-04-28 21:21:55,324 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 290 to 282.
[2025-04-28 21:21:55,325 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 282 states, 128 states have (on average 1.0) internal successors, (128), 128 states have internal predecessors, (128), 75 states have call successors, (86), 71 states have call predecessors, (86), 78 states have return successors, (96), 82 states have call predecessors, (96), 75 states have call successors, (96)
[2025-04-28 21:21:55,327 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 282 states to 282 states and 310 transitions.
[2025-04-28 21:21:55,327 INFO  L79                 Accepts]: Start accepts. Automaton has 282 states and 310 transitions. Word has length 218
[2025-04-28 21:21:55,329 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,332 INFO  L485      AbstractCegarLoop]: Abstraction has 282 states and 310 transitions.
[2025-04-28 21:21:55,332 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 8 states have (on average 8.875) internal successors, (71), 11 states have internal predecessors, (71), 5 states have call successors, (43), 1 states have call predecessors, (43), 8 states have return successors, (43), 8 states have call predecessors, (43), 5 states have call successors, (43)
[2025-04-28 21:21:55,332 INFO  L278                IsEmpty]: Start isEmpty. Operand 282 states and 310 transitions.
[2025-04-28 21:21:55,336 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 220
[2025-04-28 21:21:55,336 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,337 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,337 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:55,337 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,337 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,338 INFO  L85        PathProgramCache]: Analyzing trace with hash 2029233967, now seen corresponding path program 1 times
[2025-04-28 21:21:55,338 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,338 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [542839442]
[2025-04-28 21:21:55,338 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,338 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,394 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 219 statements into 1 equivalence classes.
[2025-04-28 21:21:55,401 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 219 of 219 statements.
[2025-04-28 21:21:55,402 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,402 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,757 INFO  L134       CoverageAnalysis]: Checked inductivity of 74 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 74 trivial. 0 not checked.
[2025-04-28 21:21:55,757 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,757 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [542839442]
[2025-04-28 21:21:55,757 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [542839442] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,757 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,758 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:55,758 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [223386752]
[2025-04-28 21:21:55,758 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,758 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:55,758 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,759 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:55,759 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:55,759 INFO  L87              Difference]: Start difference. First operand 282 states and 310 transitions. Second operand  has 10 states, 9 states have (on average 7.333333333333333) internal successors, (66), 10 states have internal predecessors, (66), 4 states have call successors, (40), 1 states have call predecessors, (40), 9 states have return successors, (40), 9 states have call predecessors, (40), 4 states have call successors, (40)
[2025-04-28 21:21:55,930 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,930 INFO  L93              Difference]: Finished difference Result 285 states and 314 transitions.
[2025-04-28 21:21:55,931 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:55,931 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 7.333333333333333) internal successors, (66), 10 states have internal predecessors, (66), 4 states have call successors, (40), 1 states have call predecessors, (40), 9 states have return successors, (40), 9 states have call predecessors, (40), 4 states have call successors, (40) Word has length 219
[2025-04-28 21:21:55,933 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,935 INFO  L225             Difference]: With dead ends: 285
[2025-04-28 21:21:55,935 INFO  L226             Difference]: Without dead ends: 285
[2025-04-28 21:21:55,936 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:55,936 INFO  L437           NwaCegarLoop]: 281 mSDtfsCounter, 1 mSDsluCounter, 2228 mSDsCounter, 0 mSdLazyCounter, 115 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 2509 SdHoareTripleChecker+Invalid, 115 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 115 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,937 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 2509 Invalid, 115 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 115 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:55,938 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 285 states.
[2025-04-28 21:21:55,953 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 285 to 285.
[2025-04-28 21:21:55,954 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 285 states, 129 states have (on average 1.0) internal successors, (129), 129 states have internal predecessors, (129), 76 states have call successors, (87), 71 states have call predecessors, (87), 79 states have return successors, (98), 84 states have call predecessors, (98), 76 states have call successors, (98)
[2025-04-28 21:21:55,956 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 285 states to 285 states and 314 transitions.
[2025-04-28 21:21:55,956 INFO  L79                 Accepts]: Start accepts. Automaton has 285 states and 314 transitions. Word has length 219
[2025-04-28 21:21:55,958 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,959 INFO  L485      AbstractCegarLoop]: Abstraction has 285 states and 314 transitions.
[2025-04-28 21:21:55,960 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 7.333333333333333) internal successors, (66), 10 states have internal predecessors, (66), 4 states have call successors, (40), 1 states have call predecessors, (40), 9 states have return successors, (40), 9 states have call predecessors, (40), 4 states have call successors, (40)
[2025-04-28 21:21:55,960 INFO  L278                IsEmpty]: Start isEmpty. Operand 285 states and 314 transitions.
[2025-04-28 21:21:55,963 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 233
[2025-04-28 21:21:55,963 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,963 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,963 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:55,964 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,964 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,964 INFO  L85        PathProgramCache]: Analyzing trace with hash -1814432371, now seen corresponding path program 1 times
[2025-04-28 21:21:55,964 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,964 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1288151339]
[2025-04-28 21:21:55,964 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,965 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,021 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 232 statements into 1 equivalence classes.
[2025-04-28 21:21:56,051 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 232 of 232 statements.
[2025-04-28 21:21:56,055 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,055 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,506 INFO  L134       CoverageAnalysis]: Checked inductivity of 62 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 62 trivial. 0 not checked.
[2025-04-28 21:21:57,506 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,506 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1288151339]
[2025-04-28 21:21:57,506 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1288151339] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:57,506 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:57,507 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [20] imperfect sequences [] total 20
[2025-04-28 21:21:57,507 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [378426726]
[2025-04-28 21:21:57,507 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,507 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:57,507 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,508 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:57,508 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=342, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:57,509 INFO  L87              Difference]: Start difference. First operand 285 states and 314 transitions. Second operand  has 20 states, 16 states have (on average 4.8125) internal successors, (77), 19 states have internal predecessors, (77), 7 states have call successors, (47), 1 states have call predecessors, (47), 16 states have return successors, (47), 17 states have call predecessors, (47), 7 states have call successors, (47)
[2025-04-28 21:21:57,989 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,989 INFO  L93              Difference]: Finished difference Result 301 states and 329 transitions.
[2025-04-28 21:21:57,989 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-04-28 21:21:57,990 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 16 states have (on average 4.8125) internal successors, (77), 19 states have internal predecessors, (77), 7 states have call successors, (47), 1 states have call predecessors, (47), 16 states have return successors, (47), 17 states have call predecessors, (47), 7 states have call successors, (47) Word has length 232
[2025-04-28 21:21:57,990 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,992 INFO  L225             Difference]: With dead ends: 301
[2025-04-28 21:21:57,992 INFO  L226             Difference]: Without dead ends: 283
[2025-04-28 21:21:57,993 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 22 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=46, Invalid=416, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:57,993 INFO  L437           NwaCegarLoop]: 274 mSDtfsCounter, 6 mSDsluCounter, 4623 mSDsCounter, 0 mSdLazyCounter, 359 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 4897 SdHoareTripleChecker+Invalid, 359 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 359 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,994 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 4897 Invalid, 359 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 359 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:57,995 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 283 states.
[2025-04-28 21:21:58,003 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 283 to 283.
[2025-04-28 21:21:58,004 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 283 states, 128 states have (on average 1.0) internal successors, (128), 128 states have internal predecessors, (128), 76 states have call successors, (87), 71 states have call predecessors, (87), 78 states have return successors, (96), 83 states have call predecessors, (96), 76 states have call successors, (96)
[2025-04-28 21:21:58,006 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 283 states to 283 states and 311 transitions.
[2025-04-28 21:21:58,006 INFO  L79                 Accepts]: Start accepts. Automaton has 283 states and 311 transitions. Word has length 232
[2025-04-28 21:21:58,007 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,007 INFO  L485      AbstractCegarLoop]: Abstraction has 283 states and 311 transitions.
[2025-04-28 21:21:58,007 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 16 states have (on average 4.8125) internal successors, (77), 19 states have internal predecessors, (77), 7 states have call successors, (47), 1 states have call predecessors, (47), 16 states have return successors, (47), 17 states have call predecessors, (47), 7 states have call successors, (47)
[2025-04-28 21:21:58,007 INFO  L278                IsEmpty]: Start isEmpty. Operand 283 states and 311 transitions.
[2025-04-28 21:21:58,010 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 233
[2025-04-28 21:21:58,010 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,011 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,011 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:58,011 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,011 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,012 INFO  L85        PathProgramCache]: Analyzing trace with hash 726490364, now seen corresponding path program 1 times
[2025-04-28 21:21:58,012 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,012 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [577554193]
[2025-04-28 21:21:58,012 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,012 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,064 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 232 statements into 1 equivalence classes.
[2025-04-28 21:21:58,085 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 232 of 232 statements.
[2025-04-28 21:21:58,085 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,085 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,978 INFO  L134       CoverageAnalysis]: Checked inductivity of 74 backedges. 12 proven. 0 refuted. 0 times theorem prover too weak. 62 trivial. 0 not checked.
[2025-04-28 21:21:58,979 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,980 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [577554193]
[2025-04-28 21:21:58,980 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [577554193] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:58,980 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:58,980 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [18] imperfect sequences [] total 18
[2025-04-28 21:21:58,980 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [737914808]
[2025-04-28 21:21:58,980 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,981 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:58,981 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,982 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:58,982 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=34, Invalid=272, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:58,982 INFO  L87              Difference]: Start difference. First operand 283 states and 311 transitions. Second operand  has 18 states, 16 states have (on average 4.875) internal successors, (78), 18 states have internal predecessors, (78), 4 states have call successors, (46), 1 states have call predecessors, (46), 16 states have return successors, (49), 16 states have call predecessors, (49), 4 states have call successors, (49)
[2025-04-28 21:21:59,324 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,326 INFO  L93              Difference]: Finished difference Result 295 states and 322 transitions.
[2025-04-28 21:21:59,327 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:21:59,327 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 16 states have (on average 4.875) internal successors, (78), 18 states have internal predecessors, (78), 4 states have call successors, (46), 1 states have call predecessors, (46), 16 states have return successors, (49), 16 states have call predecessors, (49), 4 states have call successors, (49) Word has length 232
[2025-04-28 21:21:59,328 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,329 INFO  L225             Difference]: With dead ends: 295
[2025-04-28 21:21:59,329 INFO  L226             Difference]: Without dead ends: 273
[2025-04-28 21:21:59,330 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 18 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 11 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=34, Invalid=272, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:59,332 INFO  L437           NwaCegarLoop]: 287 mSDtfsCounter, 1 mSDsluCounter, 4264 mSDsCounter, 0 mSdLazyCounter, 281 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 4551 SdHoareTripleChecker+Invalid, 281 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 281 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,332 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 4551 Invalid, 281 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 281 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:59,333 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 273 states.
[2025-04-28 21:21:59,343 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 273 to 273.
[2025-04-28 21:21:59,344 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 273 states, 124 states have (on average 1.0) internal successors, (124), 124 states have internal predecessors, (124), 73 states have call successors, (83), 69 states have call predecessors, (83), 75 states have return successors, (90), 79 states have call predecessors, (90), 73 states have call successors, (90)
[2025-04-28 21:21:59,345 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 273 states to 273 states and 297 transitions.
[2025-04-28 21:21:59,346 INFO  L79                 Accepts]: Start accepts. Automaton has 273 states and 297 transitions. Word has length 232
[2025-04-28 21:21:59,346 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,346 INFO  L485      AbstractCegarLoop]: Abstraction has 273 states and 297 transitions.
[2025-04-28 21:21:59,346 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 16 states have (on average 4.875) internal successors, (78), 18 states have internal predecessors, (78), 4 states have call successors, (46), 1 states have call predecessors, (46), 16 states have return successors, (49), 16 states have call predecessors, (49), 4 states have call successors, (49)
[2025-04-28 21:21:59,346 INFO  L278                IsEmpty]: Start isEmpty. Operand 273 states and 297 transitions.
[2025-04-28 21:21:59,351 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 346
[2025-04-28 21:21:59,351 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,352 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,352 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:59,352 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,353 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,353 INFO  L85        PathProgramCache]: Analyzing trace with hash 1312129742, now seen corresponding path program 1 times
[2025-04-28 21:21:59,353 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,353 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1849652754]
[2025-04-28 21:21:59,353 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,353 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,443 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 345 statements into 1 equivalence classes.
[2025-04-28 21:21:59,465 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 345 of 345 statements.
[2025-04-28 21:21:59,465 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,465 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,865 INFO  L134       CoverageAnalysis]: Checked inductivity of 247 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 243 trivial. 0 not checked.
[2025-04-28 21:21:59,865 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,865 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1849652754]
[2025-04-28 21:21:59,865 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1849652754] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,865 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:59,865 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:59,866 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [65339405]
[2025-04-28 21:21:59,866 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,868 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:59,868 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,868 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:59,869 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:59,869 INFO  L87              Difference]: Start difference. First operand 273 states and 297 transitions. Second operand  has 8 states, 7 states have (on average 11.428571428571429) internal successors, (80), 8 states have internal predecessors, (80), 3 states have call successors, (49), 1 states have call predecessors, (49), 7 states have return successors, (50), 7 states have call predecessors, (50), 3 states have call successors, (50)
[2025-04-28 21:21:59,979 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,979 INFO  L93              Difference]: Finished difference Result 279 states and 306 transitions.
[2025-04-28 21:21:59,979 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:59,980 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 11.428571428571429) internal successors, (80), 8 states have internal predecessors, (80), 3 states have call successors, (49), 1 states have call predecessors, (49), 7 states have return successors, (50), 7 states have call predecessors, (50), 3 states have call successors, (50) Word has length 345
[2025-04-28 21:21:59,980 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,982 INFO  L225             Difference]: With dead ends: 279
[2025-04-28 21:21:59,982 INFO  L226             Difference]: Without dead ends: 279
[2025-04-28 21:21:59,982 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:59,983 INFO  L437           NwaCegarLoop]: 280 mSDtfsCounter, 1 mSDsluCounter, 1662 mSDsCounter, 0 mSdLazyCounter, 69 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1942 SdHoareTripleChecker+Invalid, 69 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 69 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,983 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1942 Invalid, 69 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 69 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:59,984 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 279 states.
[2025-04-28 21:21:59,993 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 279 to 279.
[2025-04-28 21:21:59,993 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 279 states, 127 states have (on average 1.0) internal successors, (127), 127 states have internal predecessors, (127), 73 states have call successors, (83), 69 states have call predecessors, (83), 78 states have return successors, (96), 82 states have call predecessors, (96), 73 states have call successors, (96)
[2025-04-28 21:21:59,995 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 279 states to 279 states and 306 transitions.
[2025-04-28 21:21:59,996 INFO  L79                 Accepts]: Start accepts. Automaton has 279 states and 306 transitions. Word has length 345
[2025-04-28 21:21:59,996 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,996 INFO  L485      AbstractCegarLoop]: Abstraction has 279 states and 306 transitions.
[2025-04-28 21:21:59,997 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 11.428571428571429) internal successors, (80), 8 states have internal predecessors, (80), 3 states have call successors, (49), 1 states have call predecessors, (49), 7 states have return successors, (50), 7 states have call predecessors, (50), 3 states have call successors, (50)
[2025-04-28 21:21:59,997 INFO  L278                IsEmpty]: Start isEmpty. Operand 279 states and 306 transitions.
[2025-04-28 21:22:00,002 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 347
[2025-04-28 21:22:00,002 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,002 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,002 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:22:00,003 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,003 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,003 INFO  L85        PathProgramCache]: Analyzing trace with hash -1449541103, now seen corresponding path program 1 times
[2025-04-28 21:22:00,003 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,003 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [570923373]
[2025-04-28 21:22:00,003 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,004 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,080 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 346 statements into 1 equivalence classes.
[2025-04-28 21:22:00,112 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 346 of 346 statements.
[2025-04-28 21:22:00,112 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,112 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,802 INFO  L134       CoverageAnalysis]: Checked inductivity of 223 backedges. 5 proven. 0 refuted. 0 times theorem prover too weak. 218 trivial. 0 not checked.
[2025-04-28 21:22:00,802 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,802 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [570923373]
[2025-04-28 21:22:00,802 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [570923373] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:00,802 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:00,802 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-04-28 21:22:00,802 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [616369196]
[2025-04-28 21:22:00,802 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,805 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:22:00,805 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,806 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:22:00,806 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=23, Invalid=133, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:22:00,806 INFO  L87              Difference]: Start difference. First operand 279 states and 306 transitions. Second operand  has 13 states, 12 states have (on average 7.333333333333333) internal successors, (88), 13 states have internal predecessors, (88), 3 states have call successors, (53), 1 states have call predecessors, (53), 12 states have return successors, (54), 12 states have call predecessors, (54), 3 states have call successors, (54)
[2025-04-28 21:22:01,048 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,048 INFO  L93              Difference]: Finished difference Result 291 states and 322 transitions.
[2025-04-28 21:22:01,049 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:01,049 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 12 states have (on average 7.333333333333333) internal successors, (88), 13 states have internal predecessors, (88), 3 states have call successors, (53), 1 states have call predecessors, (53), 12 states have return successors, (54), 12 states have call predecessors, (54), 3 states have call successors, (54) Word has length 346
[2025-04-28 21:22:01,050 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,052 INFO  L225             Difference]: With dead ends: 291
[2025-04-28 21:22:01,052 INFO  L226             Difference]: Without dead ends: 291
[2025-04-28 21:22:01,053 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 15 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=133, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:22:01,054 INFO  L437           NwaCegarLoop]: 272 mSDtfsCounter, 1 mSDsluCounter, 2969 mSDsCounter, 0 mSdLazyCounter, 200 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 3241 SdHoareTripleChecker+Invalid, 200 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 200 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,054 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 3241 Invalid, 200 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 200 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:01,055 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 291 states.
[2025-04-28 21:22:01,065 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 291 to 289.
[2025-04-28 21:22:01,066 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 289 states, 132 states have (on average 1.0) internal successors, (132), 132 states have internal predecessors, (132), 73 states have call successors, (83), 69 states have call predecessors, (83), 83 states have return successors, (105), 87 states have call predecessors, (105), 73 states have call successors, (105)
[2025-04-28 21:22:01,069 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 289 states to 289 states and 320 transitions.
[2025-04-28 21:22:01,070 INFO  L79                 Accepts]: Start accepts. Automaton has 289 states and 320 transitions. Word has length 346
[2025-04-28 21:22:01,070 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,070 INFO  L485      AbstractCegarLoop]: Abstraction has 289 states and 320 transitions.
[2025-04-28 21:22:01,071 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 12 states have (on average 7.333333333333333) internal successors, (88), 13 states have internal predecessors, (88), 3 states have call successors, (53), 1 states have call predecessors, (53), 12 states have return successors, (54), 12 states have call predecessors, (54), 3 states have call successors, (54)
[2025-04-28 21:22:01,071 INFO  L278                IsEmpty]: Start isEmpty. Operand 289 states and 320 transitions.
[2025-04-28 21:22:01,076 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 347
[2025-04-28 21:22:01,076 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,077 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,077 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:22:01,077 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,077 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,077 INFO  L85        PathProgramCache]: Analyzing trace with hash 1392496623, now seen corresponding path program 1 times
[2025-04-28 21:22:01,078 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,078 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [43920905]
[2025-04-28 21:22:01,078 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,078 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,154 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 346 statements into 1 equivalence classes.
[2025-04-28 21:22:01,171 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 346 of 346 statements.
[2025-04-28 21:22:01,171 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,171 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,825 INFO  L134       CoverageAnalysis]: Checked inductivity of 223 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 218 trivial. 0 not checked.
[2025-04-28 21:22:01,825 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,825 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [43920905]
[2025-04-28 21:22:01,825 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [43920905] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:01,825 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [675169044]
[2025-04-28 21:22:01,826 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,827 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,830 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:01,837 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:01,840 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,349 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 346 statements into 1 equivalence classes.
[2025-04-28 21:22:02,957 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 346 of 346 statements.
[2025-04-28 21:22:02,957 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,957 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,978 INFO  L256         TraceCheckSpWp]: Trace formula consists of 3167 conjuncts, 43 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:03,010 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:03,192 INFO  L134       CoverageAnalysis]: Checked inductivity of 223 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 218 trivial. 0 not checked.
[2025-04-28 21:22:03,192 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:12,138 INFO  L134       CoverageAnalysis]: Checked inductivity of 223 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 218 trivial. 0 not checked.
[2025-04-28 21:22:12,138 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [675169044] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:12,138 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:12,139 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 14, 13] total 14
[2025-04-28 21:22:12,139 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [470098591]
[2025-04-28 21:22:12,139 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,140 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:22:12,140 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,142 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:22:12,142 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=157, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:22:12,143 INFO  L87              Difference]: Start difference. First operand 289 states and 320 transitions. Second operand  has 14 states, 12 states have (on average 7.416666666666667) internal successors, (89), 14 states have internal predecessors, (89), 5 states have call successors, (54), 1 states have call predecessors, (54), 12 states have return successors, (55), 12 states have call predecessors, (55), 5 states have call successors, (55)
[2025-04-28 21:22:12,388 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,389 INFO  L93              Difference]: Finished difference Result 302 states and 338 transitions.
[2025-04-28 21:22:12,389 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:22:12,390 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 12 states have (on average 7.416666666666667) internal successors, (89), 14 states have internal predecessors, (89), 5 states have call successors, (54), 1 states have call predecessors, (54), 12 states have return successors, (55), 12 states have call predecessors, (55), 5 states have call successors, (55) Word has length 346
[2025-04-28 21:22:12,390 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,393 INFO  L225             Difference]: With dead ends: 302
[2025-04-28 21:22:12,393 INFO  L226             Difference]: Without dead ends: 302
[2025-04-28 21:22:12,393 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 706 GetRequests, 694 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=25, Invalid=157, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:22:12,395 INFO  L437           NwaCegarLoop]: 271 mSDtfsCounter, 2 mSDsluCounter, 3225 mSDsCounter, 0 mSdLazyCounter, 230 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 3496 SdHoareTripleChecker+Invalid, 230 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 230 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,395 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 3496 Invalid, 230 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 230 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:12,396 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 302 states.
[2025-04-28 21:22:12,410 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 302 to 300.
[2025-04-28 21:22:12,410 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 300 states, 137 states have (on average 1.0) internal successors, (137), 137 states have internal predecessors, (137), 74 states have call successors, (84), 69 states have call predecessors, (84), 88 states have return successors, (115), 93 states have call predecessors, (115), 74 states have call successors, (115)
[2025-04-28 21:22:12,412 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 300 states to 300 states and 336 transitions.
[2025-04-28 21:22:12,413 INFO  L79                 Accepts]: Start accepts. Automaton has 300 states and 336 transitions. Word has length 346
[2025-04-28 21:22:12,413 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:12,413 INFO  L485      AbstractCegarLoop]: Abstraction has 300 states and 336 transitions.
[2025-04-28 21:22:12,414 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 12 states have (on average 7.416666666666667) internal successors, (89), 14 states have internal predecessors, (89), 5 states have call successors, (54), 1 states have call predecessors, (54), 12 states have return successors, (55), 12 states have call predecessors, (55), 5 states have call successors, (55)
[2025-04-28 21:22:12,414 INFO  L278                IsEmpty]: Start isEmpty. Operand 300 states and 336 transitions.
[2025-04-28 21:22:12,419 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 346
[2025-04-28 21:22:12,419 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:12,420 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:12,433 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:22:12,625 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable13
[2025-04-28 21:22:12,625 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:12,626 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:12,626 INFO  L85        PathProgramCache]: Analyzing trace with hash -54110048, now seen corresponding path program 1 times
[2025-04-28 21:22:12,626 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:12,626 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [387697723]
[2025-04-28 21:22:12,626 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:12,626 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:12,682 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 345 statements into 1 equivalence classes.
[2025-04-28 21:22:12,700 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 345 of 345 statements.
[2025-04-28 21:22:12,701 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:12,701 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,047 INFO  L134       CoverageAnalysis]: Checked inductivity of 223 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 219 trivial. 0 not checked.
[2025-04-28 21:22:13,047 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,047 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [387697723]
[2025-04-28 21:22:13,047 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [387697723] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:13,047 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:13,047 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:22:13,047 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [981816887]
[2025-04-28 21:22:13,048 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:13,048 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:22:13,048 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:13,049 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:22:13,050 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:13,050 INFO  L87              Difference]: Start difference. First operand 300 states and 336 transitions. Second operand  has 8 states, 7 states have (on average 12.285714285714286) internal successors, (86), 8 states have internal predecessors, (86), 3 states have call successors, (52), 1 states have call predecessors, (52), 7 states have return successors, (53), 7 states have call predecessors, (53), 3 states have call successors, (53)
[2025-04-28 21:22:13,150 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:13,150 INFO  L93              Difference]: Finished difference Result 306 states and 345 transitions.
[2025-04-28 21:22:13,150 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:13,151 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 12.285714285714286) internal successors, (86), 8 states have internal predecessors, (86), 3 states have call successors, (52), 1 states have call predecessors, (52), 7 states have return successors, (53), 7 states have call predecessors, (53), 3 states have call successors, (53) Word has length 345
[2025-04-28 21:22:13,152 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:13,153 INFO  L225             Difference]: With dead ends: 306
[2025-04-28 21:22:13,154 INFO  L226             Difference]: Without dead ends: 306
[2025-04-28 21:22:13,154 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:13,155 INFO  L437           NwaCegarLoop]: 284 mSDtfsCounter, 1 mSDsluCounter, 1684 mSDsCounter, 0 mSdLazyCounter, 69 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1968 SdHoareTripleChecker+Invalid, 69 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 69 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:13,155 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1968 Invalid, 69 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 69 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:13,157 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 306 states.
[2025-04-28 21:22:13,168 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 306 to 300.
[2025-04-28 21:22:13,169 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 300 states, 137 states have (on average 1.0) internal successors, (137), 137 states have internal predecessors, (137), 74 states have call successors, (84), 69 states have call predecessors, (84), 88 states have return successors, (115), 93 states have call predecessors, (115), 74 states have call successors, (115)
[2025-04-28 21:22:13,171 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 300 states to 300 states and 336 transitions.
[2025-04-28 21:22:13,172 INFO  L79                 Accepts]: Start accepts. Automaton has 300 states and 336 transitions. Word has length 345
[2025-04-28 21:22:13,172 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,172 INFO  L485      AbstractCegarLoop]: Abstraction has 300 states and 336 transitions.
[2025-04-28 21:22:13,173 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 12.285714285714286) internal successors, (86), 8 states have internal predecessors, (86), 3 states have call successors, (52), 1 states have call predecessors, (52), 7 states have return successors, (53), 7 states have call predecessors, (53), 3 states have call successors, (53)
[2025-04-28 21:22:13,173 INFO  L278                IsEmpty]: Start isEmpty. Operand 300 states and 336 transitions.
[2025-04-28 21:22:13,178 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 346
[2025-04-28 21:22:13,179 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,179 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:13,179 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:22:13,179 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,180 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,180 INFO  L85        PathProgramCache]: Analyzing trace with hash 39787518, now seen corresponding path program 1 times
[2025-04-28 21:22:13,180 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,180 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [579896553]
[2025-04-28 21:22:13,181 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,181 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,231 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 345 statements into 1 equivalence classes.
[2025-04-28 21:22:13,237 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 345 of 345 statements.
[2025-04-28 21:22:13,237 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,237 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,568 INFO  L134       CoverageAnalysis]: Checked inductivity of 247 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 243 trivial. 0 not checked.
[2025-04-28 21:22:13,568 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,568 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [579896553]
[2025-04-28 21:22:13,568 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [579896553] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:13,568 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:13,568 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:22:13,570 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2081181411]
[2025-04-28 21:22:13,570 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:13,570 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:22:13,570 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:13,571 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:22:13,571 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:13,571 INFO  L87              Difference]: Start difference. First operand 300 states and 336 transitions. Second operand  has 8 states, 7 states have (on average 11.428571428571429) internal successors, (80), 8 states have internal predecessors, (80), 4 states have call successors, (49), 1 states have call predecessors, (49), 7 states have return successors, (50), 7 states have call predecessors, (50), 4 states have call successors, (50)
[2025-04-28 21:22:13,657 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:13,657 INFO  L93              Difference]: Finished difference Result 307 states and 346 transitions.
[2025-04-28 21:22:13,658 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:13,658 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 11.428571428571429) internal successors, (80), 8 states have internal predecessors, (80), 4 states have call successors, (49), 1 states have call predecessors, (49), 7 states have return successors, (50), 7 states have call predecessors, (50), 4 states have call successors, (50) Word has length 345
[2025-04-28 21:22:13,659 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:13,661 INFO  L225             Difference]: With dead ends: 307
[2025-04-28 21:22:13,661 INFO  L226             Difference]: Without dead ends: 304
[2025-04-28 21:22:13,661 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:13,664 INFO  L437           NwaCegarLoop]: 284 mSDtfsCounter, 1 mSDsluCounter, 1686 mSDsCounter, 0 mSdLazyCounter, 61 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 1970 SdHoareTripleChecker+Invalid, 61 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 61 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:13,664 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 1970 Invalid, 61 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 61 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:13,665 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 304 states.
[2025-04-28 21:22:13,679 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 304 to 304.
[2025-04-28 21:22:13,679 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 304 states, 139 states have (on average 1.0) internal successors, (139), 139 states have internal predecessors, (139), 74 states have call successors, (84), 69 states have call predecessors, (84), 90 states have return successors, (119), 95 states have call predecessors, (119), 74 states have call successors, (119)
[2025-04-28 21:22:13,681 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 304 states to 304 states and 342 transitions.
[2025-04-28 21:22:13,682 INFO  L79                 Accepts]: Start accepts. Automaton has 304 states and 342 transitions. Word has length 345
[2025-04-28 21:22:13,682 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,682 INFO  L485      AbstractCegarLoop]: Abstraction has 304 states and 342 transitions.
[2025-04-28 21:22:13,683 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 11.428571428571429) internal successors, (80), 8 states have internal predecessors, (80), 4 states have call successors, (49), 1 states have call predecessors, (49), 7 states have return successors, (50), 7 states have call predecessors, (50), 4 states have call successors, (50)
[2025-04-28 21:22:13,683 INFO  L278                IsEmpty]: Start isEmpty. Operand 304 states and 342 transitions.
[2025-04-28 21:22:13,686 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 347
[2025-04-28 21:22:13,686 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,687 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:13,687 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:22:13,687 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,687 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,688 INFO  L85        PathProgramCache]: Analyzing trace with hash -1658890881, now seen corresponding path program 1 times
[2025-04-28 21:22:13,688 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,688 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1550407894]
[2025-04-28 21:22:13,688 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,688 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,737 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 346 statements into 1 equivalence classes.
[2025-04-28 21:22:13,751 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 346 of 346 statements.
[2025-04-28 21:22:13,751 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,751 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:14,454 INFO  L134       CoverageAnalysis]: Checked inductivity of 247 backedges. 5 proven. 0 refuted. 0 times theorem prover too weak. 242 trivial. 0 not checked.
[2025-04-28 21:22:14,455 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:14,455 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1550407894]
[2025-04-28 21:22:14,455 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1550407894] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:14,455 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:14,455 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-04-28 21:22:14,455 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1731127538]
[2025-04-28 21:22:14,455 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:14,456 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:22:14,456 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:14,457 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:22:14,458 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=23, Invalid=133, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:22:14,458 INFO  L87              Difference]: Start difference. First operand 304 states and 342 transitions. Second operand  has 13 states, 12 states have (on average 6.833333333333333) internal successors, (82), 13 states have internal predecessors, (82), 4 states have call successors, (50), 1 states have call predecessors, (50), 12 states have return successors, (51), 12 states have call predecessors, (51), 4 states have call successors, (51)
[2025-04-28 21:22:14,679 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:14,679 INFO  L93              Difference]: Finished difference Result 307 states and 345 transitions.
[2025-04-28 21:22:14,679 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:14,680 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 12 states have (on average 6.833333333333333) internal successors, (82), 13 states have internal predecessors, (82), 4 states have call successors, (50), 1 states have call predecessors, (50), 12 states have return successors, (51), 12 states have call predecessors, (51), 4 states have call successors, (51) Word has length 346
[2025-04-28 21:22:14,681 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:14,683 INFO  L225             Difference]: With dead ends: 307
[2025-04-28 21:22:14,684 INFO  L226             Difference]: Without dead ends: 304
[2025-04-28 21:22:14,684 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 15 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=133, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:22:14,685 INFO  L437           NwaCegarLoop]: 271 mSDtfsCounter, 1 mSDsluCounter, 2959 mSDsCounter, 0 mSdLazyCounter, 187 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 3230 SdHoareTripleChecker+Invalid, 187 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 187 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:14,685 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 3230 Invalid, 187 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 187 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:14,686 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 304 states.
[2025-04-28 21:22:14,705 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 304 to 304.
[2025-04-28 21:22:14,707 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 304 states, 139 states have (on average 1.0) internal successors, (139), 139 states have internal predecessors, (139), 74 states have call successors, (84), 69 states have call predecessors, (84), 90 states have return successors, (118), 95 states have call predecessors, (118), 74 states have call successors, (118)
[2025-04-28 21:22:14,710 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 304 states to 304 states and 341 transitions.
[2025-04-28 21:22:14,710 INFO  L79                 Accepts]: Start accepts. Automaton has 304 states and 341 transitions. Word has length 346
[2025-04-28 21:22:14,711 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:14,711 INFO  L485      AbstractCegarLoop]: Abstraction has 304 states and 341 transitions.
[2025-04-28 21:22:14,711 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 12 states have (on average 6.833333333333333) internal successors, (82), 13 states have internal predecessors, (82), 4 states have call successors, (50), 1 states have call predecessors, (50), 12 states have return successors, (51), 12 states have call predecessors, (51), 4 states have call successors, (51)
[2025-04-28 21:22:14,711 INFO  L278                IsEmpty]: Start isEmpty. Operand 304 states and 341 transitions.
[2025-04-28 21:22:14,717 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 347
[2025-04-28 21:22:14,717 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:14,718 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:14,718 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:22:14,718 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:14,718 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:14,719 INFO  L85        PathProgramCache]: Analyzing trace with hash -1454014479, now seen corresponding path program 1 times
[2025-04-28 21:22:14,719 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:14,719 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [755626490]
[2025-04-28 21:22:14,719 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:14,719 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:14,781 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 346 statements into 1 equivalence classes.
[2025-04-28 21:22:14,793 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 346 of 346 statements.
[2025-04-28 21:22:14,793 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:14,794 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:15,371 INFO  L134       CoverageAnalysis]: Checked inductivity of 223 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 218 trivial. 0 not checked.
[2025-04-28 21:22:15,371 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:15,371 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [755626490]
[2025-04-28 21:22:15,372 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [755626490] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:15,372 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1482946804]
[2025-04-28 21:22:15,372 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:15,372 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:15,374 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:15,377 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:15,381 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
