From f95a2cc0ee8dac7bc4232406afdd82317c1eaf73 Mon Sep 17 00:00:00 2001
From: Albin Coquereau <6535385+ACoquereau@users.noreply.github.com>
Date: Tue, 9 Feb 2021 15:05:09 +0100
Subject: [PATCH] Fix declare-fun command in models

---
 src/lib/frontend/models.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index 05da3d4b5..c0a80e363 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -422,7 +422,7 @@ module Why3CounterExample = struct
           Printer.print_fmt ~flushed:false fmt "(declare-const %s %s)@ "
             name ty
         | l ->
-          Printer.print_fmt ~flushed:false fmt "(declate-fun %s (%s) %s)@ "
+          Printer.print_fmt ~flushed:false fmt "(declare-fun %s (%s) %s)@ "
             name
             (String.concat " " l)
             ty