Fix declare-fun command in models

OCamlPro · Mar 23, 2021 · f95a2cc · f95a2cc
1 parent 40d40cf
commit f95a2cc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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