./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-041.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:38,394 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:38,493 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e345f915-14f3-4a2d-b4d1-6160375a43ec/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:38,497 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:38,498 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:38,541 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:38,543 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:38,543 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:38,543 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:38,543 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:38,544 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:38,544 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:38,544 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:38,544 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:38,544 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:38,544 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:38,544 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:38,545 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:38,545 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:38,545 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:38,545 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:38,545 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:38,545 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:38,545 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:38,546 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:38,546 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:38,547 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:38,902 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:38,914 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:38,917 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:38,920 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:38,921 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:38,923 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e345f915-14f3-4a2d-b4d1-6160375a43ec/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-041.smt2
[2025-04-28 21:21:38,926 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:38,931 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:39,584 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e345f915-14f3-4a2d-b4d1-6160375a43ec/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-041.smt2
[2025-04-28 21:21:39,588 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:39,590 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:39,592 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:39,593 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:39,593 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:39,599 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,684 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39 Unit
[2025-04-28 21:21:39,688 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:39,693 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:39,693 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:39,693 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:39,712 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,712 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,769 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,769 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,791 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,794 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,797 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,803 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,806 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,830 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:39,831 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:39,832 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:39,832 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:39,833 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,836 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:39,863 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,883 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:39,887 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:39,903 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:39,904 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:39,904 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:39,904 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:39,904 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:39,904 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:39,904 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:39,904 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:39,904 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:39,905 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS__syn given in one single declaration
[2025-04-28 21:21:39,905 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS__syn
[2025-04-28 21:21:39,905 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS__syn
[2025-04-28 21:21:39,905 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS2__syn given in one single declaration
[2025-04-28 21:21:39,906 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS2__syn
[2025-04-28 21:21:39,906 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS2__syn
[2025-04-28 21:21:39,906 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS22__syn given in one single declaration
[2025-04-28 21:21:39,906 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS22__syn
[2025-04-28 21:21:39,906 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS22__syn
[2025-04-28 21:21:39,907 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcM__syn given in one single declaration
[2025-04-28 21:21:39,908 INFO  L130     BoogieDeclarations]: Found specification of procedure funcM__syn
[2025-04-28 21:21:39,908 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcM__syn
[2025-04-28 21:21:39,908 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS21__syn given in one single declaration
[2025-04-28 21:21:39,908 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS21__syn
[2025-04-28 21:21:39,908 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS21__syn
[2025-04-28 21:21:39,908 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB2__syn given in one single declaration
[2025-04-28 21:21:39,908 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB2__syn
[2025-04-28 21:21:39,908 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB2__syn
[2025-04-28 21:21:39,908 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS21__sem given in one single declaration
[2025-04-28 21:21:39,908 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS21__sem
[2025-04-28 21:21:39,908 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS21__sem
[2025-04-28 21:21:39,908 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS3__sem given in one single declaration
[2025-04-28 21:21:39,908 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS3__sem
[2025-04-28 21:21:39,909 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS3__sem
[2025-04-28 21:21:39,909 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS32__sem given in one single declaration
[2025-04-28 21:21:39,909 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS32__sem
[2025-04-28 21:21:39,909 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS32__sem
[2025-04-28 21:21:39,909 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcP__sem given in one single declaration
[2025-04-28 21:21:39,910 INFO  L130     BoogieDeclarations]: Found specification of procedure funcP__sem
[2025-04-28 21:21:39,910 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcP__sem
[2025-04-28 21:21:39,910 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS31__sem given in one single declaration
[2025-04-28 21:21:39,910 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS31__sem
[2025-04-28 21:21:39,910 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS31__sem
[2025-04-28 21:21:39,911 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__sem given in one single declaration
[2025-04-28 21:21:39,911 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__sem
[2025-04-28 21:21:39,911 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__sem
[2025-04-28 21:21:39,911 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcA__sem given in one single declaration
[2025-04-28 21:21:39,912 INFO  L130     BoogieDeclarations]: Found specification of procedure funcA__sem
[2025-04-28 21:21:39,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcA__sem
[2025-04-28 21:21:39,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB2__sem given in one single declaration
[2025-04-28 21:21:39,912 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB2__sem
[2025-04-28 21:21:39,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB2__sem
[2025-04-28 21:21:39,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS3__syn given in one single declaration
[2025-04-28 21:21:39,912 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS3__syn
[2025-04-28 21:21:39,912 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS3__syn
[2025-04-28 21:21:39,912 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS32__syn given in one single declaration
[2025-04-28 21:21:39,912 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS32__syn
[2025-04-28 21:21:39,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS32__syn
[2025-04-28 21:21:39,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcP__syn given in one single declaration
[2025-04-28 21:21:39,913 INFO  L130     BoogieDeclarations]: Found specification of procedure funcP__syn
[2025-04-28 21:21:39,913 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcP__syn
[2025-04-28 21:21:39,913 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS31__syn given in one single declaration
[2025-04-28 21:21:39,914 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS31__syn
[2025-04-28 21:21:39,914 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS31__syn
[2025-04-28 21:21:39,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__syn given in one single declaration
[2025-04-28 21:21:39,915 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__syn
[2025-04-28 21:21:39,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__syn
[2025-04-28 21:21:39,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcA__syn given in one single declaration
[2025-04-28 21:21:39,915 INFO  L130     BoogieDeclarations]: Found specification of procedure funcA__syn
[2025-04-28 21:21:39,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcA__syn
[2025-04-28 21:21:39,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS1__syn given in one single declaration
[2025-04-28 21:21:39,915 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS1__syn
[2025-04-28 21:21:39,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS1__syn
[2025-04-28 21:21:39,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__sem given in one single declaration
[2025-04-28 21:21:39,915 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__sem
[2025-04-28 21:21:39,915 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__sem
[2025-04-28 21:21:39,915 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS__sem given in one single declaration
[2025-04-28 21:21:39,916 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS__sem
[2025-04-28 21:21:39,916 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS__sem
[2025-04-28 21:21:39,916 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS1__sem given in one single declaration
[2025-04-28 21:21:39,916 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS1__sem
[2025-04-28 21:21:39,916 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS1__sem
[2025-04-28 21:21:39,916 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS2__sem given in one single declaration
[2025-04-28 21:21:39,917 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS2__sem
[2025-04-28 21:21:39,917 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS2__sem
[2025-04-28 21:21:39,917 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS22__sem given in one single declaration
[2025-04-28 21:21:39,917 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS22__sem
[2025-04-28 21:21:39,917 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS22__sem
[2025-04-28 21:21:39,917 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcM__sem given in one single declaration
[2025-04-28 21:21:39,918 INFO  L130     BoogieDeclarations]: Found specification of procedure funcM__sem
[2025-04-28 21:21:39,918 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcM__sem
[2025-04-28 21:21:39,918 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__sem given in one single declaration
[2025-04-28 21:21:39,918 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__sem
[2025-04-28 21:21:39,918 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__sem
[2025-04-28 21:21:39,918 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__syn given in one single declaration
[2025-04-28 21:21:39,918 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__syn
[2025-04-28 21:21:39,918 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__syn
[2025-04-28 21:21:39,918 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:39,919 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:39,919 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:40,324 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:40,327 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:41,006 INFO  L?                        ?]: Removed 120 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:41,006 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:41,026 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:41,026 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:41,027 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41 BoogieIcfgContainer
[2025-04-28 21:21:41,027 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:41,030 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:41,031 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:41,036 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:41,036 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:39" (1/3) ...
[2025-04-28 21:21:41,037 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6fd38ebb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,037 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (2/3) ...
[2025-04-28 21:21:41,038 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6fd38ebb and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,038 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41" (3/3) ...
[2025-04-28 21:21:41,039 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:41,057 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:41,060 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 33 procedures, 140 locations, 197 edges, 33 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:41,132 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:41,149 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;@48d11990, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:41,151 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:41,156 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 140 states, 65 states have (on average 1.1384615384615384) internal successors, (74), 70 states have internal predecessors, (74), 41 states have call successors, (41), 32 states have call predecessors, (41), 32 states have return successors, (41), 39 states have call predecessors, (41), 41 states have call successors, (41)
[2025-04-28 21:21:41,176 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 81
[2025-04-28 21:21:41,176 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,177 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,178 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,183 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,183 INFO  L85        PathProgramCache]: Analyzing trace with hash 660259248, now seen corresponding path program 1 times
[2025-04-28 21:21:41,193 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,193 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1368739081]
[2025-04-28 21:21:41,194 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,196 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,311 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 80 statements into 1 equivalence classes.
[2025-04-28 21:21:41,561 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 80 of 80 statements.
[2025-04-28 21:21:41,562 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,562 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,919 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:42,920 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,921 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1368739081]
[2025-04-28 21:21:42,921 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1368739081] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,922 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,926 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:42,927 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [308712620]
[2025-04-28 21:21:42,929 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,937 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:42,938 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,969 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:42,971 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:42,974 INFO  L87              Difference]: Start difference. First operand  has 140 states, 65 states have (on average 1.1384615384615384) internal successors, (74), 70 states have internal predecessors, (74), 41 states have call successors, (41), 32 states have call predecessors, (41), 32 states have return successors, (41), 39 states have call predecessors, (41), 41 states have call successors, (41) Second operand  has 8 states, 5 states have (on average 7.6) internal successors, (38), 7 states have internal predecessors, (38), 5 states have call successors, (20), 1 states have call predecessors, (20), 5 states have return successors, (20), 4 states have call predecessors, (20), 5 states have call successors, (20)
[2025-04-28 21:21:43,215 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,216 INFO  L93              Difference]: Finished difference Result 143 states and 160 transitions.
[2025-04-28 21:21:43,218 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:43,219 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 7.6) internal successors, (38), 7 states have internal predecessors, (38), 5 states have call successors, (20), 1 states have call predecessors, (20), 5 states have return successors, (20), 4 states have call predecessors, (20), 5 states have call successors, (20) Word has length 80
[2025-04-28 21:21:43,220 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,232 INFO  L225             Difference]: With dead ends: 143
[2025-04-28 21:21:43,233 INFO  L226             Difference]: Without dead ends: 140
[2025-04-28 21:21:43,235 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=24, Invalid=66, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:43,239 INFO  L437           NwaCegarLoop]: 150 mSDtfsCounter, 4 mSDsluCounter, 734 mSDsCounter, 0 mSdLazyCounter, 29 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 884 SdHoareTripleChecker+Invalid, 35 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 29 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,240 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 884 Invalid, 35 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 29 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:43,256 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 140 states.
[2025-04-28 21:21:43,290 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 140 to 140.
[2025-04-28 21:21:43,295 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 140 states, 65 states have (on average 1.123076923076923) internal successors, (73), 69 states have internal predecessors, (73), 41 states have call successors, (41), 32 states have call predecessors, (41), 33 states have return successors, (42), 39 states have call predecessors, (42), 41 states have call successors, (42)
[2025-04-28 21:21:43,306 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 140 states to 140 states and 156 transitions.
[2025-04-28 21:21:43,307 INFO  L79                 Accepts]: Start accepts. Automaton has 140 states and 156 transitions. Word has length 80
[2025-04-28 21:21:43,308 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,308 INFO  L485      AbstractCegarLoop]: Abstraction has 140 states and 156 transitions.
[2025-04-28 21:21:43,309 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 7.6) internal successors, (38), 7 states have internal predecessors, (38), 5 states have call successors, (20), 1 states have call predecessors, (20), 5 states have return successors, (20), 4 states have call predecessors, (20), 5 states have call successors, (20)
[2025-04-28 21:21:43,309 INFO  L278                IsEmpty]: Start isEmpty. Operand 140 states and 156 transitions.
[2025-04-28 21:21:43,313 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 113
[2025-04-28 21:21:43,316 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,317 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,317 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:43,317 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,318 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,318 INFO  L85        PathProgramCache]: Analyzing trace with hash -1678224159, now seen corresponding path program 1 times
[2025-04-28 21:21:43,318 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,318 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1128028086]
[2025-04-28 21:21:43,319 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,319 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,434 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 112 statements into 1 equivalence classes.
[2025-04-28 21:21:43,470 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 112 of 112 statements.
[2025-04-28 21:21:43,470 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,471 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,296 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:44,296 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,296 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1128028086]
[2025-04-28 21:21:44,296 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1128028086] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:44,296 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1356653355]
[2025-04-28 21:21:44,296 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,297 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,300 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,304 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:44,307 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,735 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 112 statements into 1 equivalence classes.
[2025-04-28 21:21:45,117 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 112 of 112 statements.
[2025-04-28 21:21:45,117 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,117 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,137 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2047 conjuncts, 29 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,156 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,177 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:46,178 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:46,178 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1356653355] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,178 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:46,178 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [16] imperfect sequences [5] total 19
[2025-04-28 21:21:46,181 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1416144599]
[2025-04-28 21:21:46,181 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,182 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:46,182 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,182 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:46,184 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=35, Invalid=307, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:46,185 INFO  L87              Difference]: Start difference. First operand 140 states and 156 transitions. Second operand  has 16 states, 10 states have (on average 5.3) internal successors, (53), 13 states have internal predecessors, (53), 8 states have call successors, (28), 1 states have call predecessors, (28), 10 states have return successors, (28), 10 states have call predecessors, (28), 8 states have call successors, (28)
[2025-04-28 21:21:46,706 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,706 INFO  L93              Difference]: Finished difference Result 152 states and 171 transitions.
[2025-04-28 21:21:46,707 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:21:46,707 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 10 states have (on average 5.3) internal successors, (53), 13 states have internal predecessors, (53), 8 states have call successors, (28), 1 states have call predecessors, (28), 10 states have return successors, (28), 10 states have call predecessors, (28), 8 states have call successors, (28) Word has length 112
[2025-04-28 21:21:46,708 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,714 INFO  L225             Difference]: With dead ends: 152
[2025-04-28 21:21:46,714 INFO  L226             Difference]: Without dead ends: 142
[2025-04-28 21:21:46,715 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 121 GetRequests, 99 SyntacticMatches, 0 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=59, Invalid=493, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:46,715 INFO  L437           NwaCegarLoop]: 144 mSDtfsCounter, 10 mSDsluCounter, 1975 mSDsCounter, 0 mSdLazyCounter, 164 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 2119 SdHoareTripleChecker+Invalid, 171 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 164 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,716 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 2119 Invalid, 171 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 164 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:46,717 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-04-28 21:21:46,733 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 142.
[2025-04-28 21:21:46,734 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 66 states have (on average 1.121212121212121) internal successors, (74), 70 states have internal predecessors, (74), 41 states have call successors, (41), 32 states have call predecessors, (41), 34 states have return successors, (44), 39 states have call predecessors, (44), 41 states have call successors, (44)
[2025-04-28 21:21:46,737 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 159 transitions.
[2025-04-28 21:21:46,739 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 159 transitions. Word has length 112
[2025-04-28 21:21:46,740 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,740 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 159 transitions.
[2025-04-28 21:21:46,740 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 10 states have (on average 5.3) internal successors, (53), 13 states have internal predecessors, (53), 8 states have call successors, (28), 1 states have call predecessors, (28), 10 states have return successors, (28), 10 states have call predecessors, (28), 8 states have call successors, (28)
[2025-04-28 21:21:46,740 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 159 transitions.
[2025-04-28 21:21:46,747 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 149
[2025-04-28 21:21:46,748 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,748 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:46,757 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:46,951 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,952 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,952 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,952 INFO  L85        PathProgramCache]: Analyzing trace with hash 854265086, now seen corresponding path program 1 times
[2025-04-28 21:21:46,952 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,953 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [706744090]
[2025-04-28 21:21:46,953 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,953 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,054 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 148 statements into 1 equivalence classes.
[2025-04-28 21:21:47,085 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 148 of 148 statements.
[2025-04-28 21:21:47,085 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,085 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,731 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:47,732 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,732 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [706744090]
[2025-04-28 21:21:47,732 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [706744090] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,732 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1792949140]
[2025-04-28 21:21:47,732 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,732 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,735 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,737 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:47,740 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,162 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 148 statements into 1 equivalence classes.
[2025-04-28 21:21:48,656 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 148 of 148 statements.
[2025-04-28 21:21:48,656 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,656 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,674 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2687 conjuncts, 67 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,685 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:51,134 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 6 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:51,134 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
