./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-180.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:14,466 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:14,534 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30d68e1c-385a-4e87-99c0-133805014718/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:14,541 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:14,545 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:14,568 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:14,568 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:14,569 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:14,569 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:14,569 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:14,569 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:14,569 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:14,570 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:14,570 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:14,570 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:14,570 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:14,570 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:14,570 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:14,570 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:14,571 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:14,571 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:14,571 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:14,571 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:14,571 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:14,571 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:14,572 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:14,572 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:14,914 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:14,926 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:14,928 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:14,931 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:14,931 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:14,932 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30d68e1c-385a-4e87-99c0-133805014718/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-180.smt2
[2025-04-28 21:21:14,937 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:14,941 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:15,640 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30d68e1c-385a-4e87-99c0-133805014718/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-180.smt2
[2025-04-28 21:21:15,646 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:15,648 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:15,650 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:15,650 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:15,651 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:15,657 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,704 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15 Unit
[2025-04-28 21:21:15,704 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:15,708 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,709 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:15,709 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:15,727 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,727 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,774 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,774 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,789 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,791 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,795 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,800 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,803 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,831 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,832 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:15,832 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:15,832 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:15,833 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,837 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:15,870 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:15,888 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:15,894 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:15,908 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:15,908 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:15,909 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:15,909 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:15,909 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:15,909 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:15,910 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h23 given in one single declaration
[2025-04-28 21:21:15,910 INFO  L130     BoogieDeclarations]: Found specification of procedure h23
[2025-04-28 21:21:15,910 INFO  L138     BoogieDeclarations]: Found implementation of procedure h23
[2025-04-28 21:21:15,910 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h19 given in one single declaration
[2025-04-28 21:21:15,910 INFO  L130     BoogieDeclarations]: Found specification of procedure h19
[2025-04-28 21:21:15,910 INFO  L138     BoogieDeclarations]: Found implementation of procedure h19
[2025-04-28 21:21:15,910 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h18 given in one single declaration
[2025-04-28 21:21:15,910 INFO  L130     BoogieDeclarations]: Found specification of procedure h18
[2025-04-28 21:21:15,910 INFO  L138     BoogieDeclarations]: Found implementation of procedure h18
[2025-04-28 21:21:15,910 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h16 given in one single declaration
[2025-04-28 21:21:15,911 INFO  L130     BoogieDeclarations]: Found specification of procedure h16
[2025-04-28 21:21:15,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure h16
[2025-04-28 21:21:15,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h15 given in one single declaration
[2025-04-28 21:21:15,912 INFO  L130     BoogieDeclarations]: Found specification of procedure h15
[2025-04-28 21:21:15,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure h15
[2025-04-28 21:21:15,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h13 given in one single declaration
[2025-04-28 21:21:15,912 INFO  L130     BoogieDeclarations]: Found specification of procedure h13
[2025-04-28 21:21:15,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure h13
[2025-04-28 21:21:15,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h12 given in one single declaration
[2025-04-28 21:21:15,912 INFO  L130     BoogieDeclarations]: Found specification of procedure h12
[2025-04-28 21:21:15,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure h12
[2025-04-28 21:21:15,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h10 given in one single declaration
[2025-04-28 21:21:15,913 INFO  L130     BoogieDeclarations]: Found specification of procedure h10
[2025-04-28 21:21:15,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure h10
[2025-04-28 21:21:15,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h9 given in one single declaration
[2025-04-28 21:21:15,913 INFO  L130     BoogieDeclarations]: Found specification of procedure h9
[2025-04-28 21:21:15,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure h9
[2025-04-28 21:21:15,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h7 given in one single declaration
[2025-04-28 21:21:15,914 INFO  L130     BoogieDeclarations]: Found specification of procedure h7
[2025-04-28 21:21:15,914 INFO  L138     BoogieDeclarations]: Found implementation of procedure h7
[2025-04-28 21:21:15,914 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h6 given in one single declaration
[2025-04-28 21:21:15,915 INFO  L130     BoogieDeclarations]: Found specification of procedure h6
[2025-04-28 21:21:15,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure h6
[2025-04-28 21:21:15,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h5 given in one single declaration
[2025-04-28 21:21:15,915 INFO  L130     BoogieDeclarations]: Found specification of procedure h5
[2025-04-28 21:21:15,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure h5
[2025-04-28 21:21:15,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h4 given in one single declaration
[2025-04-28 21:21:15,915 INFO  L130     BoogieDeclarations]: Found specification of procedure h4
[2025-04-28 21:21:15,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure h4
[2025-04-28 21:21:15,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h3 given in one single declaration
[2025-04-28 21:21:15,915 INFO  L130     BoogieDeclarations]: Found specification of procedure h3
[2025-04-28 21:21:15,916 INFO  L138     BoogieDeclarations]: Found implementation of procedure h3
[2025-04-28 21:21:15,916 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h2 given in one single declaration
[2025-04-28 21:21:15,916 INFO  L130     BoogieDeclarations]: Found specification of procedure h2
[2025-04-28 21:21:15,916 INFO  L138     BoogieDeclarations]: Found implementation of procedure h2
[2025-04-28 21:21:15,916 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h1 given in one single declaration
[2025-04-28 21:21:15,917 INFO  L130     BoogieDeclarations]: Found specification of procedure h1
[2025-04-28 21:21:15,917 INFO  L138     BoogieDeclarations]: Found implementation of procedure h1
[2025-04-28 21:21:15,917 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h44 given in one single declaration
[2025-04-28 21:21:15,917 INFO  L130     BoogieDeclarations]: Found specification of procedure h44
[2025-04-28 21:21:15,917 INFO  L138     BoogieDeclarations]: Found implementation of procedure h44
[2025-04-28 21:21:15,917 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h38 given in one single declaration
[2025-04-28 21:21:15,917 INFO  L130     BoogieDeclarations]: Found specification of procedure h38
[2025-04-28 21:21:15,917 INFO  L138     BoogieDeclarations]: Found implementation of procedure h38
[2025-04-28 21:21:15,917 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h37 given in one single declaration
[2025-04-28 21:21:15,918 INFO  L130     BoogieDeclarations]: Found specification of procedure h37
[2025-04-28 21:21:15,919 INFO  L138     BoogieDeclarations]: Found implementation of procedure h37
[2025-04-28 21:21:15,919 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h36 given in one single declaration
[2025-04-28 21:21:15,919 INFO  L130     BoogieDeclarations]: Found specification of procedure h36
[2025-04-28 21:21:15,919 INFO  L138     BoogieDeclarations]: Found implementation of procedure h36
[2025-04-28 21:21:15,919 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h35 given in one single declaration
[2025-04-28 21:21:15,919 INFO  L130     BoogieDeclarations]: Found specification of procedure h35
[2025-04-28 21:21:15,919 INFO  L138     BoogieDeclarations]: Found implementation of procedure h35
[2025-04-28 21:21:15,919 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h58 given in one single declaration
[2025-04-28 21:21:15,919 INFO  L130     BoogieDeclarations]: Found specification of procedure h58
[2025-04-28 21:21:15,920 INFO  L138     BoogieDeclarations]: Found implementation of procedure h58
[2025-04-28 21:21:15,920 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h57 given in one single declaration
[2025-04-28 21:21:15,920 INFO  L130     BoogieDeclarations]: Found specification of procedure h57
[2025-04-28 21:21:15,921 INFO  L138     BoogieDeclarations]: Found implementation of procedure h57
[2025-04-28 21:21:15,921 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h55 given in one single declaration
[2025-04-28 21:21:15,921 INFO  L130     BoogieDeclarations]: Found specification of procedure h55
[2025-04-28 21:21:15,921 INFO  L138     BoogieDeclarations]: Found implementation of procedure h55
[2025-04-28 21:21:15,921 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h54 given in one single declaration
[2025-04-28 21:21:15,921 INFO  L130     BoogieDeclarations]: Found specification of procedure h54
[2025-04-28 21:21:15,921 INFO  L138     BoogieDeclarations]: Found implementation of procedure h54
[2025-04-28 21:21:15,921 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h52 given in one single declaration
[2025-04-28 21:21:15,921 INFO  L130     BoogieDeclarations]: Found specification of procedure h52
[2025-04-28 21:21:15,921 INFO  L138     BoogieDeclarations]: Found implementation of procedure h52
[2025-04-28 21:21:15,922 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h51 given in one single declaration
[2025-04-28 21:21:15,922 INFO  L130     BoogieDeclarations]: Found specification of procedure h51
[2025-04-28 21:21:15,923 INFO  L138     BoogieDeclarations]: Found implementation of procedure h51
[2025-04-28 21:21:15,923 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h49 given in one single declaration
[2025-04-28 21:21:15,923 INFO  L130     BoogieDeclarations]: Found specification of procedure h49
[2025-04-28 21:21:15,923 INFO  L138     BoogieDeclarations]: Found implementation of procedure h49
[2025-04-28 21:21:15,923 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h48 given in one single declaration
[2025-04-28 21:21:15,923 INFO  L130     BoogieDeclarations]: Found specification of procedure h48
[2025-04-28 21:21:15,923 INFO  L138     BoogieDeclarations]: Found implementation of procedure h48
[2025-04-28 21:21:15,923 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h46 given in one single declaration
[2025-04-28 21:21:15,923 INFO  L130     BoogieDeclarations]: Found specification of procedure h46
[2025-04-28 21:21:15,923 INFO  L138     BoogieDeclarations]: Found implementation of procedure h46
[2025-04-28 21:21:15,923 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h45 given in one single declaration
[2025-04-28 21:21:15,923 INFO  L130     BoogieDeclarations]: Found specification of procedure h45
[2025-04-28 21:21:15,924 INFO  L138     BoogieDeclarations]: Found implementation of procedure h45
[2025-04-28 21:21:15,924 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h43 given in one single declaration
[2025-04-28 21:21:15,924 INFO  L130     BoogieDeclarations]: Found specification of procedure h43
[2025-04-28 21:21:15,924 INFO  L138     BoogieDeclarations]: Found implementation of procedure h43
[2025-04-28 21:21:15,924 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h42 given in one single declaration
[2025-04-28 21:21:15,924 INFO  L130     BoogieDeclarations]: Found specification of procedure h42
[2025-04-28 21:21:15,924 INFO  L138     BoogieDeclarations]: Found implementation of procedure h42
[2025-04-28 21:21:15,924 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h34 given in one single declaration
[2025-04-28 21:21:15,924 INFO  L130     BoogieDeclarations]: Found specification of procedure h34
[2025-04-28 21:21:15,924 INFO  L138     BoogieDeclarations]: Found implementation of procedure h34
[2025-04-28 21:21:15,924 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h33 given in one single declaration
[2025-04-28 21:21:15,924 INFO  L130     BoogieDeclarations]: Found specification of procedure h33
[2025-04-28 21:21:15,925 INFO  L138     BoogieDeclarations]: Found implementation of procedure h33
[2025-04-28 21:21:15,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h29 given in one single declaration
[2025-04-28 21:21:15,925 INFO  L130     BoogieDeclarations]: Found specification of procedure h29
[2025-04-28 21:21:15,925 INFO  L138     BoogieDeclarations]: Found implementation of procedure h29
[2025-04-28 21:21:15,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h28 given in one single declaration
[2025-04-28 21:21:15,925 INFO  L130     BoogieDeclarations]: Found specification of procedure h28
[2025-04-28 21:21:15,925 INFO  L138     BoogieDeclarations]: Found implementation of procedure h28
[2025-04-28 21:21:15,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h27 given in one single declaration
[2025-04-28 21:21:15,925 INFO  L130     BoogieDeclarations]: Found specification of procedure h27
[2025-04-28 21:21:15,925 INFO  L138     BoogieDeclarations]: Found implementation of procedure h27
[2025-04-28 21:21:15,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h26 given in one single declaration
[2025-04-28 21:21:15,925 INFO  L130     BoogieDeclarations]: Found specification of procedure h26
[2025-04-28 21:21:15,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure h26
[2025-04-28 21:21:15,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h77 given in one single declaration
[2025-04-28 21:21:15,926 INFO  L130     BoogieDeclarations]: Found specification of procedure h77
[2025-04-28 21:21:15,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure h77
[2025-04-28 21:21:15,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h76 given in one single declaration
[2025-04-28 21:21:15,926 INFO  L130     BoogieDeclarations]: Found specification of procedure h76
[2025-04-28 21:21:15,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure h76
[2025-04-28 21:21:15,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h74 given in one single declaration
[2025-04-28 21:21:15,926 INFO  L130     BoogieDeclarations]: Found specification of procedure h74
[2025-04-28 21:21:15,929 INFO  L138     BoogieDeclarations]: Found implementation of procedure h74
[2025-04-28 21:21:15,929 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h73 given in one single declaration
[2025-04-28 21:21:15,929 INFO  L130     BoogieDeclarations]: Found specification of procedure h73
[2025-04-28 21:21:15,930 INFO  L138     BoogieDeclarations]: Found implementation of procedure h73
[2025-04-28 21:21:15,930 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h71 given in one single declaration
[2025-04-28 21:21:15,930 INFO  L130     BoogieDeclarations]: Found specification of procedure h71
[2025-04-28 21:21:15,930 INFO  L138     BoogieDeclarations]: Found implementation of procedure h71
[2025-04-28 21:21:15,930 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h70 given in one single declaration
[2025-04-28 21:21:15,930 INFO  L130     BoogieDeclarations]: Found specification of procedure h70
[2025-04-28 21:21:15,930 INFO  L138     BoogieDeclarations]: Found implementation of procedure h70
[2025-04-28 21:21:15,930 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h68 given in one single declaration
[2025-04-28 21:21:15,930 INFO  L130     BoogieDeclarations]: Found specification of procedure h68
[2025-04-28 21:21:15,930 INFO  L138     BoogieDeclarations]: Found implementation of procedure h68
[2025-04-28 21:21:15,930 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h67 given in one single declaration
[2025-04-28 21:21:15,930 INFO  L130     BoogieDeclarations]: Found specification of procedure h67
[2025-04-28 21:21:15,930 INFO  L138     BoogieDeclarations]: Found implementation of procedure h67
[2025-04-28 21:21:15,930 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h65 given in one single declaration
[2025-04-28 21:21:15,931 INFO  L130     BoogieDeclarations]: Found specification of procedure h65
[2025-04-28 21:21:15,931 INFO  L138     BoogieDeclarations]: Found implementation of procedure h65
[2025-04-28 21:21:15,931 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h64 given in one single declaration
[2025-04-28 21:21:15,931 INFO  L130     BoogieDeclarations]: Found specification of procedure h64
[2025-04-28 21:21:15,931 INFO  L138     BoogieDeclarations]: Found implementation of procedure h64
[2025-04-28 21:21:15,931 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h62 given in one single declaration
[2025-04-28 21:21:15,931 INFO  L130     BoogieDeclarations]: Found specification of procedure h62
[2025-04-28 21:21:15,931 INFO  L138     BoogieDeclarations]: Found implementation of procedure h62
[2025-04-28 21:21:15,931 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h61 given in one single declaration
[2025-04-28 21:21:15,931 INFO  L130     BoogieDeclarations]: Found specification of procedure h61
[2025-04-28 21:21:15,931 INFO  L138     BoogieDeclarations]: Found implementation of procedure h61
[2025-04-28 21:21:15,931 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h60 given in one single declaration
[2025-04-28 21:21:15,931 INFO  L130     BoogieDeclarations]: Found specification of procedure h60
[2025-04-28 21:21:15,931 INFO  L138     BoogieDeclarations]: Found implementation of procedure h60
[2025-04-28 21:21:15,931 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h41 given in one single declaration
[2025-04-28 21:21:15,931 INFO  L130     BoogieDeclarations]: Found specification of procedure h41
[2025-04-28 21:21:15,931 INFO  L138     BoogieDeclarations]: Found implementation of procedure h41
[2025-04-28 21:21:15,931 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h40 given in one single declaration
[2025-04-28 21:21:15,932 INFO  L130     BoogieDeclarations]: Found specification of procedure h40
[2025-04-28 21:21:15,932 INFO  L138     BoogieDeclarations]: Found implementation of procedure h40
[2025-04-28 21:21:15,932 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h39 given in one single declaration
[2025-04-28 21:21:15,932 INFO  L130     BoogieDeclarations]: Found specification of procedure h39
[2025-04-28 21:21:15,932 INFO  L138     BoogieDeclarations]: Found implementation of procedure h39
[2025-04-28 21:21:15,932 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h25 given in one single declaration
[2025-04-28 21:21:15,932 INFO  L130     BoogieDeclarations]: Found specification of procedure h25
[2025-04-28 21:21:15,932 INFO  L138     BoogieDeclarations]: Found implementation of procedure h25
[2025-04-28 21:21:15,932 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h24 given in one single declaration
[2025-04-28 21:21:15,932 INFO  L130     BoogieDeclarations]: Found specification of procedure h24
[2025-04-28 21:21:15,932 INFO  L138     BoogieDeclarations]: Found implementation of procedure h24
[2025-04-28 21:21:15,932 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h22 given in one single declaration
[2025-04-28 21:21:15,932 INFO  L130     BoogieDeclarations]: Found specification of procedure h22
[2025-04-28 21:21:15,933 INFO  L138     BoogieDeclarations]: Found implementation of procedure h22
[2025-04-28 21:21:15,933 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h21 given in one single declaration
[2025-04-28 21:21:15,933 INFO  L130     BoogieDeclarations]: Found specification of procedure h21
[2025-04-28 21:21:15,933 INFO  L138     BoogieDeclarations]: Found implementation of procedure h21
[2025-04-28 21:21:15,933 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h53 given in one single declaration
[2025-04-28 21:21:15,933 INFO  L130     BoogieDeclarations]: Found specification of procedure h53
[2025-04-28 21:21:15,933 INFO  L138     BoogieDeclarations]: Found implementation of procedure h53
[2025-04-28 21:21:15,933 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h8 given in one single declaration
[2025-04-28 21:21:15,933 INFO  L130     BoogieDeclarations]: Found specification of procedure h8
[2025-04-28 21:21:15,933 INFO  L138     BoogieDeclarations]: Found implementation of procedure h8
[2025-04-28 21:21:15,934 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h17 given in one single declaration
[2025-04-28 21:21:15,934 INFO  L130     BoogieDeclarations]: Found specification of procedure h17
[2025-04-28 21:21:15,934 INFO  L138     BoogieDeclarations]: Found implementation of procedure h17
[2025-04-28 21:21:15,934 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h14 given in one single declaration
[2025-04-28 21:21:15,934 INFO  L130     BoogieDeclarations]: Found specification of procedure h14
[2025-04-28 21:21:15,934 INFO  L138     BoogieDeclarations]: Found implementation of procedure h14
[2025-04-28 21:21:15,934 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h59 given in one single declaration
[2025-04-28 21:21:15,934 INFO  L130     BoogieDeclarations]: Found specification of procedure h59
[2025-04-28 21:21:15,934 INFO  L138     BoogieDeclarations]: Found implementation of procedure h59
[2025-04-28 21:21:15,934 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h69 given in one single declaration
[2025-04-28 21:21:15,934 INFO  L130     BoogieDeclarations]: Found specification of procedure h69
[2025-04-28 21:21:15,935 INFO  L138     BoogieDeclarations]: Found implementation of procedure h69
[2025-04-28 21:21:15,935 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h75 given in one single declaration
[2025-04-28 21:21:15,935 INFO  L130     BoogieDeclarations]: Found specification of procedure h75
[2025-04-28 21:21:15,935 INFO  L138     BoogieDeclarations]: Found implementation of procedure h75
[2025-04-28 21:21:15,935 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h78 given in one single declaration
[2025-04-28 21:21:15,935 INFO  L130     BoogieDeclarations]: Found specification of procedure h78
[2025-04-28 21:21:15,935 INFO  L138     BoogieDeclarations]: Found implementation of procedure h78
[2025-04-28 21:21:15,935 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h63 given in one single declaration
[2025-04-28 21:21:15,935 INFO  L130     BoogieDeclarations]: Found specification of procedure h63
[2025-04-28 21:21:15,935 INFO  L138     BoogieDeclarations]: Found implementation of procedure h63
[2025-04-28 21:21:15,935 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h56 given in one single declaration
[2025-04-28 21:21:15,935 INFO  L130     BoogieDeclarations]: Found specification of procedure h56
[2025-04-28 21:21:15,935 INFO  L138     BoogieDeclarations]: Found implementation of procedure h56
[2025-04-28 21:21:15,936 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h66 given in one single declaration
[2025-04-28 21:21:15,936 INFO  L130     BoogieDeclarations]: Found specification of procedure h66
[2025-04-28 21:21:15,936 INFO  L138     BoogieDeclarations]: Found implementation of procedure h66
[2025-04-28 21:21:15,936 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h50 given in one single declaration
[2025-04-28 21:21:15,936 INFO  L130     BoogieDeclarations]: Found specification of procedure h50
[2025-04-28 21:21:15,936 INFO  L138     BoogieDeclarations]: Found implementation of procedure h50
[2025-04-28 21:21:15,936 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h11 given in one single declaration
[2025-04-28 21:21:15,936 INFO  L130     BoogieDeclarations]: Found specification of procedure h11
[2025-04-28 21:21:15,936 INFO  L138     BoogieDeclarations]: Found implementation of procedure h11
[2025-04-28 21:21:15,936 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h47 given in one single declaration
[2025-04-28 21:21:15,936 INFO  L130     BoogieDeclarations]: Found specification of procedure h47
[2025-04-28 21:21:15,937 INFO  L138     BoogieDeclarations]: Found implementation of procedure h47
[2025-04-28 21:21:15,937 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h72 given in one single declaration
[2025-04-28 21:21:15,937 INFO  L130     BoogieDeclarations]: Found specification of procedure h72
[2025-04-28 21:21:15,937 INFO  L138     BoogieDeclarations]: Found implementation of procedure h72
[2025-04-28 21:21:15,937 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h20 given in one single declaration
[2025-04-28 21:21:15,937 INFO  L130     BoogieDeclarations]: Found specification of procedure h20
[2025-04-28 21:21:15,937 INFO  L138     BoogieDeclarations]: Found implementation of procedure h20
[2025-04-28 21:21:15,937 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:15,937 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:15,937 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:16,465 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:16,468 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:17,123 INFO  L?                        ?]: Removed 1 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:17,123 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:17,146 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:17,149 INFO  L312             CfgBuilder]: Removed 50 assume(true) statements.
[2025-04-28 21:21:17,150 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17 BoogieIcfgContainer
[2025-04-28 21:21:17,150 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:17,154 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:17,154 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:17,157 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:17,158 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/3) ...
[2025-04-28 21:21:17,159 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@281966d0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,159 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (2/3) ...
[2025-04-28 21:21:17,159 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@281966d0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,159 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17" (3/3) ...
[2025-04-28 21:21:17,162 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:17,177 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:17,180 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 78 procedures, 281 locations, 414 edges, 78 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:17,243 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:17,263 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;@670959e7, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:17,264 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:17,269 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 281 states, 125 states have (on average 1.008) internal successors, (126), 126 states have internal predecessors, (126), 77 states have call successors, (96), 77 states have call predecessors, (96), 77 states have return successors, (96), 77 states have call predecessors, (96), 77 states have call successors, (96)
[2025-04-28 21:21:17,286 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:17,287 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,287 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,288 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,293 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,295 INFO  L85        PathProgramCache]: Analyzing trace with hash 613506161, now seen corresponding path program 1 times
[2025-04-28 21:21:17,302 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,303 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [994127569]
[2025-04-28 21:21:17,304 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,305 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,365 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:17,439 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:17,443 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,444 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,077 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:18,081 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,081 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [994127569]
[2025-04-28 21:21:18,082 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [994127569] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,082 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,090 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:18,096 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1433924877]
[2025-04-28 21:21:18,096 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,106 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:18,106 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,172 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:18,176 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:18,181 INFO  L87              Difference]: Start difference. First operand  has 281 states, 125 states have (on average 1.008) internal successors, (126), 126 states have internal predecessors, (126), 77 states have call successors, (96), 77 states have call predecessors, (96), 77 states have return successors, (96), 77 states have call predecessors, (96), 77 states have call successors, (96) Second operand  has 7 states, 5 states have (on average 2.6) internal successors, (13), 7 states have internal predecessors, (13), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:18,448 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,449 INFO  L93              Difference]: Finished difference Result 277 states and 313 transitions.
[2025-04-28 21:21:18,451 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:18,453 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.6) internal successors, (13), 7 states have internal predecessors, (13), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8) Word has length 29
[2025-04-28 21:21:18,454 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,469 INFO  L225             Difference]: With dead ends: 277
[2025-04-28 21:21:18,475 INFO  L226             Difference]: Without dead ends: 275
[2025-04-28 21:21:18,477 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:18,482 INFO  L437           NwaCegarLoop]: 310 mSDtfsCounter, 0 mSDsluCounter, 1535 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1845 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 22 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,483 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1845 Invalid, 22 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:18,501 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 275 states.
[2025-04-28 21:21:18,572 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 275 to 275.
[2025-04-28 21:21:18,574 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 275 states, 122 states have (on average 1.0) internal successors, (122), 122 states have internal predecessors, (122), 76 states have call successors, (94), 76 states have call predecessors, (94), 76 states have return successors, (94), 76 states have call predecessors, (94), 76 states have call successors, (94)
[2025-04-28 21:21:18,586 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 275 states to 275 states and 310 transitions.
[2025-04-28 21:21:18,591 INFO  L79                 Accepts]: Start accepts. Automaton has 275 states and 310 transitions. Word has length 29
[2025-04-28 21:21:18,594 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,594 INFO  L485      AbstractCegarLoop]: Abstraction has 275 states and 310 transitions.
[2025-04-28 21:21:18,595 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.6) internal successors, (13), 7 states have internal predecessors, (13), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:18,595 INFO  L278                IsEmpty]: Start isEmpty. Operand 275 states and 310 transitions.
[2025-04-28 21:21:18,597 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:18,601 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,601 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,602 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:18,602 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,603 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,604 INFO  L85        PathProgramCache]: Analyzing trace with hash 80805547, now seen corresponding path program 1 times
[2025-04-28 21:21:18,604 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,604 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [109314461]
[2025-04-28 21:21:18,604 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,605 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,631 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:18,644 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:18,645 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,645 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,944 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:18,944 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,944 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [109314461]
[2025-04-28 21:21:18,945 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [109314461] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,946 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,947 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:18,947 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [462370544]
[2025-04-28 21:21:18,947 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,948 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:18,948 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,949 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:18,950 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:18,951 INFO  L87              Difference]: Start difference. First operand 275 states and 310 transitions. Second operand  has 7 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 7 states have internal predecessors, (16), 3 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (10), 6 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:19,088 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,088 INFO  L93              Difference]: Finished difference Result 273 states and 307 transitions.
[2025-04-28 21:21:19,089 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:19,089 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 7 states have internal predecessors, (16), 3 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (10), 6 states have call predecessors, (10), 3 states have call successors, (10) Word has length 36
[2025-04-28 21:21:19,090 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,096 INFO  L225             Difference]: With dead ends: 273
[2025-04-28 21:21:19,096 INFO  L226             Difference]: Without dead ends: 271
[2025-04-28 21:21:19,097 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:19,098 INFO  L437           NwaCegarLoop]: 303 mSDtfsCounter, 0 mSDsluCounter, 1501 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1804 SdHoareTripleChecker+Invalid, 28 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,098 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1804 Invalid, 28 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:19,099 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 271 states.
[2025-04-28 21:21:19,126 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 271 to 271.
[2025-04-28 21:21:19,126 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 271 states, 120 states have (on average 1.0) internal successors, (120), 120 states have internal predecessors, (120), 75 states have call successors, (92), 75 states have call predecessors, (92), 75 states have return successors, (92), 75 states have call predecessors, (92), 75 states have call successors, (92)
[2025-04-28 21:21:19,132 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 271 states to 271 states and 304 transitions.
[2025-04-28 21:21:19,133 INFO  L79                 Accepts]: Start accepts. Automaton has 271 states and 304 transitions. Word has length 36
[2025-04-28 21:21:19,133 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,133 INFO  L485      AbstractCegarLoop]: Abstraction has 271 states and 304 transitions.
[2025-04-28 21:21:19,133 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 7 states have internal predecessors, (16), 3 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (10), 6 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:19,133 INFO  L278                IsEmpty]: Start isEmpty. Operand 271 states and 304 transitions.
[2025-04-28 21:21:19,138 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 44
[2025-04-28 21:21:19,139 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,139 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,139 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:19,139 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,139 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,139 INFO  L85        PathProgramCache]: Analyzing trace with hash -1464178672, now seen corresponding path program 1 times
[2025-04-28 21:21:19,140 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,140 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1286230366]
[2025-04-28 21:21:19,140 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,140 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,173 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 43 statements into 1 equivalence classes.
[2025-04-28 21:21:19,190 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 43 of 43 statements.
[2025-04-28 21:21:19,190 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,190 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,741 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:19,741 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,741 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1286230366]
[2025-04-28 21:21:19,741 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1286230366] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:19,741 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:19,741 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:19,741 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1306703163]
[2025-04-28 21:21:19,742 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,742 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:19,742 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,742 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:19,743 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:19,743 INFO  L87              Difference]: Start difference. First operand 271 states and 304 transitions. Second operand  has 10 states, 8 states have (on average 2.375) internal successors, (19), 10 states have internal predecessors, (19), 4 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 8 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:19,920 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,920 INFO  L93              Difference]: Finished difference Result 269 states and 301 transitions.
[2025-04-28 21:21:19,921 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:19,921 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 2.375) internal successors, (19), 10 states have internal predecessors, (19), 4 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 8 states have call predecessors, (12), 4 states have call successors, (12) Word has length 43
[2025-04-28 21:21:19,921 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,923 INFO  L225             Difference]: With dead ends: 269
[2025-04-28 21:21:19,924 INFO  L226             Difference]: Without dead ends: 267
[2025-04-28 21:21:19,924 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:19,925 INFO  L437           NwaCegarLoop]: 295 mSDtfsCounter, 0 mSDsluCounter, 2046 mSDsCounter, 0 mSdLazyCounter, 53 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 2341 SdHoareTripleChecker+Invalid, 53 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 53 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,925 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 2341 Invalid, 53 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 53 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:19,926 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 267 states.
[2025-04-28 21:21:19,940 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 267 to 267.
[2025-04-28 21:21:19,940 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 267 states, 118 states have (on average 1.0) internal successors, (118), 118 states have internal predecessors, (118), 74 states have call successors, (90), 74 states have call predecessors, (90), 74 states have return successors, (90), 74 states have call predecessors, (90), 74 states have call successors, (90)
[2025-04-28 21:21:19,942 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 267 states to 267 states and 298 transitions.
[2025-04-28 21:21:19,942 INFO  L79                 Accepts]: Start accepts. Automaton has 267 states and 298 transitions. Word has length 43
[2025-04-28 21:21:19,943 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,943 INFO  L485      AbstractCegarLoop]: Abstraction has 267 states and 298 transitions.
[2025-04-28 21:21:19,943 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 2.375) internal successors, (19), 10 states have internal predecessors, (19), 4 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 8 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:19,943 INFO  L278                IsEmpty]: Start isEmpty. Operand 267 states and 298 transitions.
[2025-04-28 21:21:19,945 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 51
[2025-04-28 21:21:19,945 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,945 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,945 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:19,945 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,946 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,946 INFO  L85        PathProgramCache]: Analyzing trace with hash 1874520376, now seen corresponding path program 1 times
[2025-04-28 21:21:19,946 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,946 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2016410493]
[2025-04-28 21:21:19,946 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,946 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,981 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 50 statements into 1 equivalence classes.
[2025-04-28 21:21:19,997 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 50 of 50 statements.
[2025-04-28 21:21:19,998 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,998 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,498 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:20,498 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,498 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2016410493]
[2025-04-28 21:21:20,498 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2016410493] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,498 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,498 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [12] imperfect sequences [] total 12
[2025-04-28 21:21:20,499 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [330361301]
[2025-04-28 21:21:20,499 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,499 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:20,500 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,500 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:20,501 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=22, Invalid=110, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:20,501 INFO  L87              Difference]: Start difference. First operand 267 states and 298 transitions. Second operand  has 12 states, 10 states have (on average 2.2) internal successors, (22), 12 states have internal predecessors, (22), 4 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (14), 10 states have call predecessors, (14), 4 states have call successors, (14)
[2025-04-28 21:21:20,694 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,698 INFO  L93              Difference]: Finished difference Result 265 states and 295 transitions.
[2025-04-28 21:21:20,699 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:20,699 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 10 states have (on average 2.2) internal successors, (22), 12 states have internal predecessors, (22), 4 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (14), 10 states have call predecessors, (14), 4 states have call successors, (14) Word has length 50
[2025-04-28 21:21:20,700 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,703 INFO  L225             Difference]: With dead ends: 265
[2025-04-28 21:21:20,706 INFO  L226             Difference]: Without dead ends: 263
[2025-04-28 21:21:20,706 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=22, Invalid=110, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:20,707 INFO  L437           NwaCegarLoop]: 287 mSDtfsCounter, 0 mSDsluCounter, 2560 mSDsCounter, 0 mSdLazyCounter, 85 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 2847 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:20,707 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 2847 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:20,708 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 263 states.
[2025-04-28 21:21:20,733 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 263 to 263.
[2025-04-28 21:21:20,737 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 263 states, 116 states have (on average 1.0) internal successors, (116), 116 states have internal predecessors, (116), 73 states have call successors, (88), 73 states have call predecessors, (88), 73 states have return successors, (88), 73 states have call predecessors, (88), 73 states have call successors, (88)
[2025-04-28 21:21:20,739 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 263 states to 263 states and 292 transitions.
[2025-04-28 21:21:20,739 INFO  L79                 Accepts]: Start accepts. Automaton has 263 states and 292 transitions. Word has length 50
[2025-04-28 21:21:20,739 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,739 INFO  L485      AbstractCegarLoop]: Abstraction has 263 states and 292 transitions.
[2025-04-28 21:21:20,740 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 10 states have (on average 2.2) internal successors, (22), 12 states have internal predecessors, (22), 4 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (14), 10 states have call predecessors, (14), 4 states have call successors, (14)
[2025-04-28 21:21:20,740 INFO  L278                IsEmpty]: Start isEmpty. Operand 263 states and 292 transitions.
[2025-04-28 21:21:20,741 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 58
[2025-04-28 21:21:20,742 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,742 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,742 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:20,742 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,743 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,743 INFO  L85        PathProgramCache]: Analyzing trace with hash -732745075, now seen corresponding path program 1 times
[2025-04-28 21:21:20,743 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,743 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [191589587]
[2025-04-28 21:21:20,743 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,743 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,771 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 57 statements into 1 equivalence classes.
[2025-04-28 21:21:20,789 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 57 of 57 statements.
[2025-04-28 21:21:20,790 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,790 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,090 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:21,090 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,091 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [191589587]
[2025-04-28 21:21:21,092 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [191589587] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,092 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,092 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:21,092 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2043938305]
[2025-04-28 21:21:21,092 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,093 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:21,093 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,093 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:21,094 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,094 INFO  L87              Difference]: Start difference. First operand 263 states and 292 transitions. Second operand  has 7 states, 6 states have (on average 4.166666666666667) internal successors, (25), 7 states have internal predecessors, (25), 3 states have call successors, (16), 1 states have call predecessors, (16), 6 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:21,180 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,180 INFO  L93              Difference]: Finished difference Result 261 states and 289 transitions.
[2025-04-28 21:21:21,181 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:21,182 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 4.166666666666667) internal successors, (25), 7 states have internal predecessors, (25), 3 states have call successors, (16), 1 states have call predecessors, (16), 6 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16) Word has length 57
[2025-04-28 21:21:21,182 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,184 INFO  L225             Difference]: With dead ends: 261
[2025-04-28 21:21:21,184 INFO  L226             Difference]: Without dead ends: 259
[2025-04-28 21:21:21,184 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,185 INFO  L437           NwaCegarLoop]: 285 mSDtfsCounter, 0 mSDsluCounter, 1411 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1696 SdHoareTripleChecker+Invalid, 28 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,185 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1696 Invalid, 28 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:21,190 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 259 states.
[2025-04-28 21:21:21,207 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 259 to 259.
[2025-04-28 21:21:21,208 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 259 states, 114 states have (on average 1.0) internal successors, (114), 114 states have internal predecessors, (114), 72 states have call successors, (86), 72 states have call predecessors, (86), 72 states have return successors, (86), 72 states have call predecessors, (86), 72 states have call successors, (86)
[2025-04-28 21:21:21,214 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 259 states to 259 states and 286 transitions.
[2025-04-28 21:21:21,214 INFO  L79                 Accepts]: Start accepts. Automaton has 259 states and 286 transitions. Word has length 57
[2025-04-28 21:21:21,214 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,214 INFO  L485      AbstractCegarLoop]: Abstraction has 259 states and 286 transitions.
[2025-04-28 21:21:21,214 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 4.166666666666667) internal successors, (25), 7 states have internal predecessors, (25), 3 states have call successors, (16), 1 states have call predecessors, (16), 6 states have return successors, (16), 6 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:21:21,215 INFO  L278                IsEmpty]: Start isEmpty. Operand 259 states and 286 transitions.
[2025-04-28 21:21:21,220 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 65
[2025-04-28 21:21:21,220 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,220 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,220 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:21,220 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,221 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,221 INFO  L85        PathProgramCache]: Analyzing trace with hash 405517732, now seen corresponding path program 1 times
[2025-04-28 21:21:21,221 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,221 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1175479689]
[2025-04-28 21:21:21,221 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,221 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,257 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 64 statements into 1 equivalence classes.
[2025-04-28 21:21:21,277 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 64 of 64 statements.
[2025-04-28 21:21:21,277 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,277 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,512 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:21,512 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,513 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1175479689]
[2025-04-28 21:21:21,513 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1175479689] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,513 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,513 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:21,513 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1769801386]
[2025-04-28 21:21:21,513 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,514 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:21,514 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,514 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:21,515 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,515 INFO  L87              Difference]: Start difference. First operand 259 states and 286 transitions. Second operand  has 7 states, 6 states have (on average 4.666666666666667) internal successors, (28), 7 states have internal predecessors, (28), 3 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-04-28 21:21:21,589 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,589 INFO  L93              Difference]: Finished difference Result 257 states and 283 transitions.
[2025-04-28 21:21:21,590 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:21,591 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 4.666666666666667) internal successors, (28), 7 states have internal predecessors, (28), 3 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18) Word has length 64
[2025-04-28 21:21:21,591 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,593 INFO  L225             Difference]: With dead ends: 257
[2025-04-28 21:21:21,593 INFO  L226             Difference]: Without dead ends: 255
[2025-04-28 21:21:21,593 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,594 INFO  L437           NwaCegarLoop]: 279 mSDtfsCounter, 0 mSDsluCounter, 1381 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 1660 SdHoareTripleChecker+Invalid, 28 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,594 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 1660 Invalid, 28 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:21,595 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 255 states.
[2025-04-28 21:21:21,604 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 255 to 255.
[2025-04-28 21:21:21,605 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 255 states, 112 states have (on average 1.0) internal successors, (112), 112 states have internal predecessors, (112), 71 states have call successors, (84), 71 states have call predecessors, (84), 71 states have return successors, (84), 71 states have call predecessors, (84), 71 states have call successors, (84)
[2025-04-28 21:21:21,607 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 255 states to 255 states and 280 transitions.
[2025-04-28 21:21:21,607 INFO  L79                 Accepts]: Start accepts. Automaton has 255 states and 280 transitions. Word has length 64
[2025-04-28 21:21:21,608 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,608 INFO  L485      AbstractCegarLoop]: Abstraction has 255 states and 280 transitions.
[2025-04-28 21:21:21,608 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 4.666666666666667) internal successors, (28), 7 states have internal predecessors, (28), 3 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 3 states have call successors, (18)
[2025-04-28 21:21:21,608 INFO  L278                IsEmpty]: Start isEmpty. Operand 255 states and 280 transitions.
[2025-04-28 21:21:21,610 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-04-28 21:21:21,610 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,610 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,610 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:21,611 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,611 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,611 INFO  L85        PathProgramCache]: Analyzing trace with hash 462773929, now seen corresponding path program 1 times
[2025-04-28 21:21:21,612 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,612 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1284909809]
[2025-04-28 21:21:21,612 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,612 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,655 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-04-28 21:21:21,676 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-04-28 21:21:21,676 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,677 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,201 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:23,202 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,203 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1284909809]
[2025-04-28 21:21:23,203 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1284909809] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:23,203 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:23,203 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [21] imperfect sequences [] total 21
[2025-04-28 21:21:23,203 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1962202340]
[2025-04-28 21:21:23,203 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:23,203 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:23,204 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:23,204 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:23,205 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=41, Invalid=379, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:23,205 INFO  L87              Difference]: Start difference. First operand 255 states and 280 transitions. Second operand  has 21 states, 18 states have (on average 2.611111111111111) internal successors, (47), 21 states have internal predecessors, (47), 5 states have call successors, (32), 1 states have call predecessors, (32), 18 states have return successors, (32), 18 states have call predecessors, (32), 5 states have call successors, (32)
[2025-04-28 21:21:23,705 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,705 INFO  L93              Difference]: Finished difference Result 275 states and 301 transitions.
[2025-04-28 21:21:23,706 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-04-28 21:21:23,706 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 18 states have (on average 2.611111111111111) internal successors, (47), 21 states have internal predecessors, (47), 5 states have call successors, (32), 1 states have call predecessors, (32), 18 states have return successors, (32), 18 states have call predecessors, (32), 5 states have call successors, (32) Word has length 111
[2025-04-28 21:21:23,707 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,710 INFO  L225             Difference]: With dead ends: 275
[2025-04-28 21:21:23,712 INFO  L226             Difference]: Without dead ends: 275
[2025-04-28 21:21:23,712 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 21 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=41, Invalid=379, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:23,713 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 2 mSDsluCounter, 4685 mSDsCounter, 0 mSdLazyCounter, 353 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 4947 SdHoareTripleChecker+Invalid, 353 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 353 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,716 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 4947 Invalid, 353 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 353 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:23,718 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 275 states.
[2025-04-28 21:21:23,737 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 275 to 275.
[2025-04-28 21:21:23,740 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 275 states, 122 states have (on average 1.0) internal successors, (122), 122 states have internal predecessors, (122), 71 states have call successors, (84), 71 states have call predecessors, (84), 81 states have return successors, (95), 81 states have call predecessors, (95), 71 states have call successors, (95)
[2025-04-28 21:21:23,743 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 275 states to 275 states and 301 transitions.
[2025-04-28 21:21:23,743 INFO  L79                 Accepts]: Start accepts. Automaton has 275 states and 301 transitions. Word has length 111
[2025-04-28 21:21:23,743 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,744 INFO  L485      AbstractCegarLoop]: Abstraction has 275 states and 301 transitions.
[2025-04-28 21:21:23,744 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 18 states have (on average 2.611111111111111) internal successors, (47), 21 states have internal predecessors, (47), 5 states have call successors, (32), 1 states have call predecessors, (32), 18 states have return successors, (32), 18 states have call predecessors, (32), 5 states have call successors, (32)
[2025-04-28 21:21:23,744 INFO  L278                IsEmpty]: Start isEmpty. Operand 275 states and 301 transitions.
[2025-04-28 21:21:23,746 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 118
[2025-04-28 21:21:23,748 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,748 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:23,748 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:23,748 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,749 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,749 INFO  L85        PathProgramCache]: Analyzing trace with hash -1311712987, now seen corresponding path program 1 times
[2025-04-28 21:21:23,749 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,749 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [424470679]
[2025-04-28 21:21:23,749 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,749 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,794 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 117 statements into 1 equivalence classes.
[2025-04-28 21:21:23,821 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 117 of 117 statements.
[2025-04-28 21:21:23,822 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,822 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,590 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:25,590 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,590 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [424470679]
[2025-04-28 21:21:25,590 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [424470679] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:25,590 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:25,590 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [32] imperfect sequences [] total 32
[2025-04-28 21:21:25,590 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [417727876]
[2025-04-28 21:21:25,590 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,591 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 32 states
[2025-04-28 21:21:25,591 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,592 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 32 interpolants.
[2025-04-28 21:21:25,592 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=62, Invalid=930, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:25,593 INFO  L87              Difference]: Start difference. First operand 275 states and 301 transitions. Second operand  has 32 states, 30 states have (on average 1.6333333333333333) internal successors, (49), 32 states have internal predecessors, (49), 4 states have call successors, (34), 1 states have call predecessors, (34), 30 states have return successors, (34), 30 states have call predecessors, (34), 4 states have call successors, (34)
[2025-04-28 21:21:26,587 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,588 INFO  L93              Difference]: Finished difference Result 283 states and 309 transitions.
[2025-04-28 21:21:26,588 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 32 states. 
[2025-04-28 21:21:26,589 INFO  L79                 Accepts]: Start accepts. Automaton has  has 32 states, 30 states have (on average 1.6333333333333333) internal successors, (49), 32 states have internal predecessors, (49), 4 states have call successors, (34), 1 states have call predecessors, (34), 30 states have return successors, (34), 30 states have call predecessors, (34), 4 states have call successors, (34) Word has length 117
[2025-04-28 21:21:26,589 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,591 INFO  L225             Difference]: With dead ends: 283
[2025-04-28 21:21:26,591 INFO  L226             Difference]: Without dead ends: 283
[2025-04-28 21:21:26,592 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=62, Invalid=930, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:26,592 INFO  L437           NwaCegarLoop]: 250 mSDtfsCounter, 2 mSDsluCounter, 7204 mSDsCounter, 0 mSdLazyCounter, 909 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 7454 SdHoareTripleChecker+Invalid, 909 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 909 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,593 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 7454 Invalid, 909 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 909 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:26,596 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 283 states.
[2025-04-28 21:21:26,609 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 283 to 283.
[2025-04-28 21:21:26,610 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 283 states, 126 states have (on average 1.0) internal successors, (126), 126 states have internal predecessors, (126), 71 states have call successors, (84), 71 states have call predecessors, (84), 85 states have return successors, (99), 85 states have call predecessors, (99), 71 states have call successors, (99)
[2025-04-28 21:21:26,612 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 283 states to 283 states and 309 transitions.
[2025-04-28 21:21:26,612 INFO  L79                 Accepts]: Start accepts. Automaton has 283 states and 309 transitions. Word has length 117
[2025-04-28 21:21:26,613 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,613 INFO  L485      AbstractCegarLoop]: Abstraction has 283 states and 309 transitions.
[2025-04-28 21:21:26,613 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 32 states, 30 states have (on average 1.6333333333333333) internal successors, (49), 32 states have internal predecessors, (49), 4 states have call successors, (34), 1 states have call predecessors, (34), 30 states have return successors, (34), 30 states have call predecessors, (34), 4 states have call successors, (34)
[2025-04-28 21:21:26,613 INFO  L278                IsEmpty]: Start isEmpty. Operand 283 states and 309 transitions.
[2025-04-28 21:21:26,615 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 119
[2025-04-28 21:21:26,615 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,615 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,615 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:26,616 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,616 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,616 INFO  L85        PathProgramCache]: Analyzing trace with hash -410047672, now seen corresponding path program 1 times
[2025-04-28 21:21:26,616 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,616 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [415591478]
[2025-04-28 21:21:26,616 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,616 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,656 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 118 statements into 1 equivalence classes.
[2025-04-28 21:21:26,675 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 118 of 118 statements.
[2025-04-28 21:21:26,675 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,675 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,608 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:27,609 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,609 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [415591478]
[2025-04-28 21:21:27,609 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [415591478] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,609 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,609 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [20] imperfect sequences [] total 20
[2025-04-28 21:21:27,609 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [718045863]
[2025-04-28 21:21:27,609 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,610 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:27,610 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,610 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:27,611 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=343, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:27,612 INFO  L87              Difference]: Start difference. First operand 283 states and 309 transitions. Second operand  has 20 states, 18 states have (on average 2.7777777777777777) internal successors, (50), 20 states have internal predecessors, (50), 4 states have call successors, (34), 1 states have call predecessors, (34), 18 states have return successors, (34), 18 states have call predecessors, (34), 4 states have call successors, (34)
[2025-04-28 21:21:28,045 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,046 INFO  L93              Difference]: Finished difference Result 287 states and 313 transitions.
[2025-04-28 21:21:28,046 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-04-28 21:21:28,046 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 18 states have (on average 2.7777777777777777) internal successors, (50), 20 states have internal predecessors, (50), 4 states have call successors, (34), 1 states have call predecessors, (34), 18 states have return successors, (34), 18 states have call predecessors, (34), 4 states have call successors, (34) Word has length 118
[2025-04-28 21:21:28,047 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,048 INFO  L225             Difference]: With dead ends: 287
[2025-04-28 21:21:28,048 INFO  L226             Difference]: Without dead ends: 287
[2025-04-28 21:21:28,049 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 21 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=41, Invalid=379, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:28,049 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 3 mSDsluCounter, 4690 mSDsCounter, 0 mSdLazyCounter, 352 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 4952 SdHoareTripleChecker+Invalid, 352 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 352 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,050 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 4952 Invalid, 352 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 352 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:28,052 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 287 states.
[2025-04-28 21:21:28,068 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 287 to 287.
[2025-04-28 21:21:28,069 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 287 states, 128 states have (on average 1.0) internal successors, (128), 128 states have internal predecessors, (128), 71 states have call successors, (84), 71 states have call predecessors, (84), 87 states have return successors, (101), 87 states have call predecessors, (101), 71 states have call successors, (101)
[2025-04-28 21:21:28,074 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 287 states to 287 states and 313 transitions.
[2025-04-28 21:21:28,074 INFO  L79                 Accepts]: Start accepts. Automaton has 287 states and 313 transitions. Word has length 118
[2025-04-28 21:21:28,075 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,075 INFO  L485      AbstractCegarLoop]: Abstraction has 287 states and 313 transitions.
[2025-04-28 21:21:28,075 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 18 states have (on average 2.7777777777777777) internal successors, (50), 20 states have internal predecessors, (50), 4 states have call successors, (34), 1 states have call predecessors, (34), 18 states have return successors, (34), 18 states have call predecessors, (34), 4 states have call successors, (34)
[2025-04-28 21:21:28,075 INFO  L278                IsEmpty]: Start isEmpty. Operand 287 states and 313 transitions.
[2025-04-28 21:21:28,076 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 126
[2025-04-28 21:21:28,077 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,077 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,077 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:28,079 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,080 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,080 INFO  L85        PathProgramCache]: Analyzing trace with hash 1142758463, now seen corresponding path program 1 times
[2025-04-28 21:21:28,080 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,080 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1221064666]
[2025-04-28 21:21:28,080 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,080 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,133 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 125 statements into 1 equivalence classes.
[2025-04-28 21:21:28,162 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 125 of 125 statements.
[2025-04-28 21:21:28,162 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,163 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,074 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:30,075 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,075 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1221064666]
[2025-04-28 21:21:30,075 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1221064666] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,075 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:30,075 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [34] imperfect sequences [] total 34
[2025-04-28 21:21:30,075 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [716395423]
[2025-04-28 21:21:30,075 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,076 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 34 states
[2025-04-28 21:21:30,076 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,077 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 34 interpolants.
[2025-04-28 21:21:30,078 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=65, Invalid=1057, Unknown=0, NotChecked=0, Total=1122
[2025-04-28 21:21:30,078 INFO  L87              Difference]: Start difference. First operand 287 states and 313 transitions. Second operand  has 34 states, 32 states have (on average 1.65625) internal successors, (53), 34 states have internal predecessors, (53), 4 states have call successors, (36), 1 states have call predecessors, (36), 32 states have return successors, (36), 32 states have call predecessors, (36), 4 states have call successors, (36)
[2025-04-28 21:21:31,195 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,195 INFO  L93              Difference]: Finished difference Result 291 states and 317 transitions.
[2025-04-28 21:21:31,195 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 34 states. 
[2025-04-28 21:21:31,196 INFO  L79                 Accepts]: Start accepts. Automaton has  has 34 states, 32 states have (on average 1.65625) internal successors, (53), 34 states have internal predecessors, (53), 4 states have call successors, (36), 1 states have call predecessors, (36), 32 states have return successors, (36), 32 states have call predecessors, (36), 4 states have call successors, (36) Word has length 125
[2025-04-28 21:21:31,196 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,198 INFO  L225             Difference]: With dead ends: 291
[2025-04-28 21:21:31,198 INFO  L226             Difference]: Without dead ends: 291
[2025-04-28 21:21:31,198 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 36 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=69, Invalid=1121, Unknown=0, NotChecked=0, Total=1190
[2025-04-28 21:21:31,199 INFO  L437           NwaCegarLoop]: 248 mSDtfsCounter, 3 mSDsluCounter, 7885 mSDsCounter, 0 mSdLazyCounter, 1067 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 8133 SdHoareTripleChecker+Invalid, 1067 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 1067 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,199 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 8133 Invalid, 1067 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 1067 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:21:31,200 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 291 states.
[2025-04-28 21:21:31,216 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 291 to 291.
[2025-04-28 21:21:31,217 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 291 states, 130 states have (on average 1.0) internal successors, (130), 130 states have internal predecessors, (130), 71 states have call successors, (84), 71 states have call predecessors, (84), 89 states have return successors, (103), 89 states have call predecessors, (103), 71 states have call successors, (103)
[2025-04-28 21:21:31,219 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 291 states to 291 states and 317 transitions.
[2025-04-28 21:21:31,219 INFO  L79                 Accepts]: Start accepts. Automaton has 291 states and 317 transitions. Word has length 125
[2025-04-28 21:21:31,220 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,220 INFO  L485      AbstractCegarLoop]: Abstraction has 291 states and 317 transitions.
[2025-04-28 21:21:31,220 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 34 states, 32 states have (on average 1.65625) internal successors, (53), 34 states have internal predecessors, (53), 4 states have call successors, (36), 1 states have call predecessors, (36), 32 states have return successors, (36), 32 states have call predecessors, (36), 4 states have call successors, (36)
[2025-04-28 21:21:31,221 INFO  L278                IsEmpty]: Start isEmpty. Operand 291 states and 317 transitions.
[2025-04-28 21:21:31,223 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 125
[2025-04-28 21:21:31,226 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,226 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,226 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:31,226 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,227 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,227 INFO  L85        PathProgramCache]: Analyzing trace with hash -1021660548, now seen corresponding path program 1 times
[2025-04-28 21:21:31,227 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,227 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [544104062]
[2025-04-28 21:21:31,227 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,228 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,296 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 124 statements into 1 equivalence classes.
[2025-04-28 21:21:31,318 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 124 of 124 statements.
[2025-04-28 21:21:31,318 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,318 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,429 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:33,430 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,430 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [544104062]
[2025-04-28 21:21:33,430 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [544104062] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,430 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,430 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [30] imperfect sequences [] total 30
[2025-04-28 21:21:33,430 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [320392872]
[2025-04-28 21:21:33,430 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,431 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-04-28 21:21:33,431 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,432 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-04-28 21:21:33,433 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=812, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:33,433 INFO  L87              Difference]: Start difference. First operand 291 states and 317 transitions. Second operand  has 30 states, 28 states have (on average 1.8571428571428572) internal successors, (52), 30 states have internal predecessors, (52), 4 states have call successors, (36), 1 states have call predecessors, (36), 28 states have return successors, (36), 28 states have call predecessors, (36), 4 states have call successors, (36)
[2025-04-28 21:21:34,259 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,260 INFO  L93              Difference]: Finished difference Result 295 states and 321 transitions.
[2025-04-28 21:21:34,260 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 30 states. 
[2025-04-28 21:21:34,261 INFO  L79                 Accepts]: Start accepts. Automaton has  has 30 states, 28 states have (on average 1.8571428571428572) internal successors, (52), 30 states have internal predecessors, (52), 4 states have call successors, (36), 1 states have call predecessors, (36), 28 states have return successors, (36), 28 states have call predecessors, (36), 4 states have call successors, (36) Word has length 124
[2025-04-28 21:21:34,261 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,264 INFO  L225             Difference]: With dead ends: 295
[2025-04-28 21:21:34,264 INFO  L226             Difference]: Without dead ends: 295
[2025-04-28 21:21:34,264 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 30 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 16 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=58, Invalid=812, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:34,265 INFO  L437           NwaCegarLoop]: 252 mSDtfsCounter, 1 mSDsluCounter, 6762 mSDsCounter, 0 mSdLazyCounter, 797 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 7014 SdHoareTripleChecker+Invalid, 797 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 797 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,265 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 7014 Invalid, 797 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 797 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:34,266 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 295 states.
[2025-04-28 21:21:34,278 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 295 to 295.
[2025-04-28 21:21:34,279 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 295 states, 132 states have (on average 1.0) internal successors, (132), 132 states have internal predecessors, (132), 71 states have call successors, (84), 71 states have call predecessors, (84), 91 states have return successors, (105), 91 states have call predecessors, (105), 71 states have call successors, (105)
[2025-04-28 21:21:34,281 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 295 states to 295 states and 321 transitions.
[2025-04-28 21:21:34,281 INFO  L79                 Accepts]: Start accepts. Automaton has 295 states and 321 transitions. Word has length 124
[2025-04-28 21:21:34,282 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,282 INFO  L485      AbstractCegarLoop]: Abstraction has 295 states and 321 transitions.
[2025-04-28 21:21:34,282 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 30 states, 28 states have (on average 1.8571428571428572) internal successors, (52), 30 states have internal predecessors, (52), 4 states have call successors, (36), 1 states have call predecessors, (36), 28 states have return successors, (36), 28 states have call predecessors, (36), 4 states have call successors, (36)
[2025-04-28 21:21:34,282 INFO  L278                IsEmpty]: Start isEmpty. Operand 295 states and 321 transitions.
[2025-04-28 21:21:34,284 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 132
[2025-04-28 21:21:34,285 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,285 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,285 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:34,285 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,285 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,286 INFO  L85        PathProgramCache]: Analyzing trace with hash -359385281, now seen corresponding path program 1 times
[2025-04-28 21:21:34,286 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,286 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [355898638]
[2025-04-28 21:21:34,286 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,286 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,340 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 131 statements into 1 equivalence classes.
[2025-04-28 21:21:34,365 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 131 of 131 statements.
[2025-04-28 21:21:34,365 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,365 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,336 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:35,336 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,337 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [355898638]
[2025-04-28 21:21:35,337 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [355898638] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,337 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:35,337 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [15] imperfect sequences [] total 15
[2025-04-28 21:21:35,337 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2113814518]
[2025-04-28 21:21:35,337 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,338 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:35,338 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,338 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:35,338 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=182, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:35,339 INFO  L87              Difference]: Start difference. First operand 295 states and 321 transitions. Second operand  has 15 states, 13 states have (on average 4.230769230769231) internal successors, (55), 15 states have internal predecessors, (55), 4 states have call successors, (38), 1 states have call predecessors, (38), 13 states have return successors, (38), 13 states have call predecessors, (38), 4 states have call successors, (38)
[2025-04-28 21:21:35,540 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,540 INFO  L93              Difference]: Finished difference Result 283 states and 308 transitions.
[2025-04-28 21:21:35,541 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:35,541 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 13 states have (on average 4.230769230769231) internal successors, (55), 15 states have internal predecessors, (55), 4 states have call successors, (38), 1 states have call predecessors, (38), 13 states have return successors, (38), 13 states have call predecessors, (38), 4 states have call successors, (38) Word has length 131
[2025-04-28 21:21:35,541 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,543 INFO  L225             Difference]: With dead ends: 283
[2025-04-28 21:21:35,543 INFO  L226             Difference]: Without dead ends: 283
[2025-04-28 21:21:35,543 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 23 GetRequests, 10 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=28, Invalid=182, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:35,544 INFO  L437           NwaCegarLoop]: 268 mSDtfsCounter, 2 mSDsluCounter, 3198 mSDsCounter, 0 mSdLazyCounter, 163 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 3466 SdHoareTripleChecker+Invalid, 163 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 163 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,544 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 3466 Invalid, 163 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 163 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:35,545 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 283 states.
[2025-04-28 21:21:35,554 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 283 to 283.
[2025-04-28 21:21:35,556 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 283 states, 126 states have (on average 1.0) internal successors, (126), 126 states have internal predecessors, (126), 71 states have call successors, (84), 71 states have call predecessors, (84), 85 states have return successors, (98), 85 states have call predecessors, (98), 71 states have call successors, (98)
[2025-04-28 21:21:35,559 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 283 states to 283 states and 308 transitions.
[2025-04-28 21:21:35,560 INFO  L79                 Accepts]: Start accepts. Automaton has 283 states and 308 transitions. Word has length 131
[2025-04-28 21:21:35,560 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,560 INFO  L485      AbstractCegarLoop]: Abstraction has 283 states and 308 transitions.
[2025-04-28 21:21:35,561 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 13 states have (on average 4.230769230769231) internal successors, (55), 15 states have internal predecessors, (55), 4 states have call successors, (38), 1 states have call predecessors, (38), 13 states have return successors, (38), 13 states have call predecessors, (38), 4 states have call successors, (38)
[2025-04-28 21:21:35,562 INFO  L278                IsEmpty]: Start isEmpty. Operand 283 states and 308 transitions.
[2025-04-28 21:21:35,563 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 133
[2025-04-28 21:21:35,563 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,564 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,564 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:35,564 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,564 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,564 INFO  L85        PathProgramCache]: Analyzing trace with hash 1398655554, now seen corresponding path program 1 times
[2025-04-28 21:21:35,564 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,564 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [138371241]
[2025-04-28 21:21:35,564 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,565 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,602 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 132 statements into 1 equivalence classes.
[2025-04-28 21:21:35,619 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 132 of 132 statements.
[2025-04-28 21:21:35,619 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,619 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,981 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:37,981 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,981 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [138371241]
[2025-04-28 21:21:37,981 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [138371241] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,981 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:37,982 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [38] imperfect sequences [] total 38
[2025-04-28 21:21:37,982 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1182317371]
[2025-04-28 21:21:37,982 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,982 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 38 states
[2025-04-28 21:21:37,982 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,983 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 38 interpolants.
[2025-04-28 21:21:37,983 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=75, Invalid=1331, Unknown=0, NotChecked=0, Total=1406
[2025-04-28 21:21:37,984 INFO  L87              Difference]: Start difference. First operand 283 states and 308 transitions. Second operand  has 38 states, 34 states have (on average 1.6470588235294117) internal successors, (56), 38 states have internal predecessors, (56), 6 states have call successors, (38), 1 states have call predecessors, (38), 34 states have return successors, (38), 34 states have call predecessors, (38), 6 states have call successors, (38)
[2025-04-28 21:21:39,029 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,030 INFO  L93              Difference]: Finished difference Result 287 states and 312 transitions.
[2025-04-28 21:21:39,030 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 38 states. 
[2025-04-28 21:21:39,031 INFO  L79                 Accepts]: Start accepts. Automaton has  has 38 states, 34 states have (on average 1.6470588235294117) internal successors, (56), 38 states have internal predecessors, (56), 6 states have call successors, (38), 1 states have call predecessors, (38), 34 states have return successors, (38), 34 states have call predecessors, (38), 6 states have call successors, (38) Word has length 132
[2025-04-28 21:21:39,031 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,033 INFO  L225             Difference]: With dead ends: 287
[2025-04-28 21:21:39,033 INFO  L226             Difference]: Without dead ends: 287
[2025-04-28 21:21:39,034 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 39 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 37 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 41 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=79, Invalid=1403, Unknown=0, NotChecked=0, Total=1482
[2025-04-28 21:21:39,034 INFO  L437           NwaCegarLoop]: 247 mSDtfsCounter, 4 mSDsluCounter, 8340 mSDsCounter, 0 mSdLazyCounter, 1173 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 8587 SdHoareTripleChecker+Invalid, 1173 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 1173 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,035 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 8587 Invalid, 1173 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 1173 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:21:39,036 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 287 states.
[2025-04-28 21:21:39,044 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 287 to 287.
[2025-04-28 21:21:39,045 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 287 states, 128 states have (on average 1.0) internal successors, (128), 128 states have internal predecessors, (128), 71 states have call successors, (84), 71 states have call predecessors, (84), 87 states have return successors, (100), 87 states have call predecessors, (100), 71 states have call successors, (100)
[2025-04-28 21:21:39,046 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 287 states to 287 states and 312 transitions.
[2025-04-28 21:21:39,047 INFO  L79                 Accepts]: Start accepts. Automaton has 287 states and 312 transitions. Word has length 132
[2025-04-28 21:21:39,047 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,047 INFO  L485      AbstractCegarLoop]: Abstraction has 287 states and 312 transitions.
[2025-04-28 21:21:39,047 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 38 states, 34 states have (on average 1.6470588235294117) internal successors, (56), 38 states have internal predecessors, (56), 6 states have call successors, (38), 1 states have call predecessors, (38), 34 states have return successors, (38), 34 states have call predecessors, (38), 6 states have call successors, (38)
[2025-04-28 21:21:39,047 INFO  L278                IsEmpty]: Start isEmpty. Operand 287 states and 312 transitions.
[2025-04-28 21:21:39,049 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 140
[2025-04-28 21:21:39,049 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,049 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,049 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:39,049 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,050 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,050 INFO  L85        PathProgramCache]: Analyzing trace with hash 1913965572, now seen corresponding path program 1 times
[2025-04-28 21:21:39,050 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,050 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1872852189]
[2025-04-28 21:21:39,050 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,050 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,091 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 139 statements into 1 equivalence classes.
[2025-04-28 21:21:39,110 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 139 of 139 statements.
[2025-04-28 21:21:39,110 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,110 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
