Add missing substitution case for NLS

TDacik · Nov 19, 2024 · c327204 · c327204
1 parent 383b824
commit c327204
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/SSL/SSL.ml b/src/SSL/SSL.ml
@@ -393,6 +393,9 @@ let rec substitute ?(bounded=[]) phi v term = match phi with
   | DLS (x, y, f, l) ->
       DLS (substitute ~bounded x v term, substitute ~bounded y v term,
            substitute ~bounded f v term, substitute ~bounded l v term)
+  | NLS (x, y, z) ->
+    NLS (substitute ~bounded x v term, substitute ~bounded y v term,
+         substitute ~bounded z v term)
   | And (psi1, psi2) -> And (substitute ~bounded psi1 v term, substitute ~bounded psi2 v term)
   | Or (psi1, psi2) -> Or (substitute ~bounded psi1 v term, substitute ~bounded psi2 v term)
   | Not psi -> Not (substitute ~bounded psi v term)