From b6a77f65676ae0b9e858fd48959977830fc5dee7 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 20 Oct 2020 11:41:17 -0700
Subject: [PATCH] [sledge] Refactor nonstdlib to avoid opening Core

Summary:
The treatment of comparison and exceptions in Core/Core_kernel/Base
makes them questionable as the default. This diff changes nonstdlib so
that Core is no longer opened in the global namespace, and makes a few
changes to handle the resulting minor API changes. This leads to a
lighter-touch nonstdlib, which makes a few definitions of its own, and
selects and extends modules from several libraries, including base,
core_kernel, containers, iter.

Reviewed By: jvillard

Differential Revision: D24306090

fbshipit-source-id: 42c91bd1b
---
 sledge/cli/domain_itv.ml          |   4 +-
 sledge/cli/frontend.ml            |  13 +-
 sledge/cli/sledge_buck.ml         |   1 +
 sledge/cli/sledge_buck.mli        |   2 +
 sledge/cli/sledge_cli.ml          |  10 +-
 sledge/cli/smtlib.ml              |   2 +-
 sledge/nonstdlib/NS.ml            | 219 +++-------------------------
 sledge/nonstdlib/NS.mli           | 234 ++++++++++++++++++------------
 sledge/nonstdlib/NS0.ml           | 196 ++++++++++++++++++++++---
 sledge/nonstdlib/array.ml         |  24 +++
 sledge/nonstdlib/array.mli        |  18 +++
 sledge/nonstdlib/float.ml         |  18 +++
 sledge/nonstdlib/float.mli        |  17 +++
 sledge/nonstdlib/iArray.ml        |  20 +--
 sledge/nonstdlib/iArray.mli       |  11 +-
 sledge/nonstdlib/int.ml           |  12 ++
 sledge/nonstdlib/int.mli          |  12 ++
 sledge/nonstdlib/list.ml          |  24 +--
 sledge/nonstdlib/list.mli         |   4 +-
 sledge/nonstdlib/map.ml           |   2 +-
 sledge/nonstdlib/map_intf.ml      |   4 +-
 sledge/nonstdlib/multiset.ml      |   2 +-
 sledge/nonstdlib/multiset_intf.ml |   2 +-
 sledge/nonstdlib/option.ml        |   2 +-
 sledge/nonstdlib/option.mli       |   2 +-
 sledge/nonstdlib/q_ext.ml         |  25 ++++
 sledge/nonstdlib/q_ext.mli        |  21 +++
 sledge/nonstdlib/set.ml           |   2 +-
 sledge/nonstdlib/set_intf.ml      |   2 +-
 sledge/nonstdlib/sign.ml          |  15 ++
 sledge/nonstdlib/sign.mli         |  13 ++
 sledge/nonstdlib/string.ml        |  11 ++
 sledge/nonstdlib/string.mli       |  11 ++
 sledge/nonstdlib/sys.ml           |  10 ++
 sledge/nonstdlib/sys.mli          |  12 ++
 sledge/nonstdlib/timer.ml         |   2 +-
 sledge/nonstdlib/z_ext.ml         |  23 +++
 sledge/nonstdlib/z_ext.mli        |  24 +++
 sledge/report/sledge_report.ml    |   3 +-
 sledge/src/control.ml             |   4 +-
 sledge/src/domain_intf.ml         |   2 +-
 sledge/src/domain_sh.ml           |   2 +-
 sledge/src/domain_used_globals.ml |   2 +-
 sledge/src/llair/llair.ml         |   8 +-
 sledge/src/llair_to_Fol.ml        |   2 +-
 sledge/src/report.ml              |   2 +-
 sledge/src/report.mli             |   4 +-
 sledge/src/ses/equality.ml        |  22 +--
 sledge/src/ses/term.ml            |  28 ++--
 sledge/src/sh.ml                  |   2 +-
 sledge/src/test/equality_test.ml  |   2 +-
 sledge/src/test/fol_test.ml       |   2 +-
 sledge/src/test/sh_test.ml        |   2 +-
 sledge/src/test/solver_test.ml    |   4 +-
 54 files changed, 709 insertions(+), 408 deletions(-)
 create mode 100644 sledge/nonstdlib/array.ml
 create mode 100644 sledge/nonstdlib/array.mli
 create mode 100644 sledge/nonstdlib/float.ml
 create mode 100644 sledge/nonstdlib/float.mli
 create mode 100644 sledge/nonstdlib/int.ml
 create mode 100644 sledge/nonstdlib/int.mli
 create mode 100644 sledge/nonstdlib/q_ext.ml
 create mode 100644 sledge/nonstdlib/q_ext.mli
 create mode 100644 sledge/nonstdlib/sign.ml
 create mode 100644 sledge/nonstdlib/sign.mli
 create mode 100644 sledge/nonstdlib/string.ml
 create mode 100644 sledge/nonstdlib/string.mli
 create mode 100644 sledge/nonstdlib/sys.ml
 create mode 100644 sledge/nonstdlib/sys.mli
 create mode 100644 sledge/nonstdlib/z_ext.ml
 create mode 100644 sledge/nonstdlib/z_ext.mli

diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 91f72a39b..d01b0844d 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -46,7 +46,7 @@ let pp fs =
   in
   bindings >> Array.pp "@," (pp_pair Var.print Interval.print) fs
 
-let report_fmt_thunk = Fn.flip pp
+let report_fmt_thunk = Fun.flip pp
 let init _gs = Abstract1.top (Lazy.force man) (Environment.make [||] [||])
 let apron_var_of_name = (fun nm -> "%" ^ nm) >> Apron.Var.of_string
 let apron_var_of_reg = Llair.Reg.name >> apron_var_of_name
@@ -68,7 +68,7 @@ let rec apron_texpr_of_llair_exp exp q =
   | Reg {name} -> Some (Texpr1.Var (apron_var_of_name name))
   | Integer {data} -> Some (Texpr1.Cst (Coeff.s_of_int (Z.to_int data)))
   | Float {data} -> (
-    match Float.of_string data with
+    match Float.of_string_exn data with
     | f -> Some (Texpr1.Cst (Coeff.s_of_float f))
     | exception Invalid_argument _ -> None )
   | Ap1 (Signed {bits}, _, _) ->
diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index 447b2fbf1..311b962d3 100644
--- a/sledge/cli/frontend.ml
+++ b/sledge/cli/frontend.ml
@@ -206,7 +206,7 @@ let ptr_siz : x -> int =
 let size_of, bit_size_of =
   let size_to_int size_of x llt =
     if Llvm.type_is_sized llt then
-      match Int64.to_int (size_of llt x.lldatalayout) with
+      match Int64.unsigned_to_int (size_of llt x.lldatalayout) with
       | Some n -> n
       | None -> fail "type size too large: %a" pp_lltype llt ()
     else fail "types with undetermined size: %a" pp_lltype llt ()
@@ -460,7 +460,7 @@ and xlate_value ?(inline = false) stk :
         ([], Exp.label ~parent ~name)
     | UndefValue ->
         let typ = xlate_type x (Llvm.type_of llv) in
-        let name = sprintf "undef_%i" !undef_count in
+        let name = Printf.sprintf "undef_%i" !undef_count in
         let loc = Loc.none in
         let reg = Reg.program typ name in
         let msg = Llvm.string_of_llvalue llv in
@@ -674,7 +674,7 @@ and xlate_opcode stk :
             | Struct ->
                 let fld =
                   match
-                    Option.bind ~f:Int64.to_int
+                    Option.bind ~f:Int64.unsigned_to_int
                       (Llvm.int64_of_const (Llvm.operand llv i))
                   with
                   | Some n -> n
@@ -1486,7 +1486,12 @@ let link_in : Llvm.llcontext -> Llvm.lllinker -> string -> unit =
 let check_datalayout llcontext lldatalayout =
   let check_size llt typ =
     let llsiz =
-      Int64.to_int_exn (Llvm_target.DataLayout.abi_size llt lldatalayout)
+      match
+        Int64.unsigned_to_int
+          (Llvm_target.DataLayout.abi_size llt lldatalayout)
+      with
+      | Some n -> n
+      | None -> fail "type size too large: %a" pp_lltype llt ()
     in
     let siz = Typ.size_of typ in
     if llsiz != siz then
diff --git a/sledge/cli/sledge_buck.ml b/sledge/cli/sledge_buck.ml
index 805b241b0..c27ab1111 100644
--- a/sledge/cli/sledge_buck.ml
+++ b/sledge/cli/sledge_buck.ml
@@ -182,6 +182,7 @@ let llvm_link_opt ~fuzzer ~bitcode_output modules =
 
 (** command line interface *)
 
