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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:25,138 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:25,231 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_feff3f60-728e-4b42-a03b-c1db94f1a791/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:25,237 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:25,237 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:25,269 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:25,269 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:25,269 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:25,270 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:25,270 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:25,270 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:25,270 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:25,270 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:25,270 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:25,270 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:25,271 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:25,271 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:25,271 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:25,271 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:25,271 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:25,273 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:25,273 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:25,274 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:25,274 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:25,274 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:25,275 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:25,275 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:25,586 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:25,597 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:25,599 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:25,602 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:25,603 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:25,604 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_feff3f60-728e-4b42-a03b-c1db94f1a791/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-194.smt2
[2025-04-28 21:21:25,606 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:25,610 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:25,835 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_feff3f60-728e-4b42-a03b-c1db94f1a791/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-194.smt2
[2025-04-28 21:21:25,839 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:25,840 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:25,841 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:25,841 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:25,841 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:25,843 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,867 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25 Unit
[2025-04-28 21:21:25,867 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:25,868 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:25,868 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:25,868 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:25,879 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,879 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,910 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,911 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,918 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,923 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,925 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,926 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,931 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,943 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:25,943 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:25,944 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:25,944 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:25,945 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (1/1) ...
[2025-04-28 21:21:25,947 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:25,960 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:25,975 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:25,980 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:25,992 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:25,992 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:25,993 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:25,993 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h33 given in one single declaration
[2025-04-28 21:21:25,993 INFO  L130     BoogieDeclarations]: Found specification of procedure h33
[2025-04-28 21:21:25,993 INFO  L138     BoogieDeclarations]: Found implementation of procedure h33
[2025-04-28 21:21:25,993 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h29 given in one single declaration
[2025-04-28 21:21:25,994 INFO  L130     BoogieDeclarations]: Found specification of procedure h29
[2025-04-28 21:21:25,994 INFO  L138     BoogieDeclarations]: Found implementation of procedure h29
[2025-04-28 21:21:25,994 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h28 given in one single declaration
[2025-04-28 21:21:25,994 INFO  L130     BoogieDeclarations]: Found specification of procedure h28
[2025-04-28 21:21:25,994 INFO  L138     BoogieDeclarations]: Found implementation of procedure h28
[2025-04-28 21:21:25,994 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h27 given in one single declaration
[2025-04-28 21:21:25,994 INFO  L130     BoogieDeclarations]: Found specification of procedure h27
[2025-04-28 21:21:25,994 INFO  L138     BoogieDeclarations]: Found implementation of procedure h27
[2025-04-28 21:21:25,994 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h26 given in one single declaration
[2025-04-28 21:21:25,994 INFO  L130     BoogieDeclarations]: Found specification of procedure h26
[2025-04-28 21:21:25,994 INFO  L138     BoogieDeclarations]: Found implementation of procedure h26
[2025-04-28 21:21:25,994 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h35 given in one single declaration
[2025-04-28 21:21:25,995 INFO  L130     BoogieDeclarations]: Found specification of procedure h35
[2025-04-28 21:21:25,995 INFO  L138     BoogieDeclarations]: Found implementation of procedure h35
[2025-04-28 21:21:25,995 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h34 given in one single declaration
[2025-04-28 21:21:25,995 INFO  L130     BoogieDeclarations]: Found specification of procedure h34
[2025-04-28 21:21:25,995 INFO  L138     BoogieDeclarations]: Found implementation of procedure h34
[2025-04-28 21:21:25,995 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h25 given in one single declaration
[2025-04-28 21:21:25,995 INFO  L130     BoogieDeclarations]: Found specification of procedure h25
[2025-04-28 21:21:25,995 INFO  L138     BoogieDeclarations]: Found implementation of procedure h25
[2025-04-28 21:21:25,995 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h24 given in one single declaration
[2025-04-28 21:21:25,995 INFO  L130     BoogieDeclarations]: Found specification of procedure h24
[2025-04-28 21:21:25,995 INFO  L138     BoogieDeclarations]: Found implementation of procedure h24
[2025-04-28 21:21:25,995 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h23 given in one single declaration
[2025-04-28 21:21:25,995 INFO  L130     BoogieDeclarations]: Found specification of procedure h23
[2025-04-28 21:21:25,996 INFO  L138     BoogieDeclarations]: Found implementation of procedure h23
[2025-04-28 21:21:25,996 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h22 given in one single declaration
[2025-04-28 21:21:25,996 INFO  L130     BoogieDeclarations]: Found specification of procedure h22
[2025-04-28 21:21:25,996 INFO  L138     BoogieDeclarations]: Found implementation of procedure h22
[2025-04-28 21:21:25,996 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h21 given in one single declaration
[2025-04-28 21:21:25,996 INFO  L130     BoogieDeclarations]: Found specification of procedure h21
[2025-04-28 21:21:25,996 INFO  L138     BoogieDeclarations]: Found implementation of procedure h21
[2025-04-28 21:21:25,996 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h20 given in one single declaration
[2025-04-28 21:21:25,996 INFO  L130     BoogieDeclarations]: Found specification of procedure h20
[2025-04-28 21:21:25,996 INFO  L138     BoogieDeclarations]: Found implementation of procedure h20
[2025-04-28 21:21:25,996 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h17 given in one single declaration
[2025-04-28 21:21:25,996 INFO  L130     BoogieDeclarations]: Found specification of procedure h17
[2025-04-28 21:21:25,996 INFO  L138     BoogieDeclarations]: Found implementation of procedure h17
[2025-04-28 21:21:25,997 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h16 given in one single declaration
[2025-04-28 21:21:25,997 INFO  L130     BoogieDeclarations]: Found specification of procedure h16
[2025-04-28 21:21:25,997 INFO  L138     BoogieDeclarations]: Found implementation of procedure h16
[2025-04-28 21:21:25,997 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h15 given in one single declaration
[2025-04-28 21:21:25,997 INFO  L130     BoogieDeclarations]: Found specification of procedure h15
[2025-04-28 21:21:25,997 INFO  L138     BoogieDeclarations]: Found implementation of procedure h15
[2025-04-28 21:21:25,997 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h14 given in one single declaration
[2025-04-28 21:21:25,997 INFO  L130     BoogieDeclarations]: Found specification of procedure h14
[2025-04-28 21:21:25,997 INFO  L138     BoogieDeclarations]: Found implementation of procedure h14
[2025-04-28 21:21:25,997 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h10 given in one single declaration
[2025-04-28 21:21:25,998 INFO  L130     BoogieDeclarations]: Found specification of procedure h10
[2025-04-28 21:21:25,998 INFO  L138     BoogieDeclarations]: Found implementation of procedure h10
[2025-04-28 21:21:25,998 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h9 given in one single declaration
[2025-04-28 21:21:25,998 INFO  L130     BoogieDeclarations]: Found specification of procedure h9
[2025-04-28 21:21:25,998 INFO  L138     BoogieDeclarations]: Found implementation of procedure h9
[2025-04-28 21:21:25,998 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h8 given in one single declaration
[2025-04-28 21:21:25,998 INFO  L130     BoogieDeclarations]: Found specification of procedure h8
[2025-04-28 21:21:25,999 INFO  L138     BoogieDeclarations]: Found implementation of procedure h8
[2025-04-28 21:21:26,000 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h7 given in one single declaration
[2025-04-28 21:21:26,000 INFO  L130     BoogieDeclarations]: Found specification of procedure h7
[2025-04-28 21:21:26,000 INFO  L138     BoogieDeclarations]: Found implementation of procedure h7
[2025-04-28 21:21:26,000 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h6 given in one single declaration
[2025-04-28 21:21:26,000 INFO  L130     BoogieDeclarations]: Found specification of procedure h6
[2025-04-28 21:21:26,000 INFO  L138     BoogieDeclarations]: Found implementation of procedure h6
[2025-04-28 21:21:26,000 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h5 given in one single declaration
[2025-04-28 21:21:26,000 INFO  L130     BoogieDeclarations]: Found specification of procedure h5
[2025-04-28 21:21:26,000 INFO  L138     BoogieDeclarations]: Found implementation of procedure h5
[2025-04-28 21:21:26,000 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h4 given in one single declaration
[2025-04-28 21:21:26,000 INFO  L130     BoogieDeclarations]: Found specification of procedure h4
[2025-04-28 21:21:26,000 INFO  L138     BoogieDeclarations]: Found implementation of procedure h4
[2025-04-28 21:21:26,000 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h3 given in one single declaration
[2025-04-28 21:21:26,001 INFO  L130     BoogieDeclarations]: Found specification of procedure h3
[2025-04-28 21:21:26,001 INFO  L138     BoogieDeclarations]: Found implementation of procedure h3
[2025-04-28 21:21:26,001 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h2 given in one single declaration
[2025-04-28 21:21:26,001 INFO  L130     BoogieDeclarations]: Found specification of procedure h2
[2025-04-28 21:21:26,001 INFO  L138     BoogieDeclarations]: Found implementation of procedure h2
[2025-04-28 21:21:26,001 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h1 given in one single declaration
[2025-04-28 21:21:26,001 INFO  L130     BoogieDeclarations]: Found specification of procedure h1
[2025-04-28 21:21:26,001 INFO  L138     BoogieDeclarations]: Found implementation of procedure h1
[2025-04-28 21:21:26,001 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h36 given in one single declaration
[2025-04-28 21:21:26,001 INFO  L130     BoogieDeclarations]: Found specification of procedure h36
[2025-04-28 21:21:26,001 INFO  L138     BoogieDeclarations]: Found implementation of procedure h36
[2025-04-28 21:21:26,001 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h32 given in one single declaration
[2025-04-28 21:21:26,001 INFO  L130     BoogieDeclarations]: Found specification of procedure h32
[2025-04-28 21:21:26,001 INFO  L138     BoogieDeclarations]: Found implementation of procedure h32
[2025-04-28 21:21:26,001 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h31 given in one single declaration
[2025-04-28 21:21:26,002 INFO  L130     BoogieDeclarations]: Found specification of procedure h31
[2025-04-28 21:21:26,002 INFO  L138     BoogieDeclarations]: Found implementation of procedure h31
[2025-04-28 21:21:26,002 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h30 given in one single declaration
[2025-04-28 21:21:26,002 INFO  L130     BoogieDeclarations]: Found specification of procedure h30
[2025-04-28 21:21:26,002 INFO  L138     BoogieDeclarations]: Found implementation of procedure h30
[2025-04-28 21:21:26,002 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h19 given in one single declaration
[2025-04-28 21:21:26,002 INFO  L130     BoogieDeclarations]: Found specification of procedure h19
[2025-04-28 21:21:26,002 INFO  L138     BoogieDeclarations]: Found implementation of procedure h19
[2025-04-28 21:21:26,002 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure h18 given in one single declaration
[2025-04-28 21:21:26,002 INFO  L130     BoogieDeclarations]: Found specification of procedure h18
[2025-04-28 21:21:26,002 INFO  L138     BoogieDeclarations]: Found implementation of procedure h18
[2025-04-28 21:21:26,002 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:26,002 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:26,003 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:26,136 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:26,139 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:26,403 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:26,405 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:26,427 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:26,427 INFO  L312             CfgBuilder]: Removed 22 assume(true) statements.
[2025-04-28 21:21:26,428 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:26 BoogieIcfgContainer
[2025-04-28 21:21:26,428 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:26,431 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:26,432 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:26,436 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:26,436 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:25" (1/3) ...
[2025-04-28 21:21:26,436 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5d252966 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:26, skipping insertion in model container
[2025-04-28 21:21:26,437 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:25" (2/3) ...
[2025-04-28 21:21:26,437 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5d252966 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:26, skipping insertion in model container
[2025-04-28 21:21:26,437 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:26" (3/3) ...
[2025-04-28 21:21:26,440 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:26,459 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:26,462 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 35 procedures, 121 locations, 163 edges, 35 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:26,506 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:26,528 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;@99f779d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:26,529 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:26,533 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 121 states, 51 states have (on average 1.0196078431372548) internal successors, (52), 52 states have internal predecessors, (52), 34 states have call successors, (37), 34 states have call predecessors, (37), 34 states have return successors, (37), 34 states have call predecessors, (37), 34 states have call successors, (37)
[2025-04-28 21:21:26,550 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 89
[2025-04-28 21:21:26,551 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,553 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]
[2025-04-28 21:21:26,554 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,558 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,559 INFO  L85        PathProgramCache]: Analyzing trace with hash 137525176, now seen corresponding path program 1 times
[2025-04-28 21:21:26,564 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,564 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1944159566]
[2025-04-28 21:21:26,565 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,565 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,617 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 88 statements into 1 equivalence classes.
[2025-04-28 21:21:26,699 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 88 of 88 statements.
[2025-04-28 21:21:26,702 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,703 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,997 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,998 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,998 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1944159566]
[2025-04-28 21:21:27,999 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1944159566] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,999 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,003 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [24] imperfect sequences [] total 24
[2025-04-28 21:21:28,005 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [533752588]
[2025-04-28 21:21:28,005 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,009 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:28,009 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,041 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:28,042 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=45, Invalid=507, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:28,044 INFO  L87              Difference]: Start difference. First operand  has 121 states, 51 states have (on average 1.0196078431372548) internal successors, (52), 52 states have internal predecessors, (52), 34 states have call successors, (37), 34 states have call predecessors, (37), 34 states have return successors, (37), 34 states have call predecessors, (37), 34 states have call successors, (37) Second operand  has 24 states, 23 states have (on average 1.565217391304348) internal successors, (36), 24 states have internal predecessors, (36), 3 states have call successors, (26), 1 states have call predecessors, (26), 23 states have return successors, (26), 23 states have call predecessors, (26), 3 states have call successors, (26)
[2025-04-28 21:21:28,751 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,752 INFO  L93              Difference]: Finished difference Result 155 states and 162 transitions.
[2025-04-28 21:21:28,753 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 24 states. 
[2025-04-28 21:21:28,755 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 23 states have (on average 1.565217391304348) internal successors, (36), 24 states have internal predecessors, (36), 3 states have call successors, (26), 1 states have call predecessors, (26), 23 states have return successors, (26), 23 states have call predecessors, (26), 3 states have call successors, (26) Word has length 88
[2025-04-28 21:21:28,756 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,790 INFO  L225             Difference]: With dead ends: 155
[2025-04-28 21:21:28,790 INFO  L226             Difference]: Without dead ends: 155
[2025-04-28 21:21:28,792 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 25 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=45, Invalid=507, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:28,808 INFO  L437           NwaCegarLoop]: 100 mSDtfsCounter, 1 mSDsluCounter, 2183 mSDsCounter, 0 mSdLazyCounter, 558 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 2283 SdHoareTripleChecker+Invalid, 558 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 558 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,809 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 2283 Invalid, 558 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 558 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:28,835 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 155 states.
[2025-04-28 21:21:28,888 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 155 to 155.
[2025-04-28 21:21:28,889 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 155 states, 68 states have (on average 1.0) internal successors, (68), 68 states have internal predecessors, (68), 34 states have call successors, (37), 34 states have call predecessors, (37), 52 states have return successors, (57), 52 states have call predecessors, (57), 34 states have call successors, (57)
[2025-04-28 21:21:28,894 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 155 states to 155 states and 162 transitions.
[2025-04-28 21:21:28,896 INFO  L79                 Accepts]: Start accepts. Automaton has 155 states and 162 transitions. Word has length 88
[2025-04-28 21:21:28,896 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,897 INFO  L485      AbstractCegarLoop]: Abstraction has 155 states and 162 transitions.
[2025-04-28 21:21:28,897 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 23 states have (on average 1.565217391304348) internal successors, (36), 24 states have internal predecessors, (36), 3 states have call successors, (26), 1 states have call predecessors, (26), 23 states have return successors, (26), 23 states have call predecessors, (26), 3 states have call successors, (26)
[2025-04-28 21:21:28,897 INFO  L278                IsEmpty]: Start isEmpty. Operand 155 states and 162 transitions.
[2025-04-28 21:21:28,900 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 103
[2025-04-28 21:21:28,900 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,900 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,901 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:28,901 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,902 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,902 INFO  L85        PathProgramCache]: Analyzing trace with hash 548411168, now seen corresponding path program 1 times
[2025-04-28 21:21:28,902 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,902 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1291802324]
[2025-04-28 21:21:28,903 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,903 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,937 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 102 statements into 1 equivalence classes.
[2025-04-28 21:21:28,959 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 102 of 102 statements.
[2025-04-28 21:21:28,959 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,959 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,910 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:29,911 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,911 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1291802324]
[2025-04-28 21:21:29,911 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1291802324] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,911 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:29,911 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [26] imperfect sequences [] total 26
[2025-04-28 21:21:29,912 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [879592848]
[2025-04-28 21:21:29,912 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,913 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:29,914 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,915 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:29,916 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=49, Invalid=601, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:29,917 INFO  L87              Difference]: Start difference. First operand 155 states and 162 transitions. Second operand  has 26 states, 25 states have (on average 1.6) internal successors, (40), 26 states have internal predecessors, (40), 3 states have call successors, (29), 1 states have call predecessors, (29), 25 states have return successors, (29), 25 states have call predecessors, (29), 3 states have call successors, (29)
[2025-04-28 21:21:30,460 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,461 INFO  L93              Difference]: Finished difference Result 183 states and 192 transitions.
[2025-04-28 21:21:30,461 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 26 states. 
[2025-04-28 21:21:30,461 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 25 states have (on average 1.6) internal successors, (40), 26 states have internal predecessors, (40), 3 states have call successors, (29), 1 states have call predecessors, (29), 25 states have return successors, (29), 25 states have call predecessors, (29), 3 states have call successors, (29) Word has length 102
[2025-04-28 21:21:30,462 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,464 INFO  L225             Difference]: With dead ends: 183
[2025-04-28 21:21:30,464 INFO  L226             Difference]: Without dead ends: 183
[2025-04-28 21:21:30,464 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 29 GetRequests, 5 SyntacticMatches, 0 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=49, Invalid=601, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:30,465 INFO  L437           NwaCegarLoop]: 98 mSDtfsCounter, 1 mSDsluCounter, 2336 mSDsCounter, 0 mSdLazyCounter, 655 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 2434 SdHoareTripleChecker+Invalid, 655 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 655 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,466 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 2434 Invalid, 655 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 655 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:30,467 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 183 states.
[2025-04-28 21:21:30,488 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 183 to 159.
[2025-04-28 21:21:30,490 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 159 states, 70 states have (on average 1.0) internal successors, (70), 70 states have internal predecessors, (70), 34 states have call successors, (37), 34 states have call predecessors, (37), 54 states have return successors, (59), 54 states have call predecessors, (59), 34 states have call successors, (59)
[2025-04-28 21:21:30,492 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 159 states to 159 states and 166 transitions.
[2025-04-28 21:21:30,494 INFO  L79                 Accepts]: Start accepts. Automaton has 159 states and 166 transitions. Word has length 102
[2025-04-28 21:21:30,495 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,495 INFO  L485      AbstractCegarLoop]: Abstraction has 159 states and 166 transitions.
[2025-04-28 21:21:30,496 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 25 states have (on average 1.6) internal successors, (40), 26 states have internal predecessors, (40), 3 states have call successors, (29), 1 states have call predecessors, (29), 25 states have return successors, (29), 25 states have call predecessors, (29), 3 states have call successors, (29)
[2025-04-28 21:21:30,496 INFO  L278                IsEmpty]: Start isEmpty. Operand 159 states and 166 transitions.
[2025-04-28 21:21:30,499 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 110
[2025-04-28 21:21:30,502 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,503 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,503 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:30,503 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,504 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,504 INFO  L85        PathProgramCache]: Analyzing trace with hash 88305732, now seen corresponding path program 1 times
[2025-04-28 21:21:30,504 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,504 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [117680202]
[2025-04-28 21:21:30,504 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,504 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,531 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 109 statements into 1 equivalence classes.
[2025-04-28 21:21:30,538 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 109 of 109 statements.
[2025-04-28 21:21:30,538 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,538 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,822 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 8 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:30,822 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,822 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [117680202]
[2025-04-28 21:21:30,822 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [117680202] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,822 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:30,822 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:30,822 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1941038292]
[2025-04-28 21:21:30,823 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,823 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:30,823 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,824 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:30,824 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:30,824 INFO  L87              Difference]: Start difference. First operand 159 states and 166 transitions. Second operand  has 9 states, 8 states have (on average 5.5) internal successors, (44), 9 states have internal predecessors, (44), 3 states have call successors, (29), 1 states have call predecessors, (29), 8 states have return successors, (32), 8 states have call predecessors, (32), 3 states have call successors, (32)
[2025-04-28 21:21:30,948 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,948 INFO  L93              Difference]: Finished difference Result 183 states and 197 transitions.
[2025-04-28 21:21:30,949 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:30,949 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 8 states have (on average 5.5) internal successors, (44), 9 states have internal predecessors, (44), 3 states have call successors, (29), 1 states have call predecessors, (29), 8 states have return successors, (32), 8 states have call predecessors, (32), 3 states have call successors, (32) Word has length 109
[2025-04-28 21:21:30,950 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,952 INFO  L225             Difference]: With dead ends: 183
[2025-04-28 21:21:30,952 INFO  L226             Difference]: Without dead ends: 179
[2025-04-28 21:21:30,952 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:30,957 INFO  L437           NwaCegarLoop]: 133 mSDtfsCounter, 3 mSDsluCounter, 904 mSDsCounter, 0 mSdLazyCounter, 87 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 1037 SdHoareTripleChecker+Invalid, 93 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 87 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,957 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 1037 Invalid, 93 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 87 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:30,958 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 179 states.
[2025-04-28 21:21:30,979 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 179 to 172.
[2025-04-28 21:21:30,980 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 172 states, 75 states have (on average 1.0) internal successors, (75), 75 states have internal predecessors, (75), 38 states have call successors, (42), 38 states have call predecessors, (42), 58 states have return successors, (66), 58 states have call predecessors, (66), 38 states have call successors, (66)
[2025-04-28 21:21:30,985 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 172 states to 172 states and 183 transitions.
[2025-04-28 21:21:30,985 INFO  L79                 Accepts]: Start accepts. Automaton has 172 states and 183 transitions. Word has length 109
[2025-04-28 21:21:30,986 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,986 INFO  L485      AbstractCegarLoop]: Abstraction has 172 states and 183 transitions.
[2025-04-28 21:21:30,986 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 8 states have (on average 5.5) internal successors, (44), 9 states have internal predecessors, (44), 3 states have call successors, (29), 1 states have call predecessors, (29), 8 states have return successors, (32), 8 states have call predecessors, (32), 3 states have call successors, (32)
[2025-04-28 21:21:30,986 INFO  L278                IsEmpty]: Start isEmpty. Operand 172 states and 183 transitions.
[2025-04-28 21:21:30,992 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 155
[2025-04-28 21:21:30,992 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,992 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,993 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:30,993 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,993 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,993 INFO  L85        PathProgramCache]: Analyzing trace with hash 693553294, now seen corresponding path program 1 times
[2025-04-28 21:21:30,993 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,993 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1154092010]
[2025-04-28 21:21:30,993 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,994 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,025 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 154 statements into 1 equivalence classes.
[2025-04-28 21:21:31,049 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 154 of 154 statements.
[2025-04-28 21:21:31,049 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,049 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,949 INFO  L134       CoverageAnalysis]: Checked inductivity of 52 backedges. 26 proven. 3 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:31,949 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,949 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1154092010]
[2025-04-28 21:21:31,949 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1154092010] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,949 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1446853722]
[2025-04-28 21:21:31,949 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,949 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,954 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,958 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:31,961 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:32,103 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 154 statements into 1 equivalence classes.
[2025-04-28 21:21:32,257 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 154 of 154 statements.
[2025-04-28 21:21:32,257 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,258 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,263 INFO  L256         TraceCheckSpWp]: Trace formula consists of 936 conjuncts, 30 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:32,277 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,614 INFO  L134       CoverageAnalysis]: Checked inductivity of 52 backedges. 26 proven. 3 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:32,614 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:57,687 INFO  L134       CoverageAnalysis]: Checked inductivity of 52 backedges. 26 proven. 3 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:57,687 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1446853722] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:57,687 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:57,687 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 18, 18] total 27
[2025-04-28 21:21:57,687 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [699436256]
[2025-04-28 21:21:57,687 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,692 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:21:57,692 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,693 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:21:57,693 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=65, Invalid=637, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:57,694 INFO  L87              Difference]: Start difference. First operand 172 states and 183 transitions. Second operand  has 27 states, 21 states have (on average 3.238095238095238) internal successors, (68), 27 states have internal predecessors, (68), 9 states have call successors, (38), 1 states have call predecessors, (38), 21 states have return successors, (54), 21 states have call predecessors, (54), 9 states have call successors, (54)
[2025-04-28 21:21:58,011 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,011 INFO  L93              Difference]: Finished difference Result 220 states and 233 transitions.
[2025-04-28 21:21:58,012 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:21:58,012 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 21 states have (on average 3.238095238095238) internal successors, (68), 27 states have internal predecessors, (68), 9 states have call successors, (38), 1 states have call predecessors, (38), 21 states have return successors, (54), 21 states have call predecessors, (54), 9 states have call successors, (54) Word has length 154
[2025-04-28 21:21:58,013 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,016 INFO  L225             Difference]: With dead ends: 220
[2025-04-28 21:21:58,016 INFO  L226             Difference]: Without dead ends: 212
[2025-04-28 21:21:58,016 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 326 GetRequests, 286 SyntacticMatches, 14 SemanticMatches, 26 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 163 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=71, Invalid=685, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:58,017 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 8 mSDsluCounter, 1827 mSDsCounter, 0 mSdLazyCounter, 280 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 1936 SdHoareTripleChecker+Invalid, 284 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 280 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,017 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 1936 Invalid, 284 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 280 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:58,022 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 212 states.
[2025-04-28 21:21:58,045 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 212 to 192.
[2025-04-28 21:21:58,045 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 192 states, 85 states have (on average 1.0) internal successors, (85), 85 states have internal predecessors, (85), 38 states have call successors, (42), 38 states have call predecessors, (42), 68 states have return successors, (78), 68 states have call predecessors, (78), 38 states have call successors, (78)
[2025-04-28 21:21:58,047 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 192 states to 192 states and 205 transitions.
[2025-04-28 21:21:58,047 INFO  L79                 Accepts]: Start accepts. Automaton has 192 states and 205 transitions. Word has length 154
[2025-04-28 21:21:58,049 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,049 INFO  L485      AbstractCegarLoop]: Abstraction has 192 states and 205 transitions.
[2025-04-28 21:21:58,049 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 21 states have (on average 3.238095238095238) internal successors, (68), 27 states have internal predecessors, (68), 9 states have call successors, (38), 1 states have call predecessors, (38), 21 states have return successors, (54), 21 states have call predecessors, (54), 9 states have call successors, (54)
[2025-04-28 21:21:58,049 INFO  L278                IsEmpty]: Start isEmpty. Operand 192 states and 205 transitions.
[2025-04-28 21:21:58,053 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 169
[2025-04-28 21:21:58,054 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,054 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,062 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:58,255 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,256 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,260 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,260 INFO  L85        PathProgramCache]: Analyzing trace with hash 1887456694, now seen corresponding path program 1 times
[2025-04-28 21:21:58,260 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,260 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1906687511]
[2025-04-28 21:21:58,260 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,260 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,306 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 168 statements into 1 equivalence classes.
[2025-04-28 21:21:58,335 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 168 of 168 statements.
[2025-04-28 21:21:58,336 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,336 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
