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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:24,275 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:24,345 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d6f3b2ee-e56d-41ff-98fd-3ffcebd3eec4/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:24,354 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:24,355 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:24,391 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:24,392 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:24,392 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:24,394 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:24,394 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:24,395 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:24,395 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:24,395 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:24,395 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:24,395 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:24,396 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:24,396 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:24,396 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:24,396 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:24,396 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:24,396 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:24,396 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:24,397 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:24,397 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:24,397 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:24,398 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:24,398 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:24,717 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:24,730 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:24,733 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:24,737 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:24,738 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:24,739 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d6f3b2ee-e56d-41ff-98fd-3ffcebd3eec4/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-140.smt2
[2025-04-28 21:21:24,741 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:24,746 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,353 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d6f3b2ee-e56d-41ff-98fd-3ffcebd3eec4/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-140.smt2
[2025-04-28 21:21:25,356 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:25,358 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:25,359 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:25,359 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:25,359 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:25,365 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,437 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,437 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:25,439 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:25,439 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:25,439 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:25,460 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,460 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,505 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,506 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,528 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,535 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,541 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,548 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,554 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,586 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:25,587 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:25,589 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:25,589 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:25,590 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,593 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:25,606 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:25,620 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,623 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,640 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:25,640 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:25,641 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:25,641 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure make_array.DLRunknown.CLN45 given in one single declaration
[2025-04-28 21:21:25,641 INFO  L130     BoogieDeclarations]: Found specification of procedure make_array.DLRunknown.CLN45
[2025-04-28 21:21:25,641 INFO  L138     BoogieDeclarations]: Found implementation of procedure make_array.DLRunknown.CLN45
[2025-04-28 21:21:25,641 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure kmpMatch.DLRunknown.CLN37 given in one single declaration
[2025-04-28 21:21:25,641 INFO  L130     BoogieDeclarations]: Found specification of procedure kmpMatch.DLRunknown.CLN37
[2025-04-28 21:21:25,641 INFO  L138     BoogieDeclarations]: Found implementation of procedure kmpMatch.DLRunknown.CLN37
[2025-04-28 21:21:25,641 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN24 given in one single declaration
[2025-04-28 21:21:25,641 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN24
[2025-04-28 21:21:25,641 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN24
[2025-04-28 21:21:25,641 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN34 given in one single declaration
[2025-04-28 21:21:25,641 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN34
[2025-04-28 21:21:25,641 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN34
[2025-04-28 21:21:25,642 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN32 given in one single declaration
[2025-04-28 21:21:25,642 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN32
[2025-04-28 21:21:25,642 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN32
[2025-04-28 21:21:25,642 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN31 given in one single declaration
[2025-04-28 21:21:25,642 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN31
[2025-04-28 21:21:25,642 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN31
[2025-04-28 21:21:25,642 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN22 given in one single declaration
[2025-04-28 21:21:25,642 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN22
[2025-04-28 21:21:25,642 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN22
[2025-04-28 21:21:25,642 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN14 given in one single declaration
[2025-04-28 21:21:25,642 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN14
[2025-04-28 21:21:25,642 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN14
[2025-04-28 21:21:25,642 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure kmpMatch.DLRunknown.CLN41 given in one single declaration
[2025-04-28 21:21:25,642 INFO  L130     BoogieDeclarations]: Found specification of procedure kmpMatch.DLRunknown.CLN41
[2025-04-28 21:21:25,643 INFO  L138     BoogieDeclarations]: Found implementation of procedure kmpMatch.DLRunknown.CLN41
[2025-04-28 21:21:25,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure make_array.DLRunknown.CLN46 given in one single declaration
[2025-04-28 21:21:25,643 INFO  L130     BoogieDeclarations]: Found specification of procedure make_array.DLRunknown.CLN46
[2025-04-28 21:21:25,643 INFO  L138     BoogieDeclarations]: Found implementation of procedure make_array.DLRunknown.CLN46
[2025-04-28 21:21:25,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN13 given in one single declaration
[2025-04-28 21:21:25,643 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN13
[2025-04-28 21:21:25,643 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN13
[2025-04-28 21:21:25,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN20 given in one single declaration
[2025-04-28 21:21:25,643 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN20
[2025-04-28 21:21:25,643 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN20
[2025-04-28 21:21:25,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure update.DLRunknown.CLN53 given in one single declaration
[2025-04-28 21:21:25,643 INFO  L130     BoogieDeclarations]: Found specification of procedure update.DLRunknown.CLN53
[2025-04-28 21:21:25,643 INFO  L138     BoogieDeclarations]: Found implementation of procedure update.DLRunknown.CLN53
[2025-04-28 21:21:25,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN8 given in one single declaration
[2025-04-28 21:21:25,644 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN8
[2025-04-28 21:21:25,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN8
[2025-04-28 21:21:25,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN4 given in one single declaration
[2025-04-28 21:21:25,644 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN4
[2025-04-28 21:21:25,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN4
[2025-04-28 21:21:25,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN3 given in one single declaration
[2025-04-28 21:21:25,644 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN3
[2025-04-28 21:21:25,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN3
[2025-04-28 21:21:25,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN7 given in one single declaration
[2025-04-28 21:21:25,644 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN7
[2025-04-28 21:21:25,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN1.DSHa.DLRunknown.CLN7
[2025-04-28 21:21:25,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure update.DLRunknown.CLN50 given in one single declaration
[2025-04-28 21:21:25,646 INFO  L130     BoogieDeclarations]: Found specification of procedure update.DLRunknown.CLN50
[2025-04-28 21:21:25,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure update.DLRunknown.CLN50
[2025-04-28 21:21:25,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure update.DLRunknown.CLN49 given in one single declaration
[2025-04-28 21:21:25,646 INFO  L130     BoogieDeclarations]: Found specification of procedure update.DLRunknown.CLN49
[2025-04-28 21:21:25,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure update.DLRunknown.CLN49
[2025-04-28 21:21:25,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure update.DLRunknown.CLN52 given in one single declaration
[2025-04-28 21:21:25,647 INFO  L130     BoogieDeclarations]: Found specification of procedure update.DLRunknown.CLN52
[2025-04-28 21:21:25,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure update.DLRunknown.CLN52
[2025-04-28 21:21:25,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure update.DLRunknown.CLN51 given in one single declaration
[2025-04-28 21:21:25,648 INFO  L130     BoogieDeclarations]: Found specification of procedure update.DLRunknown.CLN51
[2025-04-28 21:21:25,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure update.DLRunknown.CLN51
[2025-04-28 21:21:25,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN21 given in one single declaration
[2025-04-28 21:21:25,648 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN21
[2025-04-28 21:21:25,649 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN21
[2025-04-28 21:21:25,649 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN18 given in one single declaration
[2025-04-28 21:21:25,649 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN18
[2025-04-28 21:21:25,649 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN18
[2025-04-28 21:21:25,649 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN28 given in one single declaration
[2025-04-28 21:21:25,649 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN28
[2025-04-28 21:21:25,649 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN28
[2025-04-28 21:21:25,649 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN27 given in one single declaration
[2025-04-28 21:21:25,650 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN27
[2025-04-28 21:21:25,650 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN27
[2025-04-28 21:21:25,650 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN25 given in one single declaration
[2025-04-28 21:21:25,650 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN25
[2025-04-28 21:21:25,650 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN3.DSHloop.DLRunknown.CLN25
[2025-04-28 21:21:25,651 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure kmpMatch.DLRunknown.CLN38 given in one single declaration
[2025-04-28 21:21:25,651 INFO  L130     BoogieDeclarations]: Found specification of procedure kmpMatch.DLRunknown.CLN38
[2025-04-28 21:21:25,651 INFO  L138     BoogieDeclarations]: Found implementation of procedure kmpMatch.DLRunknown.CLN38
[2025-04-28 21:21:25,651 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure kmpMatch.DLRunknown.CLN39 given in one single declaration
[2025-04-28 21:21:25,651 INFO  L130     BoogieDeclarations]: Found specification of procedure kmpMatch.DLRunknown.CLN39
[2025-04-28 21:21:25,651 INFO  L138     BoogieDeclarations]: Found implementation of procedure kmpMatch.DLRunknown.CLN39
[2025-04-28 21:21:25,651 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN19 given in one single declaration
[2025-04-28 21:21:25,651 INFO  L130     BoogieDeclarations]: Found specification of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN19
[2025-04-28 21:21:25,651 INFO  L138     BoogieDeclarations]: Found implementation of procedure .DLRinnerFunc.CLN2.DSHloopShift.DLRunknown.CLN19
[2025-04-28 21:21:25,651 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure kmpMatch.DLRunknown.CLN40 given in one single declaration
[2025-04-28 21:21:25,652 INFO  L130     BoogieDeclarations]: Found specification of procedure kmpMatch.DLRunknown.CLN40
[2025-04-28 21:21:25,652 INFO  L138     BoogieDeclarations]: Found implementation of procedure kmpMatch.DLRunknown.CLN40
[2025-04-28 21:21:25,652 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:25,652 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:25,652 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:25,829 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:25,834 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:26,677 INFO  L?                        ?]: Removed 213 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:26,677 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:26,697 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:26,697 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:26,698 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,698 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:26,701 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:26,701 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:26,706 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:26,706 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,707 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@580af74 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,707 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,707 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@580af74 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,708 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,712 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:26,733 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:26,738 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 32 procedures, 296 locations, 695 edges, 32 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:26,805 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:26,832 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;@51aab3e1, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:26,833 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:26,841 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 296 states, 64 states have (on average 1.53125) internal successors, (98), 98 states have internal predecessors, (98), 199 states have call successors, (199), 31 states have call predecessors, (199), 31 states have return successors, (199), 167 states have call predecessors, (199), 199 states have call successors, (199)
[2025-04-28 21:21:26,861 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-04-28 21:21:26,861 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,862 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-04-28 21:21:26,863 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,869 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,870 INFO  L85        PathProgramCache]: Analyzing trace with hash 772523288, now seen corresponding path program 1 times
[2025-04-28 21:21:26,879 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,880 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [227109983]
[2025-04-28 21:21:26,880 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,881 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,915 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-04-28 21:21:26,918 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-04-28 21:21:26,918 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,918 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,958 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:26,959 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,959 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [227109983]
[2025-04-28 21:21:26,960 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [227109983] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:26,961 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:26,965 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-04-28 21:21:26,967 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [780915355]
[2025-04-28 21:21:26,968 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,973 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-04-28 21:21:26,973 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,012 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-04-28 21:21:27,013 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:27,017 INFO  L87              Difference]: Start difference. First operand  has 296 states, 64 states have (on average 1.53125) internal successors, (98), 98 states have internal predecessors, (98), 199 states have call successors, (199), 31 states have call predecessors, (199), 31 states have return successors, (199), 167 states have call predecessors, (199), 199 states have call successors, (199) Second operand  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:27,101 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,101 INFO  L93              Difference]: Finished difference Result 294 states and 493 transitions.
[2025-04-28 21:21:27,102 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-04-28 21:21:27,104 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1) Word has length 5
[2025-04-28 21:21:27,105 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,126 INFO  L225             Difference]: With dead ends: 294
[2025-04-28 21:21:27,128 INFO  L226             Difference]: Without dead ends: 294
[2025-04-28 21:21:27,130 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:27,133 INFO  L437           NwaCegarLoop]: 493 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 493 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,134 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 493 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:27,195 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 294 states.
[2025-04-28 21:21:27,272 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 294 to 294.
[2025-04-28 21:21:27,274 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 294 states, 63 states have (on average 1.507936507936508) internal successors, (95), 95 states have internal predecessors, (95), 199 states have call successors, (199), 31 states have call predecessors, (199), 31 states have return successors, (199), 167 states have call predecessors, (199), 199 states have call successors, (199)
[2025-04-28 21:21:27,314 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 294 states to 294 states and 493 transitions.
[2025-04-28 21:21:27,324 INFO  L79                 Accepts]: Start accepts. Automaton has 294 states and 493 transitions. Word has length 5
[2025-04-28 21:21:27,324 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,325 INFO  L485      AbstractCegarLoop]: Abstraction has 294 states and 493 transitions.
[2025-04-28 21:21:27,325 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:27,325 INFO  L278                IsEmpty]: Start isEmpty. Operand 294 states and 493 transitions.
[2025-04-28 21:21:27,332 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:27,332 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,333 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]
[2025-04-28 21:21:27,333 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:27,333 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,334 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,334 INFO  L85        PathProgramCache]: Analyzing trace with hash -572451056, now seen corresponding path program 1 times
[2025-04-28 21:21:27,334 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,341 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [726367616]
[2025-04-28 21:21:27,341 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,341 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,356 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:27,422 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:27,422 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,422 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,106 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:28,108 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,108 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [726367616]
[2025-04-28 21:21:28,108 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [726367616] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,108 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,108 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:28,108 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1754905250]
[2025-04-28 21:21:28,109 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,110 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:28,110 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,113 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:28,114 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:28,115 INFO  L87              Difference]: Start difference. First operand 294 states and 493 transitions. Second operand  has 9 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 9 states have internal predecessors, (13), 6 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:28,753 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,753 INFO  L93              Difference]: Finished difference Result 307 states and 540 transitions.
[2025-04-28 21:21:28,757 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:28,758 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 9 states have internal predecessors, (13), 6 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 6 states have call successors, (7) Word has length 29
[2025-04-28 21:21:28,758 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,768 INFO  L225             Difference]: With dead ends: 307
[2025-04-28 21:21:28,768 INFO  L226             Difference]: Without dead ends: 307
[2025-04-28 21:21:28,769 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:28,771 INFO  L437           NwaCegarLoop]: 457 mSDtfsCounter, 3 mSDsluCounter, 2693 mSDsCounter, 0 mSdLazyCounter, 297 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 3150 SdHoareTripleChecker+Invalid, 299 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 297 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,771 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 3150 Invalid, 299 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 297 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:28,772 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 307 states.
[2025-04-28 21:21:28,830 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 307 to 303.
[2025-04-28 21:21:28,831 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 303 states, 67 states have (on average 1.4776119402985075) internal successors, (99), 99 states have internal predecessors, (99), 200 states have call successors, (200), 31 states have call predecessors, (200), 35 states have return successors, (235), 172 states have call predecessors, (235), 200 states have call successors, (235)
[2025-04-28 21:21:28,840 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 303 states to 303 states and 534 transitions.
[2025-04-28 21:21:28,840 INFO  L79                 Accepts]: Start accepts. Automaton has 303 states and 534 transitions. Word has length 29
[2025-04-28 21:21:28,841 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,842 INFO  L485      AbstractCegarLoop]: Abstraction has 303 states and 534 transitions.
[2025-04-28 21:21:28,843 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 9 states have internal predecessors, (13), 6 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:28,844 INFO  L278                IsEmpty]: Start isEmpty. Operand 303 states and 534 transitions.
[2025-04-28 21:21:28,847 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:28,847 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,847 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]
[2025-04-28 21:21:28,847 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:28,847 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,848 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,848 INFO  L85        PathProgramCache]: Analyzing trace with hash -268069333, now seen corresponding path program 1 times
[2025-04-28 21:21:28,848 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,848 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [240504145]
[2025-04-28 21:21:28,851 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,851 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,865 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:28,881 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:28,884 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,884 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,171 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:29,172 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,172 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [240504145]
[2025-04-28 21:21:29,172 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [240504145] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,172 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:29,172 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:29,172 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [862060709]
[2025-04-28 21:21:29,172 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,172 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:29,173 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,174 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:29,174 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,174 INFO  L87              Difference]: Start difference. First operand 303 states and 534 transitions. Second operand  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 5 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:29,431 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,432 INFO  L93              Difference]: Finished difference Result 316 states and 558 transitions.
[2025-04-28 21:21:29,432 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:29,432 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 5 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7) Word has length 29
[2025-04-28 21:21:29,433 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,452 INFO  L225             Difference]: With dead ends: 316
[2025-04-28 21:21:29,452 INFO  L226             Difference]: Without dead ends: 316
[2025-04-28 21:21:29,453 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,458 INFO  L437           NwaCegarLoop]: 481 mSDtfsCounter, 2 mSDsluCounter, 2861 mSDsCounter, 0 mSdLazyCounter, 100 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 3342 SdHoareTripleChecker+Invalid, 102 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 100 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,458 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 3342 Invalid, 102 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 100 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:29,460 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 316 states.
[2025-04-28 21:21:29,509 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 316 to 312.
[2025-04-28 21:21:29,511 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 312 states, 70 states have (on average 1.457142857142857) internal successors, (102), 102 states have internal predecessors, (102), 203 states have call successors, (203), 31 states have call predecessors, (203), 38 states have return successors, (248), 178 states have call predecessors, (248), 203 states have call successors, (248)
[2025-04-28 21:21:29,520 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 312 states to 312 states and 553 transitions.
[2025-04-28 21:21:29,520 INFO  L79                 Accepts]: Start accepts. Automaton has 312 states and 553 transitions. Word has length 29
[2025-04-28 21:21:29,520 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,521 INFO  L485      AbstractCegarLoop]: Abstraction has 312 states and 553 transitions.
[2025-04-28 21:21:29,521 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 5 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:29,522 INFO  L278                IsEmpty]: Start isEmpty. Operand 312 states and 553 transitions.
[2025-04-28 21:21:29,532 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 102
[2025-04-28 21:21:29,532 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,532 INFO  L218           NwaCegarLoop]: trace histogram [8, 8, 4, 4, 4, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 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]
[2025-04-28 21:21:29,532 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:29,533 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,534 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,534 INFO  L85        PathProgramCache]: Analyzing trace with hash 297998557, now seen corresponding path program 1 times
[2025-04-28 21:21:29,534 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,535 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1657720650]
[2025-04-28 21:21:29,535 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,535 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,552 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 101 statements into 1 equivalence classes.
[2025-04-28 21:21:29,602 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 101 of 101 statements.
[2025-04-28 21:21:29,602 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,602 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,481 INFO  L134       CoverageAnalysis]: Checked inductivity of 148 backedges. 18 proven. 15 refuted. 0 times theorem prover too weak. 115 trivial. 0 not checked.
[2025-04-28 21:21:30,482 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,482 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1657720650]
[2025-04-28 21:21:30,482 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1657720650] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,482 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1267874833]
[2025-04-28 21:21:30,482 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,482 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,487 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,492 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:30,496 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:30,608 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 101 statements into 1 equivalence classes.
[2025-04-28 21:21:30,705 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 101 of 101 statements.
[2025-04-28 21:21:30,705 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,706 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,716 INFO  L256         TraceCheckSpWp]: Trace formula consists of 384 conjuncts, 31 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:30,733 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,157 INFO  L134       CoverageAnalysis]: Checked inductivity of 148 backedges. 18 proven. 15 refuted. 0 times theorem prover too weak. 115 trivial. 0 not checked.
[2025-04-28 21:21:31,157 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:36,475 INFO  L134       CoverageAnalysis]: Checked inductivity of 148 backedges. 18 proven. 15 refuted. 0 times theorem prover too weak. 115 trivial. 0 not checked.
[2025-04-28 21:21:36,475 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1267874833] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:36,476 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:36,476 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 15, 15] total 25
[2025-04-28 21:21:36,476 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1550913256]
[2025-04-28 21:21:36,476 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,477 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:21:36,477 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,478 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:21:36,478 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=537, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:36,478 INFO  L87              Difference]: Start difference. First operand 312 states and 553 transitions. Second operand  has 25 states, 16 states have (on average 2.25) internal successors, (36), 20 states have internal predecessors, (36), 19 states have call successors, (26), 1 states have call predecessors, (26), 16 states have return successors, (35), 21 states have call predecessors, (35), 19 states have call successors, (35)
[2025-04-28 21:21:39,818 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,818 INFO  L93              Difference]: Finished difference Result 373 states and 885 transitions.
[2025-04-28 21:21:39,819 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-04-28 21:21:39,819 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 16 states have (on average 2.25) internal successors, (36), 20 states have internal predecessors, (36), 19 states have call successors, (26), 1 states have call predecessors, (26), 16 states have return successors, (35), 21 states have call predecessors, (35), 19 states have call successors, (35) Word has length 101
[2025-04-28 21:21:39,820 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,829 INFO  L225             Difference]: With dead ends: 373
[2025-04-28 21:21:39,829 INFO  L226             Difference]: Without dead ends: 373
[2025-04-28 21:21:39,830 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 225 GetRequests, 194 SyntacticMatches, 3 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 80 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=96, Invalid=774, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:39,830 INFO  L437           NwaCegarLoop]: 442 mSDtfsCounter, 19 mSDsluCounter, 7584 mSDsCounter, 0 mSdLazyCounter, 3158 mSolverCounterSat, 43 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 64 SdHoareTripleChecker+Valid, 8026 SdHoareTripleChecker+Invalid, 3201 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 43 IncrementalHoareTripleChecker+Valid, 3158 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 3.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,831 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [64 Valid, 8026 Invalid, 3201 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [43 Valid, 3158 Invalid, 0 Unknown, 0 Unchecked, 3.0s Time]
[2025-04-28 21:21:39,832 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 373 states.
[2025-04-28 21:21:39,902 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 373 to 359.
[2025-04-28 21:21:39,903 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 359 states, 83 states have (on average 1.4457831325301205) internal successors, (120), 119 states have internal predecessors, (120), 227 states have call successors, (227), 34 states have call predecessors, (227), 48 states have return successors, (516), 205 states have call predecessors, (516), 227 states have call successors, (516)
[2025-04-28 21:21:39,911 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 359 states to 359 states and 863 transitions.
[2025-04-28 21:21:39,911 INFO  L79                 Accepts]: Start accepts. Automaton has 359 states and 863 transitions. Word has length 101
[2025-04-28 21:21:39,912 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,912 INFO  L485      AbstractCegarLoop]: Abstraction has 359 states and 863 transitions.
[2025-04-28 21:21:39,912 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 16 states have (on average 2.25) internal successors, (36), 20 states have internal predecessors, (36), 19 states have call successors, (26), 1 states have call predecessors, (26), 16 states have return successors, (35), 21 states have call predecessors, (35), 19 states have call successors, (35)
[2025-04-28 21:21:39,912 INFO  L278                IsEmpty]: Start isEmpty. Operand 359 states and 863 transitions.
[2025-04-28 21:21:39,917 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 102
[2025-04-28 21:21:39,918 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,918 INFO  L218           NwaCegarLoop]: trace histogram [8, 8, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,925 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:40,118 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:40,119 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,119 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,119 INFO  L85        PathProgramCache]: Analyzing trace with hash 272782550, now seen corresponding path program 1 times
[2025-04-28 21:21:40,120 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,120 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [590629107]
[2025-04-28 21:21:40,120 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,120 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,131 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 101 statements into 1 equivalence classes.
[2025-04-28 21:21:40,154 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 101 of 101 statements.
[2025-04-28 21:21:40,154 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,154 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,420 INFO  L134       CoverageAnalysis]: Checked inductivity of 107 backedges. 4 proven. 8 refuted. 0 times theorem prover too weak. 95 trivial. 0 not checked.
[2025-04-28 21:21:40,420 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,420 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [590629107]
[2025-04-28 21:21:40,421 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [590629107] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,421 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1127417620]
[2025-04-28 21:21:40,421 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,421 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,423 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,426 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:40,430 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,585 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 101 statements into 1 equivalence classes.
[2025-04-28 21:21:40,653 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 101 of 101 statements.
[2025-04-28 21:21:40,653 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,653 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,658 INFO  L256         TraceCheckSpWp]: Trace formula consists of 396 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,661 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,724 INFO  L134       CoverageAnalysis]: Checked inductivity of 107 backedges. 64 proven. 0 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:40,725 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:40,726 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1127417620] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,726 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:40,726 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [11] total 11
[2025-04-28 21:21:40,726 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [594385251]
[2025-04-28 21:21:40,727 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,727 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:40,727 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,728 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:40,729 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:40,729 INFO  L87              Difference]: Start difference. First operand 359 states and 863 transitions. Second operand  has 11 states, 10 states have (on average 3.6) internal successors, (36), 10 states have internal predecessors, (36), 7 states have call successors, (23), 2 states have call predecessors, (23), 10 states have return successors, (24), 10 states have call predecessors, (24), 7 states have call successors, (24)
[2025-04-28 21:21:41,217 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,218 INFO  L93              Difference]: Finished difference Result 369 states and 878 transitions.
[2025-04-28 21:21:41,218 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:41,219 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 10 states have (on average 3.6) internal successors, (36), 10 states have internal predecessors, (36), 7 states have call successors, (23), 2 states have call predecessors, (23), 10 states have return successors, (24), 10 states have call predecessors, (24), 7 states have call successors, (24) Word has length 101
[2025-04-28 21:21:41,219 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,229 INFO  L225             Difference]: With dead ends: 369
[2025-04-28 21:21:41,229 INFO  L226             Difference]: Without dead ends: 369
[2025-04-28 21:21:41,229 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 111 GetRequests, 102 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=91, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:41,230 INFO  L437           NwaCegarLoop]: 454 mSDtfsCounter, 1 mSDsluCounter, 4023 mSDsCounter, 0 mSdLazyCounter, 543 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 4477 SdHoareTripleChecker+Invalid, 545 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 543 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,230 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 4477 Invalid, 545 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 543 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:41,231 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 369 states.
[2025-04-28 21:21:41,286 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 369 to 367.
[2025-04-28 21:21:41,288 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 367 states, 86 states have (on average 1.430232558139535) internal successors, (123), 122 states have internal predecessors, (123), 229 states have call successors, (229), 34 states have call predecessors, (229), 51 states have return successors, (524), 210 states have call predecessors, (524), 229 states have call successors, (524)
[2025-04-28 21:21:41,295 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 367 states to 367 states and 876 transitions.
[2025-04-28 21:21:41,295 INFO  L79                 Accepts]: Start accepts. Automaton has 367 states and 876 transitions. Word has length 101
[2025-04-28 21:21:41,296 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,296 INFO  L485      AbstractCegarLoop]: Abstraction has 367 states and 876 transitions.
[2025-04-28 21:21:41,296 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 10 states have (on average 3.6) internal successors, (36), 10 states have internal predecessors, (36), 7 states have call successors, (23), 2 states have call predecessors, (23), 10 states have return successors, (24), 10 states have call predecessors, (24), 7 states have call successors, (24)
[2025-04-28 21:21:41,296 INFO  L278                IsEmpty]: Start isEmpty. Operand 367 states and 876 transitions.
[2025-04-28 21:21:41,304 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 170
[2025-04-28 21:21:41,304 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,304 INFO  L218           NwaCegarLoop]: trace histogram [14, 14, 7, 7, 7, 7, 6, 6, 6, 6, 4, 4, 4, 4, 4, 4, 3, 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]
[2025-04-28 21:21:41,310 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:41,507 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,508 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,508 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,508 INFO  L85        PathProgramCache]: Analyzing trace with hash 264474132, now seen corresponding path program 1 times
[2025-04-28 21:21:41,508 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,508 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1032147689]
[2025-04-28 21:21:41,509 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,509 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,523 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 169 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 169 of 169 statements.
[2025-04-28 21:21:41,561 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,561 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,788 INFO  L134       CoverageAnalysis]: Checked inductivity of 472 backedges. 4 proven. 32 refuted. 0 times theorem prover too weak. 436 trivial. 0 not checked.
[2025-04-28 21:21:41,789 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,789 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1032147689]
[2025-04-28 21:21:41,789 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1032147689] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,789 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1138319688]
[2025-04-28 21:21:41,789 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,789 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,792 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,794 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:41,797 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,931 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 169 statements into 1 equivalence classes.
[2025-04-28 21:21:42,061 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 169 of 169 statements.
[2025-04-28 21:21:42,062 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,062 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,065 INFO  L256         TraceCheckSpWp]: Trace formula consists of 667 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,070 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,143 INFO  L134       CoverageAnalysis]: Checked inductivity of 472 backedges. 43 proven. 32 refuted. 0 times theorem prover too weak. 397 trivial. 0 not checked.
[2025-04-28 21:21:42,146 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,584 INFO  L134       CoverageAnalysis]: Checked inductivity of 472 backedges. 4 proven. 32 refuted. 0 times theorem prover too weak. 436 trivial. 0 not checked.
[2025-04-28 21:21:43,584 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1138319688] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,584 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,584 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 9
[2025-04-28 21:21:43,585 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [255137464]
[2025-04-28 21:21:43,585 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,585 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:43,585 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,586 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:43,586 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:43,586 INFO  L87              Difference]: Start difference. First operand 367 states and 876 transitions. Second operand  has 9 states, 6 states have (on average 5.0) internal successors, (30), 9 states have internal predecessors, (30), 8 states have call successors, (23), 2 states have call predecessors, (23), 6 states have return successors, (25), 6 states have call predecessors, (25), 8 states have call successors, (25)
[2025-04-28 21:21:44,479 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,479 INFO  L93              Difference]: Finished difference Result 377 states and 920 transitions.
[2025-04-28 21:21:44,480 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:44,480 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 5.0) internal successors, (30), 9 states have internal predecessors, (30), 8 states have call successors, (23), 2 states have call predecessors, (23), 6 states have return successors, (25), 6 states have call predecessors, (25), 8 states have call successors, (25) Word has length 169
[2025-04-28 21:21:44,481 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,491 INFO  L225             Difference]: With dead ends: 377
[2025-04-28 21:21:44,491 INFO  L226             Difference]: Without dead ends: 377
[2025-04-28 21:21:44,491 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 346 GetRequests, 333 SyntacticMatches, 5 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=22, Invalid=68, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:44,492 INFO  L437           NwaCegarLoop]: 441 mSDtfsCounter, 11 mSDsluCounter, 2042 mSDsCounter, 0 mSdLazyCounter, 837 mSolverCounterSat, 56 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 54 SdHoareTripleChecker+Valid, 2483 SdHoareTripleChecker+Invalid, 893 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 56 IncrementalHoareTripleChecker+Valid, 837 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,493 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [54 Valid, 2483 Invalid, 893 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [56 Valid, 837 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:44,495 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 377 states.
[2025-04-28 21:21:44,575 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 377 to 371.
[2025-04-28 21:21:44,576 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 371 states, 87 states have (on average 1.4252873563218391) internal successors, (124), 123 states have internal predecessors, (124), 231 states have call successors, (231), 34 states have call predecessors, (231), 52 states have return successors, (541), 213 states have call predecessors, (541), 231 states have call successors, (541)
[2025-04-28 21:21:44,584 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 371 states to 371 states and 896 transitions.
[2025-04-28 21:21:44,584 INFO  L79                 Accepts]: Start accepts. Automaton has 371 states and 896 transitions. Word has length 169
[2025-04-28 21:21:44,585 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,585 INFO  L485      AbstractCegarLoop]: Abstraction has 371 states and 896 transitions.
[2025-04-28 21:21:44,585 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 5.0) internal successors, (30), 9 states have internal predecessors, (30), 8 states have call successors, (23), 2 states have call predecessors, (23), 6 states have return successors, (25), 6 states have call predecessors, (25), 8 states have call successors, (25)
[2025-04-28 21:21:44,589 INFO  L278                IsEmpty]: Start isEmpty. Operand 371 states and 896 transitions.
[2025-04-28 21:21:44,599 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 170
[2025-04-28 21:21:44,600 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,600 INFO  L218           NwaCegarLoop]: trace histogram [14, 14, 7, 7, 7, 7, 6, 6, 6, 6, 4, 4, 4, 4, 4, 4, 3, 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]
[2025-04-28 21:21:44,607 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:44,804 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,805 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,805 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,806 INFO  L85        PathProgramCache]: Analyzing trace with hash 1162691628, now seen corresponding path program 1 times
[2025-04-28 21:21:44,806 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,806 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2050570862]
[2025-04-28 21:21:44,806 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,806 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,819 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 169 statements into 1 equivalence classes.
[2025-04-28 21:21:44,840 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 169 of 169 statements.
[2025-04-28 21:21:44,840 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,840 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,044 INFO  L134       CoverageAnalysis]: Checked inductivity of 472 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 468 trivial. 0 not checked.
[2025-04-28 21:21:45,044 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,045 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2050570862]
[2025-04-28 21:21:45,045 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2050570862] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,045 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,045 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:45,045 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1767971529]
[2025-04-28 21:21:45,046 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,046 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:45,046 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,047 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:45,047 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:45,047 INFO  L87              Difference]: Start difference. First operand 371 states and 896 transitions. Second operand  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-04-28 21:21:45,142 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,142 INFO  L93              Difference]: Finished difference Result 375 states and 909 transitions.
[2025-04-28 21:21:45,142 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:45,143 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18) Word has length 169
[2025-04-28 21:21:45,143 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,153 INFO  L225             Difference]: With dead ends: 375
[2025-04-28 21:21:45,153 INFO  L226             Difference]: Without dead ends: 375
[2025-04-28 21:21:45,153 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:45,154 INFO  L437           NwaCegarLoop]: 490 mSDtfsCounter, 1 mSDsluCounter, 948 mSDsCounter, 0 mSdLazyCounter, 45 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1438 SdHoareTripleChecker+Invalid, 46 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 45 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,154 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1438 Invalid, 46 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 45 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,155 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 375 states.
[2025-04-28 21:21:45,222 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 375 to 371.
[2025-04-28 21:21:45,223 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 371 states, 87 states have (on average 1.4252873563218391) internal successors, (124), 123 states have internal predecessors, (124), 231 states have call successors, (231), 34 states have call predecessors, (231), 52 states have return successors, (541), 213 states have call predecessors, (541), 231 states have call successors, (541)
[2025-04-28 21:21:45,229 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 371 states to 371 states and 896 transitions.
[2025-04-28 21:21:45,229 INFO  L79                 Accepts]: Start accepts. Automaton has 371 states and 896 transitions. Word has length 169
[2025-04-28 21:21:45,230 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,230 INFO  L485      AbstractCegarLoop]: Abstraction has 371 states and 896 transitions.
[2025-04-28 21:21:45,230 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.666666666666667) internal successors, (23), 4 states have internal predecessors, (23), 4 states have call successors, (18), 1 states have call predecessors, (18), 3 states have return successors, (18), 3 states have call predecessors, (18), 4 states have call successors, (18)
[2025-04-28 21:21:45,230 INFO  L278                IsEmpty]: Start isEmpty. Operand 371 states and 896 transitions.
[2025-04-28 21:21:45,236 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 102
[2025-04-28 21:21:45,236 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,237 INFO  L218           NwaCegarLoop]: trace histogram [8, 8, 4, 4, 4, 4, 3, 3, 3, 3, 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]
[2025-04-28 21:21:45,237 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:45,237 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,237 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,237 INFO  L85        PathProgramCache]: Analyzing trace with hash -1183956623, now seen corresponding path program 1 times
[2025-04-28 21:21:45,237 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,238 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1279691907]
[2025-04-28 21:21:45,238 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,238 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,246 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 101 statements into 1 equivalence classes.
[2025-04-28 21:21:45,260 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 101 of 101 statements.
[2025-04-28 21:21:45,260 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,260 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,528 INFO  L134       CoverageAnalysis]: Checked inductivity of 128 backedges. 11 proven. 0 refuted. 0 times theorem prover too weak. 117 trivial. 0 not checked.
[2025-04-28 21:21:45,529 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,529 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1279691907]
[2025-04-28 21:21:45,529 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1279691907] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,529 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,529 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:45,529 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [548487110]
[2025-04-28 21:21:45,530 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,530 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:45,530 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,531 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:45,531 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:45,531 INFO  L87              Difference]: Start difference. First operand 371 states and 896 transitions. Second operand  has 8 states, 6 states have (on average 4.5) internal successors, (27), 8 states have internal predecessors, (27), 5 states have call successors, (19), 1 states have call predecessors, (19), 6 states have return successors, (19), 6 states have call predecessors, (19), 5 states have call successors, (19)
[2025-04-28 21:21:45,678 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,678 INFO  L93              Difference]: Finished difference Result 394 states and 949 transitions.
[2025-04-28 21:21:45,678 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:45,678 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 4.5) internal successors, (27), 8 states have internal predecessors, (27), 5 states have call successors, (19), 1 states have call predecessors, (19), 6 states have return successors, (19), 6 states have call predecessors, (19), 5 states have call successors, (19) Word has length 101
[2025-04-28 21:21:45,679 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,687 INFO  L225             Difference]: With dead ends: 394
[2025-04-28 21:21:45,687 INFO  L226             Difference]: Without dead ends: 394
[2025-04-28 21:21:45,687 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:45,688 INFO  L437           NwaCegarLoop]: 489 mSDtfsCounter, 4 mSDsluCounter, 2406 mSDsCounter, 0 mSdLazyCounter, 124 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 2895 SdHoareTripleChecker+Invalid, 127 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 124 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,688 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 2895 Invalid, 127 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 124 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,689 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 394 states.
[2025-04-28 21:21:45,752 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 394 to 388.
[2025-04-28 21:21:45,753 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 388 states, 91 states have (on average 1.4395604395604396) internal successors, (131), 128 states have internal predecessors, (131), 241 states have call successors, (241), 35 states have call predecessors, (241), 55 states have return successors, (569), 224 states have call predecessors, (569), 241 states have call successors, (569)
[2025-04-28 21:21:45,759 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 388 states to 388 states and 941 transitions.
[2025-04-28 21:21:45,760 INFO  L79                 Accepts]: Start accepts. Automaton has 388 states and 941 transitions. Word has length 101
[2025-04-28 21:21:45,760 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,760 INFO  L485      AbstractCegarLoop]: Abstraction has 388 states and 941 transitions.
[2025-04-28 21:21:45,760 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 4.5) internal successors, (27), 8 states have internal predecessors, (27), 5 states have call successors, (19), 1 states have call predecessors, (19), 6 states have return successors, (19), 6 states have call predecessors, (19), 5 states have call successors, (19)
[2025-04-28 21:21:45,760 INFO  L278                IsEmpty]: Start isEmpty. Operand 388 states and 941 transitions.
[2025-04-28 21:21:45,768 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 178
[2025-04-28 21:21:45,768 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,769 INFO  L218           NwaCegarLoop]: trace histogram [14, 14, 8, 7, 7, 7, 7, 7, 7, 7, 5, 5, 5, 5, 5, 5, 3, 3, 3, 3, 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]
[2025-04-28 21:21:45,769 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:45,769 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,769 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,769 INFO  L85        PathProgramCache]: Analyzing trace with hash 1226870476, now seen corresponding path program 1 times
[2025-04-28 21:21:45,770 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,770 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [415942493]
[2025-04-28 21:21:45,770 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,770 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,782 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 177 statements into 1 equivalence classes.
[2025-04-28 21:21:45,806 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 177 of 177 statements.
[2025-04-28 21:21:45,806 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,806 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,972 INFO  L134       CoverageAnalysis]: Checked inductivity of 539 backedges. 42 proven. 32 refuted. 0 times theorem prover too weak. 465 trivial. 0 not checked.
[2025-04-28 21:21:45,972 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,972 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [415942493]
[2025-04-28 21:21:45,972 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [415942493] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,972 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [641525200]
[2025-04-28 21:21:45,973 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,973 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,975 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,977 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:45,980 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,120 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 177 statements into 1 equivalence classes.
[2025-04-28 21:21:46,213 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 177 of 177 statements.
[2025-04-28 21:21:46,213 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,213 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,218 INFO  L256         TraceCheckSpWp]: Trace formula consists of 691 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,224 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,307 INFO  L134       CoverageAnalysis]: Checked inductivity of 539 backedges. 96 proven. 32 refuted. 0 times theorem prover too weak. 411 trivial. 0 not checked.
[2025-04-28 21:21:46,310 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,843 INFO  L134       CoverageAnalysis]: Checked inductivity of 539 backedges. 57 proven. 32 refuted. 0 times theorem prover too weak. 450 trivial. 0 not checked.
[2025-04-28 21:21:47,843 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [641525200] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,843 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,844 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 8, 8] total 10
[2025-04-28 21:21:47,844 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [767470649]
[2025-04-28 21:21:47,844 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,844 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:47,844 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,845 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:47,845 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=70, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:47,845 INFO  L87              Difference]: Start difference. First operand 388 states and 941 transitions. Second operand  has 10 states, 6 states have (on average 5.666666666666667) internal successors, (34), 9 states have internal predecessors, (34), 9 states have call successors, (26), 2 states have call predecessors, (26), 6 states have return successors, (31), 7 states have call predecessors, (31), 9 states have call successors, (31)
[2025-04-28 21:21:49,179 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,179 INFO  L93              Difference]: Finished difference Result 403 states and 1106 transitions.
[2025-04-28 21:21:49,179 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:49,179 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 5.666666666666667) internal successors, (34), 9 states have internal predecessors, (34), 9 states have call successors, (26), 2 states have call predecessors, (26), 6 states have return successors, (31), 7 states have call predecessors, (31), 9 states have call successors, (31) Word has length 177
[2025-04-28 21:21:49,180 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,190 INFO  L225             Difference]: With dead ends: 403
[2025-04-28 21:21:49,190 INFO  L226             Difference]: Without dead ends: 403
[2025-04-28 21:21:49,190 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 374 GetRequests, 353 SyntacticMatches, 5 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 24 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=75, Invalid=231, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:49,192 INFO  L437           NwaCegarLoop]: 506 mSDtfsCounter, 21 mSDsluCounter, 2332 mSDsCounter, 0 mSdLazyCounter, 1191 mSolverCounterSat, 118 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 42 SdHoareTripleChecker+Valid, 2838 SdHoareTripleChecker+Invalid, 1309 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 118 IncrementalHoareTripleChecker+Valid, 1191 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,193 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [42 Valid, 2838 Invalid, 1309 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [118 Valid, 1191 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-04-28 21:21:49,194 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 403 states.
[2025-04-28 21:21:49,262 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 403 to 388.
[2025-04-28 21:21:49,264 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 388 states, 91 states have (on average 1.4395604395604396) internal successors, (131), 128 states have internal predecessors, (131), 241 states have call successors, (241), 35 states have call predecessors, (241), 55 states have return successors, (567), 224 states have call predecessors, (567), 241 states have call successors, (567)
[2025-04-28 21:21:49,270 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 388 states to 388 states and 939 transitions.
[2025-04-28 21:21:49,270 INFO  L79                 Accepts]: Start accepts. Automaton has 388 states and 939 transitions. Word has length 177
[2025-04-28 21:21:49,272 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,272 INFO  L485      AbstractCegarLoop]: Abstraction has 388 states and 939 transitions.
[2025-04-28 21:21:49,272 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 5.666666666666667) internal successors, (34), 9 states have internal predecessors, (34), 9 states have call successors, (26), 2 states have call predecessors, (26), 6 states have return successors, (31), 7 states have call predecessors, (31), 9 states have call successors, (31)
[2025-04-28 21:21:49,273 INFO  L278                IsEmpty]: Start isEmpty. Operand 388 states and 939 transitions.
[2025-04-28 21:21:49,285 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 398
[2025-04-28 21:21:49,286 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,286 INFO  L218           NwaCegarLoop]: trace histogram [33, 33, 17, 17, 17, 17, 15, 14, 14, 14, 10, 10, 10, 10, 10, 10, 6, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 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]
[2025-04-28 21:21:49,294 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:49,486 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:21:49,487 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,487 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,487 INFO  L85        PathProgramCache]: Analyzing trace with hash 993099843, now seen corresponding path program 1 times
[2025-04-28 21:21:49,487 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,487 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [942812415]
[2025-04-28 21:21:49,487 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,487 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,511 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 397 statements into 1 equivalence classes.
[2025-04-28 21:21:49,543 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 397 of 397 statements.
[2025-04-28 21:21:49,544 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,544 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,776 INFO  L134       CoverageAnalysis]: Checked inductivity of 2967 backedges. 40 proven. 18 refuted. 0 times theorem prover too weak. 2909 trivial. 0 not checked.
[2025-04-28 21:21:49,778 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,778 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [942812415]
[2025-04-28 21:21:49,778 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [942812415] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:49,778 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [202918579]
[2025-04-28 21:21:49,778 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,778 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,781 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,784 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:49,788 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,006 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 397 statements into 1 equivalence classes.
[2025-04-28 21:21:50,222 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 397 of 397 statements.
[2025-04-28 21:21:50,222 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,223 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,230 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1561 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,237 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,345 INFO  L134       CoverageAnalysis]: Checked inductivity of 2967 backedges. 111 proven. 89 refuted. 0 times theorem prover too weak. 2767 trivial. 0 not checked.
[2025-04-28 21:21:50,345 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