+module Command = Core.Command
 open Command.Let_syntax
 
 let ( |*> ) a' f' = a' |> Command.Param.apply f'
diff --git a/sledge/cli/sledge_buck.mli b/sledge/cli/sledge_buck.mli
index 1419d20dd..e44ff0ace 100644
--- a/sledge/cli/sledge_buck.mli
+++ b/sledge/cli/sledge_buck.mli
@@ -5,6 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Core
+
 val main :
      command:Report.status Command.basic_command
   -> analyze:(string list -> unit -> Report.status) Command.Param.t
diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index b730460bb..55b422385 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/sledge/cli/sledge_cli.ml
@@ -7,8 +7,7 @@
 
 (** SLEdge command line interface *)
 
-let () = Backtrace.Exn.set_recording Version.debug
-
+module Command = Core.Command
 open Command.Let_syntax
 
 type 'a param = 'a Command.Param.t
@@ -32,7 +31,7 @@ let command ~summary ?readme param =
     let%map_open config =
       flag "trace" ~doc:"<spec> enable debug tracing"
         (optional_with_default Trace.none
-           (Arg_type.create (fun s -> Trace.parse s |> Result.ok_exn)))
+           (Arg_type.create (fun s -> Trace.parse s |> Result.get_ok)))
     and colors = flag "colors" no_arg ~doc:"enable printing in colors"
     and margin =
       flag "margin" ~doc:"<cols> wrap debug tracing at <cols> columns"
@@ -206,7 +205,7 @@ let translate =
 let llvm_grp =
   let translate_inputs =
     let expand_argsfile input =
-      if Char.(input.[0] = '@') then
+      if Char.equal input.[0] '@' then
         In_channel.with_file ~f:In_channel.input_lines
           (String.subo ~pos:1 input)
       else [input]
@@ -276,6 +275,9 @@ let readme () =
    module except the M.f function. The <spec> value * enables all debug \
    tracing."
 
+;;
+Printexc.record_backtrace Version.debug
+
 ;;
 Command.run ~version:Version.version ~build_info:Version.build_info
   (Command.group ~summary ~readme ~preserve_subcommand_order:()
diff --git a/sledge/cli/smtlib.ml b/sledge/cli/smtlib.ml
index f8c80daed..2add29919 100644
--- a/sledge/cli/smtlib.ml
+++ b/sledge/cli/smtlib.ml
@@ -57,7 +57,7 @@ and x_trm : var_env -> Smt.Ast.term -> Term.t =
     with _ -> (
       try Term.rational (Q.of_string s)
       with _ -> (
-        try Term.rational (Q.of_float (Float.of_string s))
+        try Term.rational (Q.of_float (Float.of_string_exn s))
         with _ -> fail "not a rational: %a" Smt.Ast.pp_term term () ) ) )
   | Arith (Add, e :: es) ->
       List.fold ~f:(fun s e -> Term.add s (x_trm n e)) ~init:(x_trm n e) es
diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml
index 9da6f75ed..1de4811c5 100644
--- a/sledge/nonstdlib/NS.ml
+++ b/sledge/nonstdlib/NS.ml
@@ -8,212 +8,27 @@
 (** Global namespace intended to be opened in each source file *)
 
 include NS0
-module Monad = Monad
-
-(** Failures *)
-
-exception Replay of exn * Printexc.raw_backtrace * Sexp.t
-
-let register_sexp_of_exn exn sexp_of_exn =
-  Sexplib.Conv.Exn_converter.add
-    (Obj.Extension_constructor.of_val exn)
-    sexp_of_exn
-
-;;
-register_sexp_of_exn
-  (Replay (Stdlib.Not_found, Printexc.get_callstack 1, Sexp.List []))
-  (function
-    | Replay (exn, _, payload) ->
-        Sexp.List [Atom "Replay"; sexp_of_exn exn; payload]
-    | exn -> Sexp.Atom (Printexc.to_string exn) )
-
-let fail = Trace.fail
-
-exception Unimplemented of string
-
-let todo fmt = Trace.raisef (fun msg -> Unimplemented msg) fmt
-
-let warn fmt =
-  let fs = Format.std_formatter in
-  Format.pp_open_box fs 2 ;
-  Format.pp_print_string fs "Warning: " ;
-  Format.kfprintf
-    (fun fs () ->
-      Format.pp_close_box fs () ;
-      Format.pp_force_newline fs () )
-    fs fmt
-
-(** Assertions *)
-
-let assertf cnd fmt =
-  if not cnd then fail fmt
-  else Format.ikfprintf (fun _ () -> ()) Format.str_formatter fmt
-
-let checkf cnd fmt =
-  if not cnd then fail fmt
-  else Format.ikfprintf (fun _ () -> true) Format.str_formatter fmt
-
-let check f x =
-  assert (
-    f x ;
-    true ) ;
-  x
-
-let violates f x =
-  assert (
-    f x ;
-    true ) ;
-  assert false
-
-(** Extensions *)
-
-module Invariant = struct
-  include Core.Invariant
-
-  exception
-    Violation of
-      exn * Printexc.raw_backtrace * Source_code_position.t * Sexp.t
-
-  ;;
-  register_sexp_of_exn
-    (Violation
-       ( Stdlib.Not_found
-       , Printexc.get_callstack 1
-       , Lexing.dummy_pos
-       , Sexp.List [] ))
-    (function
-      | Violation (exn, _, pos, payload) ->
-          Sexp.List
-            [ Atom "Invariant.Violation"
-            ; sexp_of_exn exn
-            ; Source_code_position.sexp_of_t pos
-            ; payload ]
-      | exn -> Sexp.Atom (Printexc.to_string exn) )
-
-  let invariant here t sexp_of_t f =
-    assert (
-      ( try f ()
-        with exn0 ->
-          let bt = Printexc.get_raw_backtrace () in
-          let exn = Violation (exn0, bt, here, sexp_of_t t) in
-          Printexc.raise_with_backtrace exn bt ) ;
-      true )
-end
-
-(** Containers *)
-
-module Option = Option
-include Option.Import
-module List = List
-
-module Array = struct
-  include Core.Array
-
-  let hash_fold_t hash_fold_elt s a =
-    Hash.Builtin.hash_fold_array_frozen hash_fold_elt s a
-
-  module Import = struct
-    type 'a array = 'a t [@@deriving compare, equal, hash, sexp]
-  end
-
-  let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
-  let map_endo xs ~f = map_endo map xs ~f
-
-  let fold_map_inplace a ~init ~f =
-    let s = ref init in
-    let f x =
-      let s', x' = f !s x in
-      s := s' ;
-      x'
-    in
-    map_inplace a ~f ;
-    !s
-
-  let to_list_rev_map xs ~f = fold ~f:(fun ys x -> f x :: ys) ~init:[] xs
-end
-
-include Array.Import
+module Array = Array
+module Float = Float
 module IArray = IArray
 include IArray.Import
-module Set = Set
+module Int = Int
+module List = List
 module Map = Map
+module Monad = Monad
 module Multiset = Multiset
+module Option = Option
+include Option.Import
+module Q = Q_ext
+module Set = Set
+module Sign = Sign
+module String = String
+module Sys = Sys
+module Timer = Timer
+module Z = Z_ext
 
-(** Data types *)
-
-module String = struct
-  include (
-    Core.String :
-      sig
-        include
-          module type of Core.String
-            with module Map := Core.String.Map
-            with module Set := Core.String.Set
-      end )
-
-  module Map = Map.Make (Core.String)
-  module Set = Set.Make (Core.String)
-end
-
-module Int = struct
-  include Stdlib.Int
-
-  include (
-    Int :
-      sig
-        include
-          module type of Core.Int
-            with module Map := Core.Int.Map
-            with module Set := Core.Int.Set
-      end )
-
-  module Map = Map.Make (Int)
-  module Set = Set.Make (Int)
-end
-
-module Q = struct
-  let pp = Q.pp_print
-  let hash = Hashtbl.hash
-  let hash_fold_t s q = Int.hash_fold_t s (hash q)
-  let sexp_of_t q = Sexp.Atom (Q.to_string q)
-
-  let t_of_sexp = function
-    | Sexp.Atom s -> Q.of_string s
-    | _ -> assert false
-
-  let of_z = Q.of_bigint
-
-  let pow q = function
-    | 1 -> q
-    | 0 -> Q.one
-    | -1 -> Q.inv q
-    | n ->
-        let q, n = if n < 0 then (Q.inv q, -n) else (q, n) in
-        Q.make (Z.pow (Q.num q) n) (Z.pow (Q.den q) n)
-
-  include Q
-end
-
-module Z = struct
-  let pp = Z.pp_print
-  let hash = [%hash: Z.t]
-  let hash_fold_t s z = Int.hash_fold_t s (hash z)
-  let sexp_of_t z = Sexp.Atom (Z.to_string z)
-
-  let t_of_sexp = function
-    | Sexp.Atom s -> Z.of_string s
-    | _ -> assert false
-
-  (* the signed 1-bit integers are -1 and 0 *)
-  let true_ = Z.minus_one
-  let false_ = Z.zero
-  let of_bool = function true -> true_ | false -> false_
-  let is_true = Z.equal true_
-  let is_false = Z.equal false_
+module Filename = struct
+  include Filename
 
