New files SmtBtype.ml(i) for module formerly in SmtAtom

1 files changed, 5 insertions, 5 deletions

diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 643ce8f..88d0769 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -81,7 +81,7 @@ let clear_all () =
 
 let import_all fsmt fproof =
   clear_all ();
-  let rt = Btype.create () in
+  let rt = SmtBtype.create () in
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in
@@ -109,16 +109,16 @@ let export out_channel rt ro l =
     let s = "Tindex_"^(string_of_int i) in
     VeritSyntax.add_btype s (Tindex t);
     Format.fprintf fmt "(declare-sort %s 0)@." s
-  ) (Btype.to_list rt);
+  ) (SmtBtype.to_list rt);
 
   List.iter (fun (i,cod,dom,op) ->
     let s = "op_"^(string_of_int i) in
     VeritSyntax.add_fun s op;
     Format.fprintf fmt "(declare-fun %s (" s;
     let is_first = ref true in
-    Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; Btype.to_smt fmt t) cod;
+    Array.iter (fun t -> if !is_first then is_first := false else Format.fprintf fmt " "; SmtBtype.to_smt fmt t) cod;
     Format.fprintf fmt ") ";
-    Btype.to_smt fmt dom;
+    SmtBtype.to_smt fmt dom;
     Format.fprintf fmt ")@."
   ) (Op.to_list ro);
 
@@ -150,7 +150,7 @@ let call_verit rt ro fl root =
 
 let tactic () =
   clear_all ();
-  let rt = Btype.create () in
+  let rt = SmtBtype.create () in
   let ro = Op.create () in
   let ra = VeritSyntax.ra in
   let rf = VeritSyntax.rf in