From 2743d631241c2a5d2e3d28fac64bb66e8c36e07b Mon Sep 17 00:00:00 2001
From: gtrepta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 22 Jan 2024 06:49:00 -0600
Subject: [PATCH] Fix missing case in semantics for string replace function
 (#3910)

fixes: #3896

---------

Co-authored-by: rv-jenkins <admin@runtimeverification.com>
---
 k-distribution/include/kframework/builtin/domains.md | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md
index 85d55b4ff99..474ea6f8b1e 100644
--- a/k-distribution/include/kframework/builtin/domains.md
+++ b/k-distribution/include/kframework/builtin/domains.md
@@ -1881,11 +1881,15 @@ of the above operations in K.
         requires findString(Source, ToReplace, 0) <Int 0
 
 
+  // Note that the replace function is undefined when Count < 0. This allows different backends to
+  // implement their own behavior without contradicting these semantics. For instance, a symbolic
+  // backend can return #Bottom for that case, while a concrete backend can throw an exception.
   rule replace(Source:String, ToReplace:String, Replacement:String, Count:Int) =>
        substrString(Source, 0, findString(Source, ToReplace, 0)) +String Replacement +String
        replace(substrString(Source, findString(Source, ToReplace, 0) +Int lengthString(ToReplace), lengthString(Source)), ToReplace, Replacement, Count -Int 1)
-        requires Count >Int 0
-  rule replace(Source:String, _, _, 0) => Source
+        requires Count >Int 0 andBool findString(Source, ToReplace, 0) >=Int 0
+  rule replace(Source:String, _, _, Count) => Source
+        requires Count >=Int 0 [owise]
   rule replaceAll(Source:String, ToReplace:String, Replacement:String) => replace(Source, ToReplace, Replacement, countAllOccurrences(Source, ToReplace))
 
 endmodule