-  include Z
+  let realpath = Core.Filename.realpath
 end
-
-(** Utilities *)
-
-module Timer = Timer
diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli
index e6f238325..ad615f3fd 100644
--- a/sledge/nonstdlib/NS.mli
+++ b/sledge/nonstdlib/NS.mli
@@ -7,8 +7,41 @@
 
 (** Global namespace intended to be opened in each source file *)
 
-include module type of NS0
-module Monad = Monad
+(** Support for [@@deriving compare, equal, hash, sexp] on builtin types *)
+
+include module type of Ppx_compare_lib.Builtin
+module Hash = Ppx_hash_lib.Std.Hash
+include module type of Hash.Builtin
+module Sexp = Sexplib.Sexp
+include module type of Ppx_sexp_conv_lib.Conv
+
+(** Comparison *)
+
+val min : int -> int -> int
+val max : int -> int -> int
+external ( = ) : int -> int -> bool = "%equal"
+external ( <> ) : int -> int -> bool = "%notequal"
+external ( < ) : int -> int -> bool = "%lessthan"
+external ( > ) : int -> int -> bool = "%greaterthan"
+external ( <= ) : int -> int -> bool = "%lessequal"
+external ( >= ) : int -> int -> bool = "%greaterequal"
+external compare : int -> int -> int = "%compare"
+external equal : int -> int -> bool = "%equal"
+
+(** Polymorphic comparison and hashing *)
+module Poly : sig
+  external ( = ) : 'a -> 'a -> bool = "%equal"
+  external ( <> ) : 'a -> 'a -> bool = "%notequal"
+  external ( < ) : 'a -> 'a -> bool = "%lessthan"
+  external ( > ) : 'a -> 'a -> bool = "%greaterthan"
+  external ( <= ) : 'a -> 'a -> bool = "%lessequal"
+  external ( >= ) : 'a -> 'a -> bool = "%greaterequal"
+  external compare : 'a -> 'a -> int = "%compare"
+  external equal : 'a -> 'a -> bool = "%equal"
+  val min : 'a -> 'a -> 'a
+  val max : 'a -> 'a -> 'a
+  val hash : 'a -> int
+end
 
 (** Function combinators *)
 
