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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:18,844 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:18,981 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_10522880-2370-45fd-9755-1369ef7424b8/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:18,987 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:18,989 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:19,030 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:19,032 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:19,032 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:19,033 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:19,034 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:19,034 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:19,035 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:19,035 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:19,035 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:19,037 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:19,037 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:19,037 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:19,038 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:19,038 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:19,038 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:19,038 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:19,038 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:19,038 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:19,038 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:19,038 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:19,040 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:19,040 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:19,426 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:19,440 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:19,443 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:19,447 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:19,447 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:19,449 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_10522880-2370-45fd-9755-1369ef7424b8/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-263.smt2
[2025-04-28 21:21:19,452 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:19,457 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:19,982 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_10522880-2370-45fd-9755-1369ef7424b8/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-263.smt2
[2025-04-28 21:21:19,988 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:19,990 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:19,992 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:19,992 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:19,993 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:19,999 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:20,047 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20 Unit
[2025-04-28 21:21:20,048 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:20,050 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:20,050 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:20,050 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:20,073 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,073 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,127 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,127 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,140 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,141 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,144 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,147 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,149 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,175 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:20,176 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:20,176 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:20,176 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:20,177 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (1/1) ...
[2025-04-28 21:21:20,180 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:20,195 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:20,212 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:20,218 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:20,236 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:20,237 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:20,237 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:20,237 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:20,237 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:20,237 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:20,237 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:20,237 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH0.CLN Main.java, line 23
[2025-04-28 21:21:20,237 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH0.CLN Main.java, line 23
[2025-04-28 21:21:20,237 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_8 given in one single declaration
[2025-04-28 21:21:20,238 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_8
[2025-04-28 21:21:20,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_8
[2025-04-28 21:21:20,238 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_7 given in one single declaration
[2025-04-28 21:21:20,238 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_7
[2025-04-28 21:21:20,238 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_7
[2025-04-28 21:21:20,238 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_6 given in one single declaration
[2025-04-28 21:21:20,240 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_6
[2025-04-28 21:21:20,241 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_6
[2025-04-28 21:21:20,241 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_5 given in one single declaration
[2025-04-28 21:21:20,241 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_5
[2025-04-28 21:21:20,241 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_5
[2025-04-28 21:21:20,241 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_post given in one single declaration
[2025-04-28 21:21:20,241 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_post
[2025-04-28 21:21:20,241 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_post
[2025-04-28 21:21:20,241 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block0 given in one single declaration
[2025-04-28 21:21:20,242 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block0
[2025-04-28 21:21:20,242 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block0
[2025-04-28 21:21:20,242 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:20,242 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:20,242 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:20,242 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:20,242 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:20,242 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:20,242 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1 given in one single declaration
[2025-04-28 21:21:20,242 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_Block1
[2025-04-28 21:21:20,242 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_Block1
[2025-04-28 21:21:20,243 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <JayHornAssertions.CLN void <clinit>()>_pre given in one single declaration
[2025-04-28 21:21:20,243 INFO  L130     BoogieDeclarations]: Found specification of procedure <JayHornAssertions.CLN void <clinit>()>_pre
[2025-04-28 21:21:20,243 INFO  L138     BoogieDeclarations]: Found implementation of procedure <JayHornAssertions.CLN void <clinit>()>_pre
[2025-04-28 21:21:20,243 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_4 given in one single declaration
[2025-04-28 21:21:20,243 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_4
[2025-04-28 21:21:20,243 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_4
[2025-04-28 21:21:20,243 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_post given in one single declaration
[2025-04-28 21:21:20,243 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_post
[2025-04-28 21:21:20,243 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_post
[2025-04-28 21:21:20,243 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block0 given in one single declaration
[2025-04-28 21:21:20,244 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block0
[2025-04-28 21:21:20,244 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block0
[2025-04-28 21:21:20,244 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1_3 given in one single declaration
[2025-04-28 21:21:20,244 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1_3
[2025-04-28 21:21:20,244 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1_3
[2025-04-28 21:21:20,244 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1_2 given in one single declaration
[2025-04-28 21:21:20,245 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:20,246 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1_2
[2025-04-28 21:21:20,246 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1_1 given in one single declaration
[2025-04-28 21:21:20,246 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:20,246 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1_1
[2025-04-28 21:21:20,247 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_Block1 given in one single declaration
[2025-04-28 21:21:20,247 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_Block1
[2025-04-28 21:21:20,247 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_Block1
[2025-04-28 21:21:20,248 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void <clinit>()>_pre given in one single declaration
[2025-04-28 21:21:20,248 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void <clinit>()>_pre
[2025-04-28 21:21:20,248 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void <clinit>()>_pre
[2025-04-28 21:21:20,249 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_3 given in one single declaration
[2025-04-28 21:21:20,249 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_3
[2025-04-28 21:21:20,249 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_3
[2025-04-28 21:21:20,249 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_2 given in one single declaration
[2025-04-28 21:21:20,249 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_2
[2025-04-28 21:21:20,249 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_2
[2025-04-28 21:21:20,249 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_1 given in one single declaration
[2025-04-28 21:21:20,249 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_1
[2025-04-28 21:21:20,249 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_1
[2025-04-28 21:21:20,249 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1 given in one single declaration
[2025-04-28 21:21:20,250 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1
[2025-04-28 21:21:20,250 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1
[2025-04-28 21:21:20,250 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:20,250 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:20,250 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_pre
[2025-04-28 21:21:20,250 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:20,250 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH1.CLN Main.java, line 24
[2025-04-28 21:21:20,251 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH1.CLN Main.java, line 24
[2025-04-28 21:21:20,251 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_12 given in one single declaration
[2025-04-28 21:21:20,251 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_12
[2025-04-28 21:21:20,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_12
[2025-04-28 21:21:20,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_11 given in one single declaration
[2025-04-28 21:21:20,252 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_11
[2025-04-28 21:21:20,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_11
[2025-04-28 21:21:20,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_10 given in one single declaration
[2025-04-28 21:21:20,252 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_10
[2025-04-28 21:21:20,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_10
[2025-04-28 21:21:20,252 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_9 given in one single declaration
[2025-04-28 21:21:20,252 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_9
[2025-04-28 21:21:20,252 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_9
[2025-04-28 21:21:20,252 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:20,252 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH3.CLN Main.java, line 29
[2025-04-28 21:21:20,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH3.CLN Main.java, line 29
[2025-04-28 21:21:20,253 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:20,253 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5
[2025-04-28 21:21:20,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block5
[2025-04-28 21:21:20,253 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:20,253 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block4
[2025-04-28 21:21:20,253 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block4
[2025-04-28 21:21:20,253 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:20,253 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3
[2025-04-28 21:21:20,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block3
[2025-04-28 21:21:20,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_16 given in one single declaration
[2025-04-28 21:21:20,254 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_16
[2025-04-28 21:21:20,254 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_16
[2025-04-28 21:21:20,254 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_15 given in one single declaration
[2025-04-28 21:21:20,254 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_15
[2025-04-28 21:21:20,255 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_15
[2025-04-28 21:21:20,255 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_14 given in one single declaration
[2025-04-28 21:21:20,255 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_14
[2025-04-28 21:21:20,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_14
[2025-04-28 21:21:20,256 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:20,256 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_post
[2025-04-28 21:21:20,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_post
[2025-04-28 21:21:20,256 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:20,256 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block0
[2025-04-28 21:21:20,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block0
[2025-04-28 21:21:20,256 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:20,256 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block8_1
[2025-04-28 21:21:20,256 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block8_1
[2025-04-28 21:21:20,256 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:20,256 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block8
[2025-04-28 21:21:20,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block8
[2025-04-28 21:21:20,257 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:20,257 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block4_3
[2025-04-28 21:21:20,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block4_3
[2025-04-28 21:21:20,257 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:20,257 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block4_2
[2025-04-28 21:21:20,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block4_2
[2025-04-28 21:21:20,257 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:20,257 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block4_1
[2025-04-28 21:21:20,257 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block4_1
[2025-04-28 21:21:20,257 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:20,257 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block4
[2025-04-28 21:21:20,258 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block4
[2025-04-28 21:21:20,258 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:20,258 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block2
[2025-04-28 21:21:20,258 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block2
[2025-04-28 21:21:20,258 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:20,258 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block1_3
[2025-04-28 21:21:20,258 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block1_3
[2025-04-28 21:21:20,258 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:20,258 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block1_2
[2025-04-28 21:21:20,258 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block1_2
[2025-04-28 21:21:20,258 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:20,259 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block1_1
[2025-04-28 21:21:20,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block1_1
[2025-04-28 21:21:20,259 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:20,259 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block1
[2025-04-28 21:21:20,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block1
[2025-04-28 21:21:20,259 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:20,259 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_pre
[2025-04-28 21:21:20,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_pre
[2025-04-28 21:21:20,259 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:20,259 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block5_2
[2025-04-28 21:21:20,259 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block5_2
[2025-04-28 21:21:20,260 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:20,260 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block5_1
[2025-04-28 21:21:20,260 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block5_1
[2025-04-28 21:21:20,260 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:20,260 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block5
[2025-04-28 21:21:20,260 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block5
[2025-04-28 21:21:20,260 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:20,263 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block7_1
[2025-04-28 21:21:20,263 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block7_1
[2025-04-28 21:21:20,264 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:20,264 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block7
[2025-04-28 21:21:20,264 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block7
[2025-04-28 21:21:20,264 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:20,264 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block5_3
[2025-04-28 21:21:20,264 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block5_3
[2025-04-28 21:21:20,264 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:20,264 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block3_1
[2025-04-28 21:21:20,264 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block3_1
[2025-04-28 21:21:20,265 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:20,265 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block3
[2025-04-28 21:21:20,265 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block3
[2025-04-28 21:21:20,265 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:20,265 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block9_1
[2025-04-28 21:21:20,265 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block9_1
[2025-04-28 21:21:20,266 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:20,266 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block9
[2025-04-28 21:21:20,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block9
[2025-04-28 21:21:20,266 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:20,266 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block6_1
[2025-04-28 21:21:20,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block6_1
[2025-04-28 21:21:20,266 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:20,266 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN int addition(int,int)>_Block6
[2025-04-28 21:21:20,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN int addition(int,int)>_Block6
[2025-04-28 21:21:20,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_13 given in one single declaration
[2025-04-28 21:21:20,266 INFO  L130     BoogieDeclarations]: Found specification of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_13
[2025-04-28 21:21:20,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure <Main.CLN void main(JayArray_java_lang_String)>_Block1_13
[2025-04-28 21:21:20,267 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:20,267 INFO  L130     BoogieDeclarations]: Found specification of procedure Assert .HSH2.CLN Main.java, line 25
[2025-04-28 21:21:20,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure Assert .HSH2.CLN Main.java, line 25
[2025-04-28 21:21:20,267 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:20,267 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:20,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:20,513 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:20,517 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:21,017 INFO  L?                        ?]: Removed 28 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:21,017 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:21,045 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:21,046 INFO  L312             CfgBuilder]: Removed 35 assume(true) statements.
[2025-04-28 21:21:21,047 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:21 BoogieIcfgContainer
[2025-04-28 21:21:21,048 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:21,050 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:21,052 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:21,057 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:21,057 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/3) ...
[2025-04-28 21:21:21,059 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@23bb8dde and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:21, skipping insertion in model container
[2025-04-28 21:21:21,059 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:20" (2/3) ...
[2025-04-28 21:21:21,059 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@23bb8dde and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:21, skipping insertion in model container
[2025-04-28 21:21:21,060 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:21" (3/3) ...
[2025-04-28 21:21:21,062 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:21,079 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:21,082 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 67 procedures, 247 locations, 349 edges, 67 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:21,142 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:21,159 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;@136ebbb8, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:21,159 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:21,166 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 247 states, 108 states have (on average 1.0092592592592593) internal successors, (109), 109 states have internal predecessors, (109), 71 states have call successors, (80), 66 states have call predecessors, (80), 66 states have return successors, (80), 71 states have call predecessors, (80), 71 states have call successors, (80)
[2025-04-28 21:21:21,194 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 177
[2025-04-28 21:21:21,196 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,197 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 2, 2, 2, 2, 2, 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]
[2025-04-28 21:21:21,198 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,205 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,205 INFO  L85        PathProgramCache]: Analyzing trace with hash -1907327729, now seen corresponding path program 1 times
[2025-04-28 21:21:21,215 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,216 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [937897788]
[2025-04-28 21:21:21,216 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,217 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,330 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 176 statements into 1 equivalence classes.
[2025-04-28 21:21:21,492 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 176 of 176 statements.
[2025-04-28 21:21:21,492 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,493 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,005 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 136 trivial. 0 not checked.
[2025-04-28 21:21:23,006 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,006 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [937897788]
[2025-04-28 21:21:23,007 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [937897788] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:23,007 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:23,010 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:23,012 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1184680156]
[2025-04-28 21:21:23,013 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:23,020 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:23,020 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:23,063 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:23,065 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=90, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:23,069 INFO  L87              Difference]: Start difference. First operand  has 247 states, 108 states have (on average 1.0092592592592593) internal successors, (109), 109 states have internal predecessors, (109), 71 states have call successors, (80), 66 states have call predecessors, (80), 66 states have return successors, (80), 71 states have call predecessors, (80), 71 states have call successors, (80) Second operand  has 11 states, 9 states have (on average 4.444444444444445) internal successors, (40), 11 states have internal predecessors, (40), 4 states have call successors, (28), 1 states have call predecessors, (28), 9 states have return successors, (28), 9 states have call predecessors, (28), 4 states have call successors, (28)
[2025-04-28 21:21:23,391 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,391 INFO  L93              Difference]: Finished difference Result 243 states and 264 transitions.
[2025-04-28 21:21:23,393 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:23,395 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 9 states have (on average 4.444444444444445) internal successors, (40), 11 states have internal predecessors, (40), 4 states have call successors, (28), 1 states have call predecessors, (28), 9 states have return successors, (28), 9 states have call predecessors, (28), 4 states have call successors, (28) Word has length 176
[2025-04-28 21:21:23,397 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,418 INFO  L225             Difference]: With dead ends: 243
[2025-04-28 21:21:23,418 INFO  L226             Difference]: Without dead ends: 241
[2025-04-28 21:21:23,420 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=20, Invalid=90, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:23,427 INFO  L437           NwaCegarLoop]: 257 mSDtfsCounter, 0 mSDsluCounter, 2037 mSDsCounter, 0 mSdLazyCounter, 66 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 2294 SdHoareTripleChecker+Invalid, 66 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 66 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,432 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 2294 Invalid, 66 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 66 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:23,452 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 241 states.
[2025-04-28 21:21:23,511 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 241 to 241.
[2025-04-28 21:21:23,513 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 241 states, 105 states have (on average 1.0) internal successors, (105), 105 states have internal predecessors, (105), 70 states have call successors, (78), 65 states have call predecessors, (78), 65 states have return successors, (78), 70 states have call predecessors, (78), 70 states have call successors, (78)
[2025-04-28 21:21:23,523 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 241 states to 241 states and 261 transitions.
[2025-04-28 21:21:23,528 INFO  L79                 Accepts]: Start accepts. Automaton has 241 states and 261 transitions. Word has length 176
[2025-04-28 21:21:23,529 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,531 INFO  L485      AbstractCegarLoop]: Abstraction has 241 states and 261 transitions.
[2025-04-28 21:21:23,531 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 9 states have (on average 4.444444444444445) internal successors, (40), 11 states have internal predecessors, (40), 4 states have call successors, (28), 1 states have call predecessors, (28), 9 states have return successors, (28), 9 states have call predecessors, (28), 4 states have call successors, (28)
[2025-04-28 21:21:23,532 INFO  L278                IsEmpty]: Start isEmpty. Operand 241 states and 261 transitions.
[2025-04-28 21:21:23,539 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 191
[2025-04-28 21:21:23,539 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,539 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 2, 2, 2, 2, 2, 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]
[2025-04-28 21:21:23,539 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:23,543 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,543 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,543 INFO  L85        PathProgramCache]: Analyzing trace with hash 144239544, now seen corresponding path program 1 times
[2025-04-28 21:21:23,544 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,544 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [11308128]
[2025-04-28 21:21:23,544 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,544 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,612 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 190 statements into 1 equivalence classes.
[2025-04-28 21:21:23,662 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 190 of 190 statements.
[2025-04-28 21:21:23,665 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,666 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,624 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 136 trivial. 0 not checked.
[2025-04-28 21:21:24,624 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,626 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [11308128]
[2025-04-28 21:21:24,626 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [11308128] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:24,626 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:24,626 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [15] imperfect sequences [] total 15
[2025-04-28 21:21:24,626 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [680001475]
[2025-04-28 21:21:24,627 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:24,628 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:24,630 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:24,630 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:24,631 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=182, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:24,631 INFO  L87              Difference]: Start difference. First operand 241 states and 261 transitions. Second operand  has 15 states, 13 states have (on average 3.5384615384615383) internal successors, (46), 15 states have internal predecessors, (46), 4 states have call successors, (32), 1 states have call predecessors, (32), 13 states have return successors, (32), 13 states have call predecessors, (32), 4 states have call successors, (32)
[2025-04-28 21:21:24,916 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:24,916 INFO  L93              Difference]: Finished difference Result 239 states and 258 transitions.
[2025-04-28 21:21:24,917 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:24,917 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 13 states have (on average 3.5384615384615383) internal successors, (46), 15 states have internal predecessors, (46), 4 states have call successors, (32), 1 states have call predecessors, (32), 13 states have return successors, (32), 13 states have call predecessors, (32), 4 states have call successors, (32) Word has length 190
[2025-04-28 21:21:24,918 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:24,921 INFO  L225             Difference]: With dead ends: 239
[2025-04-28 21:21:24,921 INFO  L226             Difference]: Without dead ends: 237
[2025-04-28 21:21:24,921 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 15 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=28, Invalid=182, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:24,922 INFO  L437           NwaCegarLoop]: 247 mSDtfsCounter, 0 mSDsluCounter, 2936 mSDsCounter, 0 mSdLazyCounter, 147 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 3183 SdHoareTripleChecker+Invalid, 147 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 147 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:24,923 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 3183 Invalid, 147 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 147 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:24,924 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 237 states.
[2025-04-28 21:21:24,939 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 237 to 237.
[2025-04-28 21:21:24,940 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 237 states, 103 states have (on average 1.0) internal successors, (103), 103 states have internal predecessors, (103), 69 states have call successors, (76), 64 states have call predecessors, (76), 64 states have return successors, (76), 69 states have call predecessors, (76), 69 states have call successors, (76)
[2025-04-28 21:21:24,942 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 237 states to 237 states and 255 transitions.
[2025-04-28 21:21:24,942 INFO  L79                 Accepts]: Start accepts. Automaton has 237 states and 255 transitions. Word has length 190
[2025-04-28 21:21:24,943 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:24,943 INFO  L485      AbstractCegarLoop]: Abstraction has 237 states and 255 transitions.
[2025-04-28 21:21:24,943 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 13 states have (on average 3.5384615384615383) internal successors, (46), 15 states have internal predecessors, (46), 4 states have call successors, (32), 1 states have call predecessors, (32), 13 states have return successors, (32), 13 states have call predecessors, (32), 4 states have call successors, (32)
[2025-04-28 21:21:24,943 INFO  L278                IsEmpty]: Start isEmpty. Operand 237 states and 255 transitions.
[2025-04-28 21:21:24,952 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 416
[2025-04-28 21:21:24,952 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,953 INFO  L218           NwaCegarLoop]: trace histogram [8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 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]
[2025-04-28 21:21:24,953 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:24,953 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,954 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,954 INFO  L85        PathProgramCache]: Analyzing trace with hash 309430077, now seen corresponding path program 1 times
[2025-04-28 21:21:24,954 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,954 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [236596604]
[2025-04-28 21:21:24,955 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,955 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,108 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 415 statements into 1 equivalence classes.
[2025-04-28 21:21:25,194 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 415 of 415 statements.
[2025-04-28 21:21:25,195 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,195 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,195 INFO  L134       CoverageAnalysis]: Checked inductivity of 725 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 725 trivial. 0 not checked.
[2025-04-28 21:21:26,196 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,196 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [236596604]
[2025-04-28 21:21:26,197 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [236596604] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:26,197 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:26,198 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [12] imperfect sequences [] total 12
[2025-04-28 21:21:26,198 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1694455160]
[2025-04-28 21:21:26,198 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,199 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:26,199 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,200 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:26,200 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=22, Invalid=110, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:26,201 INFO  L87              Difference]: Start difference. First operand 237 states and 255 transitions. Second operand  has 12 states, 10 states have (on average 6.5) internal successors, (65), 12 states have internal predecessors, (65), 4 states have call successors, (45), 1 states have call predecessors, (45), 10 states have return successors, (45), 10 states have call predecessors, (45), 4 states have call successors, (45)
[2025-04-28 21:21:26,405 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,405 INFO  L93              Difference]: Finished difference Result 245 states and 265 transitions.
[2025-04-28 21:21:26,406 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:26,406 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 10 states have (on average 6.5) internal successors, (65), 12 states have internal predecessors, (65), 4 states have call successors, (45), 1 states have call predecessors, (45), 10 states have return successors, (45), 10 states have call predecessors, (45), 4 states have call successors, (45) Word has length 415
[2025-04-28 21:21:26,408 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,412 INFO  L225             Difference]: With dead ends: 245
[2025-04-28 21:21:26,413 INFO  L226             Difference]: Without dead ends: 245
[2025-04-28 21:21:26,414 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=22, Invalid=110, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:26,415 INFO  L437           NwaCegarLoop]: 243 mSDtfsCounter, 2 mSDsluCounter, 2168 mSDsCounter, 0 mSdLazyCounter, 126 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 2411 SdHoareTripleChecker+Invalid, 126 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 126 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,416 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 2411 Invalid, 126 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 126 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:26,420 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 245 states.
[2025-04-28 21:21:26,453 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 245 to 245.
[2025-04-28 21:21:26,457 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 245 states, 107 states have (on average 1.0) internal successors, (107), 107 states have internal predecessors, (107), 69 states have call successors, (76), 64 states have call predecessors, (76), 68 states have return successors, (82), 73 states have call predecessors, (82), 69 states have call successors, (82)
[2025-04-28 21:21:26,460 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 245 states to 245 states and 265 transitions.
[2025-04-28 21:21:26,463 INFO  L79                 Accepts]: Start accepts. Automaton has 245 states and 265 transitions. Word has length 415
[2025-04-28 21:21:26,464 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,466 INFO  L485      AbstractCegarLoop]: Abstraction has 245 states and 265 transitions.
[2025-04-28 21:21:26,467 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 10 states have (on average 6.5) internal successors, (65), 12 states have internal predecessors, (65), 4 states have call successors, (45), 1 states have call predecessors, (45), 10 states have return successors, (45), 10 states have call predecessors, (45), 4 states have call successors, (45)
[2025-04-28 21:21:26,467 INFO  L278                IsEmpty]: Start isEmpty. Operand 245 states and 265 transitions.
[2025-04-28 21:21:26,481 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 430
[2025-04-28 21:21:26,481 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,482 INFO  L218           NwaCegarLoop]: trace histogram [8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 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]
[2025-04-28 21:21:26,482 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:26,482 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,484 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,484 INFO  L85        PathProgramCache]: Analyzing trace with hash 723913511, now seen corresponding path program 1 times
[2025-04-28 21:21:26,485 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,485 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [480270062]
[2025-04-28 21:21:26,486 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,486 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,605 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 429 statements into 1 equivalence classes.
[2025-04-28 21:21:26,697 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 429 of 429 statements.
[2025-04-28 21:21:26,697 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,697 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,503 INFO  L134       CoverageAnalysis]: Checked inductivity of 725 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 725 trivial. 0 not checked.
[2025-04-28 21:21:27,504 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,504 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [480270062]
[2025-04-28 21:21:27,504 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [480270062] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,504 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,504 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:27,505 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [398214181]
[2025-04-28 21:21:27,505 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,506 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:27,507 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,512 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:27,513 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:27,514 INFO  L87              Difference]: Start difference. First operand 245 states and 265 transitions. Second operand  has 11 states, 10 states have (on average 7.1) internal successors, (71), 11 states have internal predecessors, (71), 3 states have call successors, (49), 1 states have call predecessors, (49), 10 states have return successors, (49), 10 states have call predecessors, (49), 3 states have call successors, (49)
[2025-04-28 21:21:27,703 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,704 INFO  L93              Difference]: Finished difference Result 249 states and 268 transitions.
[2025-04-28 21:21:27,704 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:27,705 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 10 states have (on average 7.1) internal successors, (71), 11 states have internal predecessors, (71), 3 states have call successors, (49), 1 states have call predecessors, (49), 10 states have return successors, (49), 10 states have call predecessors, (49), 3 states have call successors, (49) Word has length 429
[2025-04-28 21:21:27,706 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,711 INFO  L225             Difference]: With dead ends: 249
[2025-04-28 21:21:27,711 INFO  L226             Difference]: Without dead ends: 241
[2025-04-28 21:21:27,712 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:27,712 INFO  L437           NwaCegarLoop]: 245 mSDtfsCounter, 1 mSDsluCounter, 2190 mSDsCounter, 0 mSdLazyCounter, 106 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 2435 SdHoareTripleChecker+Invalid, 106 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 106 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,713 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 2435 Invalid, 106 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 106 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:27,714 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 241 states.
[2025-04-28 21:21:27,732 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 241 to 241.
[2025-04-28 21:21:27,737 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 241 states, 105 states have (on average 1.0) internal successors, (105), 105 states have internal predecessors, (105), 69 states have call successors, (76), 64 states have call predecessors, (76), 66 states have return successors, (79), 71 states have call predecessors, (79), 69 states have call successors, (79)
[2025-04-28 21:21:27,742 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 241 states to 241 states and 260 transitions.
[2025-04-28 21:21:27,742 INFO  L79                 Accepts]: Start accepts. Automaton has 241 states and 260 transitions. Word has length 429
[2025-04-28 21:21:27,744 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,747 INFO  L485      AbstractCegarLoop]: Abstraction has 241 states and 260 transitions.
[2025-04-28 21:21:27,748 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 10 states have (on average 7.1) internal successors, (71), 11 states have internal predecessors, (71), 3 states have call successors, (49), 1 states have call predecessors, (49), 10 states have return successors, (49), 10 states have call predecessors, (49), 3 states have call successors, (49)
[2025-04-28 21:21:27,748 INFO  L278                IsEmpty]: Start isEmpty. Operand 241 states and 260 transitions.
[2025-04-28 21:21:27,769 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 650
[2025-04-28 21:21:27,769 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,770 INFO  L218           NwaCegarLoop]: trace histogram [12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-04-28 21:21:27,770 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:27,770 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,771 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,771 INFO  L85        PathProgramCache]: Analyzing trace with hash -1713226498, now seen corresponding path program 1 times
[2025-04-28 21:21:27,772 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,772 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1861796903]
[2025-04-28 21:21:27,772 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,772 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,943 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 649 statements into 1 equivalence classes.
[2025-04-28 21:21:28,010 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 649 of 649 statements.
[2025-04-28 21:21:28,010 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,011 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,105 INFO  L134       CoverageAnalysis]: Checked inductivity of 1792 backedges. 9 proven. 0 refuted. 0 times theorem prover too weak. 1783 trivial. 0 not checked.
[2025-04-28 21:21:29,107 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,107 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1861796903]
[2025-04-28 21:21:29,107 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1861796903] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,107 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:29,108 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:29,108 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1596420452]
[2025-04-28 21:21:29,108 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,109 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:29,110 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,111 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:29,112 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:29,112 INFO  L87              Difference]: Start difference. First operand 241 states and 260 transitions. Second operand  has 10 states, 9 states have (on average 9.222222222222221) internal successors, (83), 10 states have internal predecessors, (83), 3 states have call successors, (55), 1 states have call predecessors, (55), 9 states have return successors, (57), 9 states have call predecessors, (57), 3 states have call successors, (57)
[2025-04-28 21:21:29,276 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,278 INFO  L93              Difference]: Finished difference Result 243 states and 262 transitions.
[2025-04-28 21:21:29,279 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:29,279 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 9.222222222222221) internal successors, (83), 10 states have internal predecessors, (83), 3 states have call successors, (55), 1 states have call predecessors, (55), 9 states have return successors, (57), 9 states have call predecessors, (57), 3 states have call successors, (57) Word has length 649
[2025-04-28 21:21:29,281 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,285 INFO  L225             Difference]: With dead ends: 243
[2025-04-28 21:21:29,285 INFO  L226             Difference]: Without dead ends: 243
[2025-04-28 21:21:29,286 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:29,291 INFO  L437           NwaCegarLoop]: 245 mSDtfsCounter, 1 mSDsluCounter, 1941 mSDsCounter, 0 mSdLazyCounter, 96 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 2186 SdHoareTripleChecker+Invalid, 96 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 96 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,291 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 2186 Invalid, 96 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 96 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:29,292 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 243 states.
[2025-04-28 21:21:29,313 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 243 to 243.
[2025-04-28 21:21:29,314 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 243 states, 106 states have (on average 1.0) internal successors, (106), 106 states have internal predecessors, (106), 69 states have call successors, (76), 64 states have call predecessors, (76), 67 states have return successors, (80), 72 states have call predecessors, (80), 69 states have call successors, (80)
[2025-04-28 21:21:29,320 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 243 states to 243 states and 262 transitions.
[2025-04-28 21:21:29,321 INFO  L79                 Accepts]: Start accepts. Automaton has 243 states and 262 transitions. Word has length 649
[2025-04-28 21:21:29,322 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,322 INFO  L485      AbstractCegarLoop]: Abstraction has 243 states and 262 transitions.
[2025-04-28 21:21:29,323 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 9.222222222222221) internal successors, (83), 10 states have internal predecessors, (83), 3 states have call successors, (55), 1 states have call predecessors, (55), 9 states have return successors, (57), 9 states have call predecessors, (57), 3 states have call successors, (57)
[2025-04-28 21:21:29,323 INFO  L278                IsEmpty]: Start isEmpty. Operand 243 states and 262 transitions.
[2025-04-28 21:21:29,337 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 650
[2025-04-28 21:21:29,337 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,338 INFO  L218           NwaCegarLoop]: trace histogram [12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-04-28 21:21:29,338 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:29,338 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,339 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,339 INFO  L85        PathProgramCache]: Analyzing trace with hash -1614771557, now seen corresponding path program 1 times
[2025-04-28 21:21:29,339 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,339 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1773784035]
[2025-04-28 21:21:29,339 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,339 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,494 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 649 statements into 1 equivalence classes.
[2025-04-28 21:21:29,554 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 649 of 649 statements.
[2025-04-28 21:21:29,554 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,555 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,416 INFO  L134       CoverageAnalysis]: Checked inductivity of 1792 backedges. 9 proven. 0 refuted. 0 times theorem prover too weak. 1783 trivial. 0 not checked.
[2025-04-28 21:21:30,419 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,420 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1773784035]
[2025-04-28 21:21:30,420 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1773784035] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,420 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:30,420 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:30,420 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2063873271]
[2025-04-28 21:21:30,420 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,421 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:30,421 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,422 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:30,422 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:30,422 INFO  L87              Difference]: Start difference. First operand 243 states and 262 transitions. Second operand  has 10 states, 9 states have (on average 9.222222222222221) internal successors, (83), 10 states have internal predecessors, (83), 3 states have call successors, (55), 1 states have call predecessors, (55), 9 states have return successors, (57), 9 states have call predecessors, (57), 3 states have call successors, (57)
[2025-04-28 21:21:30,563 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,563 INFO  L93              Difference]: Finished difference Result 245 states and 264 transitions.
[2025-04-28 21:21:30,564 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:30,564 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 9 states have (on average 9.222222222222221) internal successors, (83), 10 states have internal predecessors, (83), 3 states have call successors, (55), 1 states have call predecessors, (55), 9 states have return successors, (57), 9 states have call predecessors, (57), 3 states have call successors, (57) Word has length 649
[2025-04-28 21:21:30,565 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,567 INFO  L225             Difference]: With dead ends: 245
[2025-04-28 21:21:30,567 INFO  L226             Difference]: Without dead ends: 245
[2025-04-28 21:21:30,567 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:30,568 INFO  L437           NwaCegarLoop]: 245 mSDtfsCounter, 1 mSDsluCounter, 1941 mSDsCounter, 0 mSdLazyCounter, 96 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 2186 SdHoareTripleChecker+Invalid, 96 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 96 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,569 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 2186 Invalid, 96 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 96 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:30,569 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 245 states.
[2025-04-28 21:21:30,578 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 245 to 245.
[2025-04-28 21:21:30,579 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 245 states, 107 states have (on average 1.0) internal successors, (107), 107 states have internal predecessors, (107), 69 states have call successors, (76), 64 states have call predecessors, (76), 68 states have return successors, (81), 73 states have call predecessors, (81), 69 states have call successors, (81)
[2025-04-28 21:21:30,580 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 245 states to 245 states and 264 transitions.
[2025-04-28 21:21:30,581 INFO  L79                 Accepts]: Start accepts. Automaton has 245 states and 264 transitions. Word has length 649
[2025-04-28 21:21:30,582 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,582 INFO  L485      AbstractCegarLoop]: Abstraction has 245 states and 264 transitions.
[2025-04-28 21:21:30,582 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 9 states have (on average 9.222222222222221) internal successors, (83), 10 states have internal predecessors, (83), 3 states have call successors, (55), 1 states have call predecessors, (55), 9 states have return successors, (57), 9 states have call predecessors, (57), 3 states have call successors, (57)
[2025-04-28 21:21:30,583 INFO  L278                IsEmpty]: Start isEmpty. Operand 245 states and 264 transitions.
[2025-04-28 21:21:30,596 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 649
[2025-04-28 21:21:30,596 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,597 INFO  L218           NwaCegarLoop]: trace histogram [12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-04-28 21:21:30,597 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:30,597 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,598 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,598 INFO  L85        PathProgramCache]: Analyzing trace with hash 1519989693, now seen corresponding path program 1 times
[2025-04-28 21:21:30,598 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,598 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2058253847]
[2025-04-28 21:21:30,598 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,598 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,733 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 648 statements into 1 equivalence classes.
[2025-04-28 21:21:30,795 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 648 of 648 statements.
[2025-04-28 21:21:30,796 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,796 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,751 INFO  L134       CoverageAnalysis]: Checked inductivity of 1792 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 1788 trivial. 0 not checked.
[2025-04-28 21:21:31,752 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,752 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2058253847]
[2025-04-28 21:21:31,752 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2058253847] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:31,752 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:31,752 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:31,752 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1723422927]
[2025-04-28 21:21:31,753 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,753 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:31,754 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,755 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:31,755 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:31,755 INFO  L87              Difference]: Start difference. First operand 245 states and 264 transitions. Second operand  has 10 states, 8 states have (on average 9.875) internal successors, (79), 10 states have internal predecessors, (79), 4 states have call successors, (54), 1 states have call predecessors, (54), 8 states have return successors, (55), 8 states have call predecessors, (55), 4 states have call successors, (55)
[2025-04-28 21:21:31,899 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,899 INFO  L93              Difference]: Finished difference Result 253 states and 274 transitions.
[2025-04-28 21:21:31,900 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:31,900 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 9.875) internal successors, (79), 10 states have internal predecessors, (79), 4 states have call successors, (54), 1 states have call predecessors, (54), 8 states have return successors, (55), 8 states have call predecessors, (55), 4 states have call successors, (55) Word has length 648
[2025-04-28 21:21:31,904 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,908 INFO  L225             Difference]: With dead ends: 253
[2025-04-28 21:21:31,908 INFO  L226             Difference]: Without dead ends: 253
[2025-04-28 21:21:31,908 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:31,909 INFO  L437           NwaCegarLoop]: 255 mSDtfsCounter, 2 mSDsluCounter, 1764 mSDsCounter, 0 mSdLazyCounter, 85 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 2019 SdHoareTripleChecker+Invalid, 85 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 85 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,911 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 2019 Invalid, 85 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 85 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:31,912 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 253 states.
[2025-04-28 21:21:31,924 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 253 to 253.
[2025-04-28 21:21:31,926 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 253 states, 111 states have (on average 1.0) internal successors, (111), 111 states have internal predecessors, (111), 69 states have call successors, (76), 64 states have call predecessors, (76), 72 states have return successors, (87), 77 states have call predecessors, (87), 69 states have call successors, (87)
[2025-04-28 21:21:31,928 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 253 states to 253 states and 274 transitions.
[2025-04-28 21:21:31,928 INFO  L79                 Accepts]: Start accepts. Automaton has 253 states and 274 transitions. Word has length 648
[2025-04-28 21:21:31,930 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,932 INFO  L485      AbstractCegarLoop]: Abstraction has 253 states and 274 transitions.
[2025-04-28 21:21:31,932 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 9.875) internal successors, (79), 10 states have internal predecessors, (79), 4 states have call successors, (54), 1 states have call predecessors, (54), 8 states have return successors, (55), 8 states have call predecessors, (55), 4 states have call successors, (55)
[2025-04-28 21:21:31,932 INFO  L278                IsEmpty]: Start isEmpty. Operand 253 states and 274 transitions.
[2025-04-28 21:21:31,954 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 649
[2025-04-28 21:21:31,955 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,955 INFO  L218           NwaCegarLoop]: trace histogram [12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-04-28 21:21:31,955 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:31,955 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,956 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,956 INFO  L85        PathProgramCache]: Analyzing trace with hash 2000216227, now seen corresponding path program 1 times
[2025-04-28 21:21:31,956 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,956 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1045796868]
[2025-04-28 21:21:31,957 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,957 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,090 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 648 statements into 1 equivalence classes.
[2025-04-28 21:21:32,146 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 648 of 648 statements.
[2025-04-28 21:21:32,146 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,147 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,115 INFO  L134       CoverageAnalysis]: Checked inductivity of 1792 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 1788 trivial. 0 not checked.
[2025-04-28 21:21:33,115 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,115 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1045796868]
[2025-04-28 21:21:33,116 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1045796868] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,116 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,116 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:33,116 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [61580969]
[2025-04-28 21:21:33,116 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,117 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:33,119 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,120 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:33,120 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:33,121 INFO  L87              Difference]: Start difference. First operand 253 states and 274 transitions. Second operand  has 10 states, 8 states have (on average 9.875) internal successors, (79), 10 states have internal predecessors, (79), 4 states have call successors, (54), 1 states have call predecessors, (54), 8 states have return successors, (55), 8 states have call predecessors, (55), 4 states have call successors, (55)
[2025-04-28 21:21:33,253 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,254 INFO  L93              Difference]: Finished difference Result 261 states and 284 transitions.
[2025-04-28 21:21:33,254 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:33,255 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 9.875) internal successors, (79), 10 states have internal predecessors, (79), 4 states have call successors, (54), 1 states have call predecessors, (54), 8 states have return successors, (55), 8 states have call predecessors, (55), 4 states have call successors, (55) Word has length 648
[2025-04-28 21:21:33,256 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,260 INFO  L225             Difference]: With dead ends: 261
[2025-04-28 21:21:33,263 INFO  L226             Difference]: Without dead ends: 261
[2025-04-28 21:21:33,263 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:33,264 INFO  L437           NwaCegarLoop]: 255 mSDtfsCounter, 2 mSDsluCounter, 1764 mSDsCounter, 0 mSdLazyCounter, 85 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 2019 SdHoareTripleChecker+Invalid, 85 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 85 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,264 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 2019 Invalid, 85 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 85 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:33,265 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 261 states.
[2025-04-28 21:21:33,282 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 261 to 253.
[2025-04-28 21:21:33,283 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 253 states, 111 states have (on average 1.0) internal successors, (111), 111 states have internal predecessors, (111), 69 states have call successors, (76), 64 states have call predecessors, (76), 72 states have return successors, (87), 77 states have call predecessors, (87), 69 states have call successors, (87)
[2025-04-28 21:21:33,285 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 253 states to 253 states and 274 transitions.
[2025-04-28 21:21:33,285 INFO  L79                 Accepts]: Start accepts. Automaton has 253 states and 274 transitions. Word has length 648
[2025-04-28 21:21:33,287 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,287 INFO  L485      AbstractCegarLoop]: Abstraction has 253 states and 274 transitions.
[2025-04-28 21:21:33,287 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 9.875) internal successors, (79), 10 states have internal predecessors, (79), 4 states have call successors, (54), 1 states have call predecessors, (54), 8 states have return successors, (55), 8 states have call predecessors, (55), 4 states have call successors, (55)
[2025-04-28 21:21:33,287 INFO  L278                IsEmpty]: Start isEmpty. Operand 253 states and 274 transitions.
[2025-04-28 21:21:33,298 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 663
[2025-04-28 21:21:33,299 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,300 INFO  L218           NwaCegarLoop]: trace histogram [12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-04-28 21:21:33,300 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:33,300 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,301 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,301 INFO  L85        PathProgramCache]: Analyzing trace with hash -967669851, now seen corresponding path program 1 times
[2025-04-28 21:21:33,301 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,301 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [604996772]
[2025-04-28 21:21:33,302 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,302 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,466 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 662 statements into 1 equivalence classes.
[2025-04-28 21:21:33,523 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 662 of 662 statements.
[2025-04-28 21:21:33,523 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,524 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,538 INFO  L134       CoverageAnalysis]: Checked inductivity of 1792 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 1788 trivial. 0 not checked.
[2025-04-28 21:21:35,539 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,539 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [604996772]
[2025-04-28 21:21:35,539 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [604996772] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:35,539 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1733619087]
[2025-04-28 21:21:35,539 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,540 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:35,543 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,548 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:21:35,549 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,188 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 662 statements into 1 equivalence classes.
[2025-04-28 21:21:37,117 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 662 of 662 statements.
[2025-04-28 21:21:37,117 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,117 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,147 INFO  L256         TraceCheckSpWp]: Trace formula consists of 4878 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,189 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,593 INFO  L134       CoverageAnalysis]: Checked inductivity of 1792 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 1788 trivial. 0 not checked.
[2025-04-28 21:21:37,593 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