@@ -36,136 +69,149 @@ val ( <$ ) : ('a -> unit) -> 'a -> 'a
 (** Apply and ignore function: [f <$ x] is exactly equivalent to [f x ; x].
     Left associative. *)
 
-(** Failures *)
+(** Tuple operations *)
 
-exception Replay of exn * Printexc.raw_backtrace * Sexp.t
-exception Unimplemented of string
+val fst3 : 'a * _ * _ -> 'a
+(** First projection from a triple. *)
 
-val fail : ('a, unit -> _) fmt -> 'a
-(** Emit a message at the current indentation level, and raise a [Failure]
-    exception indicating a fatal error. *)
+val snd3 : _ * 'b * _ -> 'b
+(** Second projection from a triple. *)
 
-val todo : ('a, unit -> _) fmt -> 'a
-(** Raise an [Unimplemented] exception indicating that an input is valid but
-    not handled by the current implementation. *)
+val trd3 : _ * _ * 'c -> 'c
+(** Third projection from a triple. *)
 
-val warn : ('a, unit -> unit) fmt -> 'a
-(** Issue a warning for a survivable problem. *)
+(** Pretty-printing *)
 
-(** Assertions *)
+(** Pretty-printer for argument type. *)
+type 'a pp = Format.formatter -> 'a -> unit
 
-val assertf : bool -> ('a, unit -> unit) fmt -> 'a
-(** Raise an [Failure] exception if the bool argument is false, indicating
-    that the expected condition was not satisfied. *)
+(** Format strings. *)
+type ('a, 'b) fmt = ('a, Format.formatter, unit, 'b) format4
 
-val checkf : bool -> ('a, unit -> bool) fmt -> 'a
-(** As [assertf] but returns the argument bool. *)
+(** Monadic syntax *)
 
-val check : ('a -> unit) -> 'a -> 'a
-(** Assert that function does not raise on argument, and return argument. *)
+module type Applicative_syntax = sig
+  type 'a t
 
-val violates : ('a -> unit) -> 'a -> _
-(** Assert that function raises on argument. *)
-
-(** Extensions *)
+  val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+  val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
+end
 
-module Invariant : sig
-  include module type of Core.Invariant
+module type Monad_syntax = sig
+  type 'a t
 
-  exception
-    Violation of
-      exn * Printexc.raw_backtrace * Source_code_position.t * Sexp.t
+  val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+  val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
+  val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+  val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
 end
 
-(** Containers *)
+(** Monads *)
 
-module Option = Option
-include module type of Option.Import
-module List = List
+module Monad = Monad
 
-module Array : sig
-  include module type of Array
+(** Data types *)
 
-  type 'a t = 'a Array.t [@@deriving compare, equal, hash, sexp]
+module Sign = Sign
+module Char = Containers.Char
+module Int = Int
+module Z = Z_ext
+module Q = Q_ext
+module Float = Float
+module String = String
 
-  module Import : sig
-    type 'a array = 'a t [@@deriving compare, equal, hash, sexp]
-  end
+(** Iterators *)
+
+module Iter = Iter
+include module type of Iter.Import
+
+(** Containers *)
 
-  val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
+type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b
 
-  val map_endo : 'a t -> f:('a -> 'a) -> 'a t
-  (** Like map, but specialized to require [f] to be an endofunction, which
-      enables preserving [==] if [f] preserves [==] of every element. *)
+module Option = Option
+include module type of Option.Import
 
-  val fold_map_inplace :
-    'a array -> init:'s -> f:('s -> 'a -> 's * 'a) -> 's
+module Either : sig
+  type ('a, 'b) t = Left of 'a | Right of 'b
 
-  val to_list_rev_map : 'a array -> f:('a -> 'b) -> 'b list
+  val left : 'a -> ('a, 'b) t
+  val right : 'a -> ('b, 'a) t
 end
 
-include module type of Array.Import
+module List = List
+module Array = Array
 module IArray = IArray
 include module type of IArray.Import
 module Set = Set
 module Map = Map
 module Multiset = Multiset
+module Hashtbl = Base.Hashtbl
+module Hash_set = Base.Hash_set
+module Hash_queue = Core_kernel.Hash_queue
 
-(** Data types *)
+(** Input / Output *)
 
-module String : sig
-  include
-    module type of Core.String
-      with module Map := Core.String.Map
-      with module Set := Core.String.Set
+module In_channel = Stdio.In_channel
+module Out_channel = Stdio.Out_channel
 
-  module Map : Map.S with type key = string
-  module Set : Set.S with type elt = string
-end
+(** System interfaces *)
 
-module Int : sig
-  include module type of Stdlib.Int
+module Sys = Sys
+module Timer = Timer
 
-  include
-    module type of Core.Int
-      with module Map := Core.Int.Map
-      with module Set := Core.Int.Set
+module Filename : sig
+  include module type of Filename
 
-  module Map : Map.S with type key = int
-  module Set : Set.S with type elt = int
+  val realpath : string -> string
 end
 
-module Q : sig
-  include module type of struct
-    include Q
-  end
+(** Invariants *)
+module Invariant : sig
+  exception
+    Violation of exn * Printexc.raw_backtrace * Lexing.position * Sexp.t
 
-  val of_z : Z.t -> t
-  val compare : t -> t -> int
-  val hash : t -> int
-  val hash_fold_t : t Hash.folder
-  val t_of_sexp : Sexp.t -> t
-  val sexp_of_t : t -> Sexp.t
-  val pp : t pp
-  val pow : t -> int -> t
-end
+  val invariant :
+    Lexing.position -> 'a -> ('a -> Sexp.t) -> (unit -> unit) -> unit
 
-module Z : sig
-  include module type of struct
-    include Z
-  end
+  module type S = sig
+    type t
 
-  val compare : t -> t -> int
-  val hash : t -> int
-  val hash_fold_t : t Hash.folder
-  val t_of_sexp : Sexp.t -> t
-  val sexp_of_t : t -> Sexp.t
-  val pp : t pp
-  val true_ : t
-  val false_ : t
-  val of_bool : bool -> t
-  val is_true : t -> bool
-  val is_false : t -> bool
+    val invariant : t -> unit
+  end
 end
 
-module Timer = Timer
+(** Failures *)
+
+exception Replay of exn * Printexc.raw_backtrace * Sexp.t
+exception Unimplemented of string
+
+val fail : ('a, unit -> _) fmt -> 'a
+(** Emit a message at the current indentation level, and raise a [Failure]
+    exception indicating a fatal error. *)
+
+val todo : ('a, unit -> _) fmt -> 'a
+(** Raise an [Unimplemented] exception indicating that an input is valid but
+    not handled by the current implementation. *)
+
+val warn : ('a, unit -> unit) fmt -> 'a
+(** Issue a warning for a survivable problem. *)
+
+(** Assertions *)
+
+val assertf : bool -> ('a, unit -> unit) fmt -> 'a
+(** Raise an [Failure] exception if the bool argument is false, indicating
+    that the expected condition was not satisfied. *)
+
+val checkf : bool -> ('a, unit -> bool) fmt -> 'a
+(** As [assertf] but returns the argument bool. *)
+
+val check : ('a -> unit) -> 'a -> 'a
+(** Assert that function does not raise on argument, and return argument. *)
+
+val violates : ('a -> unit) -> 'a -> _
+(** Assert that function raises on argument. *)
+
+(**)
+
+module With_return = Base.With_return
diff --git a/sledge/nonstdlib/NS0.ml b/sledge/nonstdlib/NS0.ml
index 9ca08dad7..6532c468b 100644
--- a/sledge/nonstdlib/NS0.ml
+++ b/sledge/nonstdlib/NS0.ml
@@ -5,28 +5,51 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-include (
-  Core :
-    sig
-      include
-        module type of Core
-          with module Printexc := Core.Printexc
-           and module Monad := Core.Monad
-           and module Option := Core.Option
-           and module List := Core.List
-           and module Map := Core.Map
-           and module Map_intf := Core.Map_intf
-           and module Set := Core.Set
-           and module Set_intf := Core.Set_intf
-           and module String := Core.String
-           and type -'a return := 'a Core.return
-    end )
+(** Global namespace used when defining the rest of nonstdlib, which is
+    extended in NS, the exposed interface of nonstdlib *)
+
+(** Support for [@@deriving compare, equal, hash, sexp] on builtin types *)
+
+include Ppx_compare_lib.Builtin
+module Hash = Ppx_hash_lib.Std.Hash
+include Hash.Builtin
+module Sexp = Sexplib.Sexp
+include Ppx_sexp_conv_lib.Conv
+
+(** Iterators *)
 
 module Iter = Iter
 include Iter.Import
 
-external ( == ) : 'a -> 'a -> bool = "%eq"
-external ( != ) : 'a -> 'a -> bool = "%noteq"
+(** Specialize polymorphic comparison to int *)
+
+external ( = ) : int -> int -> bool = "%equal"
+external ( <> ) : int -> int -> bool = "%notequal"
+external ( < ) : int -> int -> bool = "%lessthan"
+external ( > ) : int -> int -> bool = "%greaterthan"
+external ( <= ) : int -> int -> bool = "%lessequal"
+external ( >= ) : int -> int -> bool = "%greaterequal"
+external compare : int -> int -> int = "%compare"
+external equal : int -> int -> bool = "%equal"
+
+let min x y = if x <= y then x else y
+let max x y = if x >= y then x else y
+
+(** Polymorphic comparison and hashing *)
+module Poly = struct
+  external ( = ) : 'a -> 'a -> bool = "%equal"
+  external ( <> ) : 'a -> 'a -> bool = "%notequal"
+  external ( < ) : 'a -> 'a -> bool = "%lessthan"
+  external ( > ) : 'a -> 'a -> bool = "%greaterthan"
+  external ( <= ) : 'a -> 'a -> bool = "%lessequal"
+  external ( >= ) : 'a -> 'a -> bool = "%greaterequal"
+  external compare : 'a -> 'a -> int = "%compare"
+  external equal : 'a -> 'a -> bool = "%equal"
+
+  let min x y = if x <= y then x else y
+  let max x y = if x >= y then x else y
+  let hash = Stdlib.Hashtbl.hash
+end
 
 (** Function combinators *)
 
@@ -47,11 +70,18 @@ let ( <$ ) f x =
 
 let ( let@ ) x f = x @@ f
 
-(** Pretty-printer for argument type. *)
+(** Tuple operations *)
+
+let fst3 (x, _, _) = x
+let snd3 (_, y, _) = y
+let trd3 (_, _, z) = z
+
+(** Pretty-printing *)
+
 type 'a pp = Format.formatter -> 'a -> unit
+type ('a, 'b) fmt = ('a, Format.formatter, unit, 'b) format4
 
-(** Format strings. *)
-type ('a, 'b) fmt = ('a, 'b) Trace.fmt
+(** Monadic syntax *)
 
 module type Applicative_syntax = sig
   type 'a t
@@ -67,6 +97,12 @@ module type Monad_syntax = sig
   val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
 end
 
+(** Data types *)
+
+module Char = Containers.Char
+
+(** Container utilities *)
+
 let map_endo map t ~f =
   let change = ref false in
   let t' =
@@ -76,3 +112,121 @@ let map_endo map t ~f =
         x' )
   in
   if !change then t' else t
+
+(** Containers *)
+
+type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b
+
+(* from upcoming Stdlib *)
+module Either = struct
+  type ('a, 'b) t = Left of 'a | Right of 'b
+
+  let left v = Left v
+  let right v = Right v
+end
+
+module Hashtbl = Base.Hashtbl
+module Hash_set = Base.Hash_set
+module Hash_queue = Core_kernel.Hash_queue
+
+(** Input / Output *)
+
+module In_channel = Stdio.In_channel
+module Out_channel = Stdio.Out_channel
+
+(** Invariants *)
+
+let register_sexp_of_exn exn sexp_of_exn =
+  Sexplib.Conv.Exn_converter.add
+    (Obj.Extension_constructor.of_val exn)
+    sexp_of_exn
+
+module Invariant = struct
+  type position = Lexing.position =
+    {pos_fname: string; pos_lnum: int; pos_bol: int; pos_cnum: int}
+  [@@deriving sexp_of]
+
+  exception Violation of exn * Printexc.raw_backtrace * position * Sexp.t
+
+  ;;
+  register_sexp_of_exn
+    (Violation
+       (Not_found, Printexc.get_callstack 1, Lexing.dummy_pos, Sexp.List []))
+    (function
+      | Violation (exn, _, pos, payload) ->
+          Sexp.List
+            [ Atom "Invariant.Violation"
+            ; sexp_of_exn exn
+            ; sexp_of_position pos
+            ; payload ]
+      | exn -> Sexp.Atom (Printexc.to_string exn) )
+
+  let invariant here t sexp_of_t f =
+    assert (
+      ( try f ()
+        with exn ->
+          let bt = Printexc.get_raw_backtrace () in
+          let exn = Violation (exn, bt, here, sexp_of_t t) in
+          Printexc.raise_with_backtrace exn bt ) ;
+      true )
+
+  module type S = sig
+    type t
+
+    val invariant : t -> unit
+  end
+end
+
+(** Failures *)
+
+exception Replay of exn * Printexc.raw_backtrace * Sexp.t
+
+;;
+register_sexp_of_exn
+  (Replay (Not_found, Printexc.get_callstack 1, Sexp.List []))
+  (function
+    | Replay (exn, _, payload) ->
+        Sexp.List [Atom "Replay"; sexp_of_exn exn; payload]
+    | exn -> Sexp.Atom (Printexc.to_string exn) )
+
+let fail = Trace.fail
+
+exception Unimplemented of string
+
+let todo fmt = Trace.raisef (fun msg -> Unimplemented msg) fmt
+
+let warn fmt =
+  let fs = Format.std_formatter in
+  Format.pp_open_box fs 2 ;
+  Format.pp_print_string fs "Warning: " ;
+  Format.kfprintf
+    (fun fs () ->
+      Format.pp_close_box fs () ;
+      Format.pp_force_newline fs () )
+    fs fmt
+
+(** Assertions *)
+
+let assertf cnd fmt =
+  if not cnd then fail fmt
+  else Format.ikfprintf (fun _ () -> ()) Format.str_formatter fmt
+
+let checkf cnd fmt =
+  if not cnd then fail fmt
+  else Format.ikfprintf (fun _ () -> true) Format.str_formatter fmt
+
+let check f x =
+  assert (
+    f x ;
+    true ) ;
+  x
+
+let violates f x =
+  assert (
+    f x ;
+    true ) ;
+  assert false
+
+(** Deprecated *)
+
+module With_return = Base.With_return
diff --git a/sledge/nonstdlib/array.ml b/sledge/nonstdlib/array.ml
new file mode 100644
index 000000000..0ffc378fb
--- /dev/null
+++ b/sledge/nonstdlib/array.ml
@@ -0,0 +1,24 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open NS0
+include Base.Array
+
+let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
+let map_endo xs ~f = map_endo map xs ~f
+
+let fold_map_inplace a ~init ~f =
+  let s = ref init in
+  let f x =
+    let s', x' = f !s x in
+    s := s' ;
+    x'
+  in
+  map_inplace a ~f ;
+  !s
+
+let to_list_rev_map xs ~f = fold ~f:(fun ys x -> f x :: ys) ~init:[] xs
diff --git a/sledge/nonstdlib/array.mli b/sledge/nonstdlib/array.mli
new file mode 100644
index 000000000..49429f151
--- /dev/null
+++ b/sledge/nonstdlib/array.mli
@@ -0,0 +1,18 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open NS0
+include module type of Base.Array
+
+val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
+
+val map_endo : 'a t -> f:('a -> 'a) -> 'a t
+(** Like map, but specialized to require [f] to be an endofunction, which
+    enables preserving [==] if [f] preserves [==] of every element. *)
+
+val fold_map_inplace : 'a array -> init:'s -> f:('s -> 'a -> 's * 'a) -> 's
+val to_list_rev_map : 'a array -> f:('a -> 'b) -> 'b list
diff --git a/sledge/nonstdlib/float.ml b/sledge/nonstdlib/float.ml
new file mode 100644
index 000000000..c0bcd1c6c
--- /dev/null
+++ b/sledge/nonstdlib/float.ml
@@ -0,0 +1,18 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+include Stdlib.Float
+
+external ( = ) : float -> float -> bool = "%equal"
+external ( <> ) : float -> float -> bool = "%notequal"
+external ( < ) : float -> float -> bool = "%lessthan"
+external ( > ) : float -> float -> bool = "%greaterthan"
+external ( <= ) : float -> float -> bool = "%lessequal"
+external ( >= ) : float -> float -> bool = "%greaterequal"
+
+let of_string_exn = of_string
+let of_string = of_string_opt
diff --git a/sledge/nonstdlib/float.mli b/sledge/nonstdlib/float.mli
new file mode 100644
index 000000000..401eaf68a
--- /dev/null
+++ b/sledge/nonstdlib/float.mli
@@ -0,0 +1,17 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+include module type of Stdlib.Float
+
+external ( = ) : float -> float -> bool = "%equal"
+external ( <> ) : float -> float -> bool = "%notequal"
+external ( < ) : float -> float -> bool = "%lessthan"
+external ( > ) : float -> float -> bool = "%greaterthan"
+external ( <= ) : float -> float -> bool = "%lessequal"
+external ( >= ) : float -> float -> bool = "%greaterequal"
+val of_string : string -> float option
+val of_string_exn : string -> float
diff --git a/sledge/nonstdlib/iArray.ml b/sledge/nonstdlib/iArray.ml
index ddb847f70..9bcc798bc 100644
--- a/sledge/nonstdlib/iArray.ml
+++ b/sledge/nonstdlib/iArray.ml
@@ -7,14 +7,15 @@
 
 (** IArray - Immutable view of an array *)
 
-open NS0
+open! NS0
+include Core_kernel.Perms.Export
 
 include (
-  Array.Permissioned :
-    module type of Array.Permissioned
-      with type ('a, 'p) t := ('a, 'p) Array.Permissioned.t )
+  Core_kernel.Array.Permissioned :
+    module type of Core_kernel.Array.Permissioned
+      with type ('a, 'p) t := ('a, 'p) Core_kernel.Array.Permissioned.t )
 
-type 'a t = ('a, immutable) Array.Permissioned.t
+type 'a t = ('a, immutable) Core_kernel.Array.Permissioned.t
 
 let a2i (a : 'a array) : 'a t = Obj.magic a
 let i2a (a : 'a t) : 'a array = Obj.magic a
@@ -41,15 +42,14 @@ let contains_dup ~compare xs =
     (find_consecutive_duplicate ~equal (sorted_copy ~compare xs))
 
 let fold_map xs ~init ~f =
-  Tuple2.map_snd ~f:a2i (Array.fold_map (i2a xs) ~init ~f)
+  let a, ys = Array.fold_map (i2a xs) ~init ~f in
+  (a, a2i ys)
 
 let fold_map_until xs ~init ~f ~finish =
-  with_return (fun {return} ->
+  With_return.with_return (fun {return} ->
       finish
         (fold_map xs ~init ~f:(fun s x ->
-             match (f s x : _ Continue_or_stop.t) with
-             | Continue x -> x
-             | Stop x -> return x )) )
+             match f s x with Continue x -> x | Stop x -> return x )) )
 
 let map_endo xs ~f = map_endo map xs ~f
 
diff --git a/sledge/nonstdlib/iArray.mli b/sledge/nonstdlib/iArray.mli
index 4ea161cb7..e0952bd26 100644
--- a/sledge/nonstdlib/iArray.mli
+++ b/sledge/nonstdlib/iArray.mli
@@ -13,13 +13,14 @@
     structure, it only attempts to make it inconvenient to unintentionally
     mutate. *)
 
-open NS0
+open! NS0
+include module type of Core_kernel.Perms.Export
 
 include
-  module type of Array.Permissioned
-    with type ('a, 'p) t := ('a, 'p) Array.Permissioned.t
+  module type of Core_kernel.Array.Permissioned
+    with type ('a, 'p) t := ('a, 'p) Core_kernel.Array.Permissioned.t
 
-type 'a t = ('a, immutable) Array.Permissioned.t
+type 'a t = ('a, immutable) Core_kernel.Array.Permissioned.t
 [@@deriving compare, equal, hash, sexp]
 
 module Import : sig
@@ -45,7 +46,7 @@ val fold_map :
 val fold_map_until :
      'a t
   -> init:'accum
-  -> f:('accum -> 'a -> ('accum * 'b, 'final) Continue_or_stop.t)
+  -> f:('accum -> 'a -> ('accum * 'b, 'final) continue_or_stop)
   -> finish:('accum * 'b t -> 'final)
   -> 'final
 
diff --git a/sledge/nonstdlib/int.ml b/sledge/nonstdlib/int.ml
new file mode 100644
index 000000000..f210464a9
--- /dev/null
+++ b/sledge/nonstdlib/int.ml
@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! NS0
+include CCInt
+include Base.Int
+module Set = Set.Make (Base.Int)
+module Map = Map.Make (Base.Int)
diff --git a/sledge/nonstdlib/int.mli b/sledge/nonstdlib/int.mli
new file mode 100644
index 000000000..8783af4d8
--- /dev/null
+++ b/sledge/nonstdlib/int.mli
@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! NS0
+include module type of CCInt
+include module type of Base.Int
+module Set : Set.S with type elt = int
+module Map : Map.S with type key = int
diff --git a/sledge/nonstdlib/list.ml b/sledge/nonstdlib/list.ml
index f81eb47ce..7f7fcdad1 100644
--- a/sledge/nonstdlib/list.ml
+++ b/sledge/nonstdlib/list.ml
@@ -5,8 +5,10 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open NS0
-include Core.List
+open! NS0
+include Base.List
+
+exception Not_found_s = Base.Sexp.Not_found_s
 
 let rec pp ?pre ?suf sep pp_elt fs = function
   | [] -> ()
@@ -42,7 +44,7 @@ let find_map_remove xs ~f =
   find_map_remove_ [] xs
 
 let fold_option xs ~init ~f =
-  let@ {return} = with_return in
+  let@ {return} = With_return.with_return in
   Some
     (fold xs ~init ~f:(fun acc elt ->
          match f acc elt with Some res -> res | None -> return None ))
@@ -54,7 +56,7 @@ let rev_map_unzip xs ~f =
       let y, z = f x in
       (y :: ys, z :: zs) )
 
-let remove_exn ?(equal = phys_equal) xs x =
+let remove_exn ?(equal = ( == )) xs x =
   let rec remove_ ys = function
     | [] -> raise (Not_found_s (Atom __LOC__))
     | z :: xs ->
@@ -78,17 +80,17 @@ let symmetric_diff ~compare xs ys =
     | x :: xs, y :: ys ->
         let ord = compare x y in
         if ord = 0 then symmetric_diff_ xs ys
-        else if ord < 0 then First x :: symmetric_diff_ xs yys
-        else Second y :: symmetric_diff_ xxs ys
-    | xs, [] -> map ~f:Either.first xs
-    | [], ys -> map ~f:Either.second ys
+        else if ord < 0 then Left x :: symmetric_diff_ xs yys
+        else Right y :: symmetric_diff_ xxs ys
+    | xs, [] -> map ~f:Either.left xs
+    | [], ys -> map ~f:Either.right ys
   in
   symmetric_diff_ (sort ~compare xs) (sort ~compare ys)
 
 let pp_diff ~compare sep pp_elt fs (xs, ys) =
-  let pp_diff_elt fs elt =
+  let pp_diff_elt fs (elt : _ Either.t) =
     match elt with
-    | First x -> Format.fprintf fs "-- %a" pp_elt x
-    | Second y -> Format.fprintf fs "++ %a" pp_elt y
+    | Left x -> Format.fprintf fs "-- %a" pp_elt x
+    | Right y -> Format.fprintf fs "++ %a" pp_elt y
   in
   pp sep pp_diff_elt fs (symmetric_diff ~compare xs ys)
diff --git a/sledge/nonstdlib/list.mli b/sledge/nonstdlib/list.mli
index 8d9f77ef9..af3456362 100644
--- a/sledge/nonstdlib/list.mli
+++ b/sledge/nonstdlib/list.mli
@@ -5,8 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open NS0
-include module type of Core.List
+open! NS0
+include module type of Base.List
 
 val pp :
      ?pre:(unit, unit) fmt
diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml
index 1e0b0b817..990754569 100644
--- a/sledge/nonstdlib/map.ml
+++ b/sledge/nonstdlib/map.ml
@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open NS0
+open! NS0
 include Map_intf
 
 module Make (Key : sig
diff --git a/sledge/nonstdlib/map_intf.ml b/sledge/nonstdlib/map_intf.ml
index 0afbeb641..67606fdaf 100644
--- a/sledge/nonstdlib/map_intf.ml
+++ b/sledge/nonstdlib/map_intf.ml
@@ -5,9 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open NS0
-
-exception Not_found = Stdlib.Not_found
+open! NS0
 
 module type S = sig
   type key
diff --git a/sledge/nonstdlib/multiset.ml b/sledge/nonstdlib/multiset.ml
index e2429689c..e44935db2 100644
--- a/sledge/nonstdlib/multiset.ml
+++ b/sledge/nonstdlib/multiset.ml
@@ -7,7 +7,7 @@
 
 (** Multiset - Set with multiplicity for each element *)
 
-open NS0
+open! NS0
 include Multiset_intf
 
 module Make
diff --git a/sledge/nonstdlib/multiset_intf.ml b/sledge/nonstdlib/multiset_intf.ml
index b31b58909..69cfa200b 100644
--- a/sledge/nonstdlib/multiset_intf.ml
+++ b/sledge/nonstdlib/multiset_intf.ml
@@ -7,7 +7,7 @@
 
 (** Multiset - Set with (signed) rational multiplicity for each element *)
 
-open NS0
+open! NS0
 
 module type MULTIPLICITY = sig
   type t [@@deriving compare, equal, hash, sexp]
diff --git a/sledge/nonstdlib/option.ml b/sledge/nonstdlib/option.ml
index 84e7e4ba4..1fa93acc5 100644
--- a/sledge/nonstdlib/option.ml
+++ b/sledge/nonstdlib/option.ml
@@ -6,7 +6,7 @@
  *)
 
 open! NS0
-include Core.Option
+include Base.Option
 
 let pp fmt pp_elt fs = function
   | Some x -> Format.fprintf fs fmt pp_elt x
diff --git a/sledge/nonstdlib/option.mli b/sledge/nonstdlib/option.mli
index 9c8b49fc0..caf9d8c8c 100644
--- a/sledge/nonstdlib/option.mli
+++ b/sledge/nonstdlib/option.mli
@@ -6,7 +6,7 @@
  *)
 
 open! NS0
-include module type of Core.Option
+include module type of Base.Option
 
 val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> 'a option pp
 (** Pretty-print an option. *)
diff --git a/sledge/nonstdlib/q_ext.ml b/sledge/nonstdlib/q_ext.ml
new file mode 100644
index 000000000..7240729e8
--- /dev/null
+++ b/sledge/nonstdlib/q_ext.ml
@@ -0,0 +1,25 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open NS0
+
+let pp = Q.pp_print
+let hash = Hashtbl.hash
+let hash_fold_t s q = Int.hash_fold_t s (hash q)
+let sexp_of_t q = Sexp.Atom (Q.to_string q)
+let t_of_sexp = function Sexp.Atom s -> Q.of_string s | _ -> assert false
+let of_z = Q.of_bigint
+
+let pow q = function
+  | 1 -> q
+  | 0 -> Q.one
+  | -1 -> Q.inv q
+  | n ->
+      let q, n = if n < 0 then (Q.inv q, -n) else (q, n) in
+      Q.make (Z.pow (Q.num q) n) (Z.pow (Q.den q) n)
+
+include Q
diff --git a/sledge/nonstdlib/q_ext.mli b/sledge/nonstdlib/q_ext.mli
new file mode 100644
index 000000000..81aa2e575
--- /dev/null
+++ b/sledge/nonstdlib/q_ext.mli
@@ -0,0 +1,21 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open NS0
+
+include module type of struct
+  include Q
+end
+
+val of_z : Z.t -> t
+val compare : t -> t -> int
+val hash : t -> int
+val hash_fold_t : t Hash.folder
+val t_of_sexp : Sexp.t -> t
+val sexp_of_t : t -> Sexp.t
+val pp : t pp
+val pow : t -> int -> t
diff --git a/sledge/nonstdlib/set.ml b/sledge/nonstdlib/set.ml
index 8dea6aa32..9261637b8 100644
--- a/sledge/nonstdlib/set.ml
+++ b/sledge/nonstdlib/set.ml
@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open NS0
+open! NS0
 module Option = CCOpt
 include Set_intf
 
diff --git a/sledge/nonstdlib/set_intf.ml b/sledge/nonstdlib/set_intf.ml
index a62817542..4c9dbd1f4 100644
--- a/sledge/nonstdlib/set_intf.ml
+++ b/sledge/nonstdlib/set_intf.ml
@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open NS0
+open! NS0
 
 module type S = sig
   type elt
diff --git a/sledge/nonstdlib/sign.ml b/sledge/nonstdlib/sign.ml
new file mode 100644
index 000000000..2351ab58a
--- /dev/null
+++ b/sledge/nonstdlib/sign.ml
@@ -0,0 +1,15 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! NS0
+
+type t = Neg | Zero | Pos
+
+let of_int i = if i < 0 then Neg else if i = 0 then Zero else Pos
+
+let of_float f =
+  if Float.(f < 0.) then Neg else if Float.(f = 0.) then Zero else Pos
diff --git a/sledge/nonstdlib/sign.mli b/sledge/nonstdlib/sign.mli
new file mode 100644
index 000000000..4b6a482ff
--- /dev/null
+++ b/sledge/nonstdlib/sign.mli
@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! NS0
+
+type t = Neg | Zero | Pos
+
+val of_int : int -> t
+val of_float : float -> t
diff --git a/sledge/nonstdlib/string.ml b/sledge/nonstdlib/string.ml
new file mode 100644
index 000000000..69f1ad492
--- /dev/null
+++ b/sledge/nonstdlib/string.ml
@@ -0,0 +1,11 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! NS0
+include Base.String
+module Set = Set.Make (Base.String)
+module Map = Map.Make (Base.String)
diff --git a/sledge/nonstdlib/string.mli b/sledge/nonstdlib/string.mli
new file mode 100644
index 000000000..3d9df7636
--- /dev/null
+++ b/sledge/nonstdlib/string.mli
@@ -0,0 +1,11 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! NS0
+include module type of Base.String
+module Set : Set.S with type elt = string
+module Map : Map.S with type key = string
diff --git a/sledge/nonstdlib/sys.ml b/sledge/nonstdlib/sys.ml
new file mode 100644
index 000000000..fff3dfdfa
--- /dev/null
+++ b/sledge/nonstdlib/sys.ml
@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+include Stdlib.Sys
+
+let getenv = getenv_opt
diff --git a/sledge/nonstdlib/sys.mli b/sledge/nonstdlib/sys.mli
new file mode 100644
index 000000000..a373cdbe2
--- /dev/null
+++ b/sledge/nonstdlib/sys.mli
@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+val executable_name : string
+val getenv : string -> string option
+external getcwd : unit -> string = "caml_sys_getcwd"
+val word_size : int
+val ocaml_version : string
diff --git a/sledge/nonstdlib/timer.ml b/sledge/nonstdlib/timer.ml
index 30d4c9099..57c620527 100644
--- a/sledge/nonstdlib/timer.ml
+++ b/sledge/nonstdlib/timer.ml
@@ -7,7 +7,7 @@
 
 (** Timers for runtime statistics *)
 
-open NS0
+open! NS0
 
 type t =
   { mutable ustart: float
diff --git a/sledge/nonstdlib/z_ext.ml b/sledge/nonstdlib/z_ext.ml
new file mode 100644
index 000000000..a3b89cf12
--- /dev/null
+++ b/sledge/nonstdlib/z_ext.ml
@@ -0,0 +1,23 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open NS0
+
+let pp = Z.pp_print
+let hash = [%hash: Z.t]
+let hash_fold_t s z = Int.hash_fold_t s (hash z)
+let sexp_of_t z = Sexp.Atom (Z.to_string z)
+let t_of_sexp = function Sexp.Atom s -> Z.of_string s | _ -> assert false
+
+(* the signed 1-bit integers are -1 and 0 *)
+let true_ = Z.minus_one
+let false_ = Z.zero
+let of_bool = function true -> true_ | false -> false_
+let is_true = Z.equal true_
+let is_false = Z.equal false_
+
+include Z
diff --git a/sledge/nonstdlib/z_ext.mli b/sledge/nonstdlib/z_ext.mli
new file mode 100644
index 000000000..a426418b2
--- /dev/null
+++ b/sledge/nonstdlib/z_ext.mli
@@ -0,0 +1,24 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open NS0
+
+include module type of struct
+  include Z
+end
+
+val compare : t -> t -> int
+val hash : t -> int
+val hash_fold_t : t Hash.folder
+val t_of_sexp : Sexp.t -> t
+val sexp_of_t : t -> Sexp.t
+val pp : t pp
+val true_ : t
+val false_ : t
+val of_bool : bool -> t
+val is_true : t -> bool
+val is_false : t -> bool
diff --git a/sledge/report/sledge_report.ml b/sledge/report/sledge_report.ml
index 8e2482982..8b1228ef7 100644
--- a/sledge/report/sledge_report.ml
+++ b/sledge/report/sledge_report.ml
@@ -5,6 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+module Command = Core.Command
 module Tbl = CCHashtbl.Make (String)
 
 let read filename =
@@ -251,7 +252,7 @@ let color max dat =
       (scale1 x r0 r1, scale1 x g0 g1, scale1 x b0 b1)
     in
     let x = Float.max (-1.) (Float.min x 1.) in
-    if Float.is_negative x then scale (-.x) lace green else scale x lace red
+    if Float.(x < 0.) then scale (-.x) lace green else scale x lace red
   in
   let rgb_to_hex (r, g, b) =
     let to_int x = Int.min 255 (Int.max 0 (Float.to_int x)) in
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index f2491bddd..8f1cf5ab9 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -467,7 +467,9 @@ module Make (Dom : Domain_intf.Dom) = struct
     [%Trace.info
       "@[<2>exec inst@\n@[%a@]@\n%a@]" Dom.pp state Llair.Inst.pp inst] ;
     Report.step () ;
-    Dom.exec_inst state inst |> Result.of_option ~error:(state, inst)
+    Dom.exec_inst state inst
+    |> function
+    | Some state -> Result.Ok state | None -> Result.Error (state, inst)
 
   let exec_block :
          exec_opts
diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index b2e01a488..3e5664116 100644
--- a/sledge/src/domain_intf.ml
+++ b/sledge/src/domain_intf.ml
@@ -10,7 +10,7 @@ module type Dom = sig
   type t [@@deriving equal, sexp_of]
 
   val pp : t pp
-  val report_fmt_thunk : t -> Formatter.t -> unit
+  val report_fmt_thunk : t -> Format.formatter -> unit
   val init : Llair.Global.t iarray -> t
   val join : t -> t -> t option
   val is_false : t -> bool
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 171dd9e64..9c2f8db99 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -13,7 +13,7 @@ open Fol
 type t = Sh.t [@@deriving equal, sexp]
 
 let pp fs q = Format.fprintf fs "@[{ %a@ }@]" Sh.pp q
-let report_fmt_thunk = Fn.flip pp
+let report_fmt_thunk = Fun.flip pp
 
 (* set by cli *)
 let simplify_states = ref true
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index b3839e804..e833de63f 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/sledge/src/domain_used_globals.ml
@@ -10,7 +10,7 @@
 type t = Llair.Reg.Set.t [@@deriving equal, sexp]
 
 let pp = Llair.Reg.Set.pp
-let report_fmt_thunk = Fn.flip pp
+let report_fmt_thunk = Fun.flip pp
 let empty = Llair.Reg.Set.empty
 
 let init globals =
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index b13aac5e3..7fc66f773 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -318,7 +318,9 @@ module Term = struct
     | Return {exp; _} -> (
       match parent with
       | Some parent ->
-          assert (Bool.(Option.is_some exp = Option.is_some parent.freturn))
+          assert (
+            Bool.equal (Option.is_some exp) (Option.is_some parent.freturn)
+          )
       | None -> assert true )
     | Throw _ | Unreachable -> assert true
 
@@ -470,7 +472,9 @@ module Func = struct
           not
             (List.contains_dup (entry_cfg func) ~compare:(fun b1 b2 ->
                  String.compare b1.lbl b2.lbl )) ) ;
-        assert (Bool.(Option.is_some return = Option.is_some func.freturn)) ;
+        assert (
+          Bool.equal (Option.is_some return) (Option.is_some func.freturn)
+        ) ;
         iter_term func ~f:(fun term -> Term.invariant ~parent:func term)
     | _ -> assert false
 
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index 6b0c3179c..d30a44f87 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -73,7 +73,7 @@ and term : Llair.Exp.t -> T.t =
       uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))
   | Integer {typ= _; data} -> T.integer data
   | Float {data; typ= _} -> (
-    match Q.of_float (Float.of_string data) with
+    match Q.of_float (Float.of_string_exn data) with
     | q when Q.is_real q -> T.rational q
     | _ | (exception Invalid_argument _) ->
         uap0 (Funsym.uninterp ("float_" ^ data)) )
diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index 3594e0f79..29f361021 100644
--- a/sledge/src/report.ml
+++ b/sledge/src/report.ml
@@ -138,7 +138,7 @@ let init ?append filename =
      | _ -> Some (Out_channel.create ?append filename)) ;
   name :=
     Option.value
-      (Stdlib.Filename.chop_suffix_opt ~suffix:".sexp" filename)
+      (Filename.chop_suffix_opt ~suffix:".sexp" filename)
       ~default:filename ;
   at_exit (fun () ->
       output (process_times ()) ;
diff --git a/sledge/src/report.mli b/sledge/src/report.mli
index c6435ca65..06af41c1f 100644
--- a/sledge/src/report.mli
+++ b/sledge/src/report.mli
@@ -10,8 +10,8 @@
 val init : ?append:bool -> string -> unit
 val step : unit -> unit
 val unknown_call : Llair.term -> unit
-val invalid_access_inst : (Formatter.t -> unit) -> Llair.inst -> unit
-val invalid_access_term : (Formatter.t -> unit) -> Llair.term -> unit
+val invalid_access_inst : (Format.formatter -> unit) -> Llair.inst -> unit
+val invalid_access_term : (Format.formatter -> unit) -> Llair.term -> unit
 
 type status =
   | Safe of {steps: int}
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
index 4f5e950d0..f12eb5edf 100644
--- a/sledge/src/ses/equality.ml
+++ b/sledge/src/ses/equality.ml
@@ -96,7 +96,7 @@ end = struct
     |>
     [%Trace.retn fun {pf} r' ->
       pf "%a" pp_diff (r, r') ;
-      assert (r' != r ==> not (equal r' r))]
+      assert (r' == r || not (equal r' r))]
 
   (** compose a substitution with a mapping *)
   let compose1 ~key ~data s =
@@ -198,10 +198,10 @@ let prefer e f =
 
 (** orient equations based on representative preference *)
 let orient e f =
-  match Ordering.of_int (prefer e f) with
-  | Less -> Some (e, f)
-  | Equal -> None
-  | Greater -> Some (f, e)
+  match Sign.of_int (prefer e f) with
+  | Neg -> Some (e, f)
+  | Zero -> None
+  | Pos -> Some (f, e)
 
 let norm (_, _, s) e = Subst.norm s e
 
@@ -420,8 +420,9 @@ let pre_invariant r =
       (* carrier is closed under subterms *)
       Term.iter trm ~f:(fun subtrm ->
           assert (
-            non_interpreted subtrm
-            ==> (Term.is_constant subtrm || in_car r subtrm)
+            (not (non_interpreted subtrm))
+            || Term.is_constant subtrm
+            || in_car r subtrm
             || fail "@[subterm %a@ of %a@ not in carrier of@ %a@]" Term.pp
                  subtrm Term.pp trm pp r () ) ) )
 
@@ -433,7 +434,8 @@ let invariant r =
     || Subst.for_alli r.rep ~f:(fun ~key:a ~data:a' ->
            Subst.for_alli r.rep ~f:(fun ~key:b ~data:b' ->
                Term.compare a b >= 0
-               || congruent r a b ==> Term.equal a' b'
+               || (not (congruent r a b))
+               || Term.equal a' b'
                || fail "not congruent %a@ %a@ in@ %a" Term.pp a Term.pp b pp
                     r () ) ) )
 
@@ -451,7 +453,7 @@ let false_ = {true_ with sat= false}
 let lookup r a =
   ([%Trace.call fun {pf} -> pf "%a" Term.pp a]
   ;
-  let@ {return} = with_return in
+  let@ {return} = With_return.with_return in
   Subst.iteri r.rep ~f:(fun ~key:b ~data:b' ->
       if semi_congruent r a b then return b' ) ;
   a)
@@ -506,7 +508,7 @@ let merge us a b r =
 
 (** find an unproved equation between congruent terms *)
 let find_missing r =
-  let@ {return} = with_return in
+  let@ {return} = With_return.with_return in
   Subst.iteri r.rep ~f:(fun ~key:a ~data:a' ->
       let a_subnorm = Term.map ~f:(Subst.norm r.rep) a in
       Subst.iteri r.rep ~f:(fun ~key:b ~data:b' ->
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index 903ca9756..794fee608 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -153,8 +153,8 @@ let assert_monomial mono =
       Qset.iter args ~f:(fun factor exponent ->
           assert (Z.equal (Q.den exponent) Z.one) ;
           assert (Q.sign exponent > 0) ;
-          assert_indeterminate factor |> Fn.id )
-  | _ -> assert_indeterminate mono |> Fn.id
+          assert_indeterminate factor |> Fun.id )
+  | _ -> assert_indeterminate mono |> Fun.id
 
 (* a polynomial term is a monomial multiplied by a non-zero coefficient
  *     c × ∏ᵢ xᵢ
@@ -169,8 +169,8 @@ let assert_poly_term mono coeff =
       | None | Some ((Integer _ | Rational _), _) -> assert false
       | Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n))
       ) ;
-      assert_monomial mono |> Fn.id
-  | _ -> assert_monomial mono |> Fn.id
+      assert_monomial mono |> Fun.id
+  | _ -> assert_monomial mono |> Fun.id
 
 (* a polynomial is a linear combination of monomials, e.g.
  *     ∑ᵢ cᵢ × ∏ⱼ xᵢⱼ
@@ -184,7 +184,7 @@ let assert_polynomial poly =
       | None | Some ((Integer _ | Rational _), _) -> assert false
       | Some (_, k) -> assert (Qset.length args > 1 || not (Q.equal Q.one k))
       ) ;
-      Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id)
+      Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fun.id)
   | _ -> assert false
 
 (* sequence args of Extract and Concat must be sequence terms, in
@@ -200,10 +200,10 @@ let rec assert_sequence = function
 let invariant e =
   let@ () = Invariant.invariant [%here] e [%sexp_of: t] in
   match e with
-  | And _ -> assert_conjunction e |> Fn.id
-  | Or _ -> assert_disjunction e |> Fn.id
-  | Add _ -> assert_polynomial e |> Fn.id
-  | Mul _ -> assert_monomial e |> Fn.id
+  | And _ -> assert_conjunction e |> Fun.id
+  | Or _ -> assert_disjunction e |> Fun.id
+  | Add _ -> assert_polynomial e |> Fun.id
+  | Mul _ -> assert_monomial e |> Fun.id
   | Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
       assert_sequence e
   | ApN (Record, elts) -> assert (not (IArray.is_empty elts))
@@ -744,10 +744,10 @@ let simp_le x y =
 
 let rec simp_eq x y =
   match
-    match Ordering.of_int (compare x y) with
-    | Equal -> None
-    | Less -> Some (x, y)
-    | Greater -> Some (y, x)
+    match Sign.of_int (compare x y) with
+    | Neg -> Some (x, y)
+    | Zero -> None
+    | Pos -> Some (y, x)
   with
   (* e = e ==> true *)
   | None -> bool true
@@ -1145,7 +1145,7 @@ let iter_vars e ~f =
   iter_terms ~f:(fun e -> Option.iter ~f (Var.of_term e)) e
 
 let exists_vars e ~f =
-  with_return (fun {return} ->
+  With_return.with_return (fun {return} ->
       iter_vars e ~f:(fun v -> if f v then return true) ;
       false )
 
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 10ef4a00b..4e0e73c19 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -633,7 +633,7 @@ let rec norm_ s q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Context.Subst.pp s pp_raw q]
   ;
   let q =
-    map q ~f_sjn:(norm_ s) ~f_ctx:Fn.id ~f_trm:(Context.Subst.subst s)
+    map q ~f_sjn:(norm_ s) ~f_ctx:Fun.id ~f_trm:(Context.Subst.subst s)
       ~f_fml:(Formula.map_terms ~f:(Context.Subst.subst s))
   in
   let xs, ctx = Context.apply_subst (Var.Set.union q.us q.xs) s q.ctx in
diff --git a/sledge/src/test/equality_test.ml b/sledge/src/test/equality_test.ml
index f822e7d02..b92bdb557 100644
--- a/sledge/src/test/equality_test.ml
+++ b/sledge/src/test/equality_test.ml
@@ -15,7 +15,7 @@ let%test_module _ =
 
     (* let () =
      *   Trace.init ~margin:160
-     *     ~config:(Result.ok_exn (Trace.parse "+Equality"))
+     *     ~config:(Result.get_ok (Trace.parse "+Equality"))
      *     ()
      *
      * [@@@warning "-32"] *)
diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml
index b2ebeaf3e..2eb5e34b0 100644
--- a/sledge/src/test/fol_test.ml
+++ b/sledge/src/test/fol_test.ml
@@ -16,7 +16,7 @@ let%test_module _ =
 
     (* let () =
      *   Trace.init ~margin:160
-     *     ~config:(Result.ok_exn (Trace.parse "+Fol"))
+     *     ~config:(Result.get_ok (Trace.parse "+Fol"))
      *     () *)
 
     [@@@warning "-32"]
diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml
index d5a9ded64..51898fd95 100644
--- a/sledge/src/test/sh_test.ml
+++ b/sledge/src/test/sh_test.ml
@@ -15,7 +15,7 @@ let%test_module _ =
     let () = Trace.init ~margin:68 ()
 
     (* let () =
-     *   Trace.init ~margin:160 ~config:(Result.ok_exn (Trace.parse "+Sh")) ()
+     *   Trace.init ~margin:160 ~config:(Result.get_ok (Trace.parse "+Sh")) ()
      *
      * [@@@warning "-32"] *)
 
diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml
index 1151acd6c..6d225a2c6 100644
--- a/sledge/src/test/solver_test.ml
+++ b/sledge/src/test/solver_test.ml
@@ -12,13 +12,13 @@ let%test_module _ =
   ( module struct
     let () =
       Trace.init ~margin:68
-        ~config:(Result.ok_exn (Trace.parse "+Solver.infer_frame"))
+        ~config:(Result.get_ok (Trace.parse "+Solver.infer_frame"))
         ()
 
     (* let () =
      *   Trace.init ~margin:160
      *     ~config:
-     *       (Result.ok_exn (Trace.parse "+Solver.infer_frame+Solver.excise"))
+     *       (Result.get_ok (Trace.parse "+Solver.infer_frame+Solver.excise"))
      *     ()
      * 
      * [@@@warning "-32"] *)