diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..8000dd9
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+.vagrant
diff --git a/Makefile b/Makefile
index 6e5a47f..1aef24a 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
 OCB_FLAGS = -use-ocamlfind -cflag -thread -cflag -linkpkg \
-  -pkg unix -pkg yojson -pkg ocamlyices -pkg xml-light -pkg str \
+  -pkg unix -pkg yojson -pkg ocamlyices -pkg xml-light -pkg str -pkg zarith -pkg z3 \
 	-I src -I src/util -I src/input -I src/logic -I src/proof -I src/rewriting \
-	-I src/termination # -pkg z3 
+	-I src/termination
 
 OCB = ocamlbuild $(OCB_FLAGS)
 OCB_NATIVE = ocamlbuild $(OCB_FLAGS)
diff --git a/README b/README
index 107dcd9..0749c03 100644
--- a/README
+++ b/README
@@ -13,6 +13,11 @@ Using OCamlbuild, the Maedmax executable can be created by executing
  $ make
 in this directory.
 
+Alternatively, using Vagrant (https://www.vagrantup.com), a virtual machine
+provisioned with a Maedmax executable can be created by executing
+ $ vagrant up
+in this directory.
+
 -------------------------------------------------------------------------------
    USAGE
 -------------------------------------------------------------------------------
@@ -53,14 +58,14 @@ Here is what these (and all other) options mean:
    - Option -K controls the number of TRSs selected in every iteration.
    - Option -N controls how many passive equations are added to the set of
      active facts, per selected TRS.
-   - The instantiation depth of ground joinability checks is controlled by -I 
-     (cf. the number of repetitions in the strategy given on p.9 of the paper). 
+   - The instantiation depth of ground joinability checks is controlled by -I
+     (cf. the number of repetitions in the strategy given on p.9 of the paper).
  - The remaining options are mainly there for analyzing input problems and
    debugging.
    - Option --term performs a termination check of the input system, considering
      the rules to be oriented as given.
    - Option --analyze prints problem properties, including recognized theories.
-   - Debugging output is triggered by the option -D. 
+   - Debugging output is triggered by the option -D.
 
 
 -------------------------------------------------------------------------------
diff --git a/Vagrantfile b/Vagrantfile
new file mode 100644
index 0000000..d30acd1
--- /dev/null
+++ b/Vagrantfile
@@ -0,0 +1,57 @@
+# -*- mode: ruby -*-
+# vi: set ft=ruby :
+
+# All Vagrant configuration is done below. The "2" in Vagrant.configure
+# configures the configuration version (we support older styles for
+# backwards compatibility). Please don't change it unless you know what
+# you're doing.
+Vagrant.configure("2") do |config|
+  # Every Vagrant development environment requires a box. You can search for
+  # boxes at https://vagrantcloud.com/search.
+  config.vm.box = "hashicorp/bionic64"
+
+  # Provision the VM with maedmax.
+  config.vm.provision "shell", privileged: false, inline: <<-SHELL
+    yes | {
+      sudo apt-get update
+      sudo apt-get install opam
+      sudo apt-get install m4
+      sudo apt-get install python3-distutils
+      sudo opam init
+      eval `opam config env`
+      sudo opam update
+      sudo opam install ocamlfind
+      sudo opam install ocamlbuild
+      sudo opam install yojson
+      sudo opam depext conf-gmp.1
+      wget -q -O- http://git.io/sWxMmg | sudo sh -s /vagrant/yices.tar.gz
+      sudo opam install ocamlyices
+      sudo opam install xml-light
+      sudo opam install zarith
+      LIB_PATH="/home/vagrant/.opam/system/lib"
+      Z3_PATH="$LIB_PATH/z3"
+      Z3_PATH_ALT="$LIB_PATH/Z3"
+      CMD="export LD_LIBRARY_PATH=\"$Z3_PATH/lib:$LD_LIBRARY_PATH\""
+      echo "$CMD" >> .bashrc
+      eval "$CMD"
+      git clone https://github.com/Z3Prover/z3
+      cd z3
+      git checkout 79734f26aee55309077de1f26e9b6f50ecd99ceb # version 4.8.9 official release
+      python3 scripts/mk_make.py --ml --prefix="$Z3_PATH"
+      cd build; sudo make
+      sudo make install
+      sudo cp "$Z3_PATH/lib/libz3.so" "$Z3_PATH" # I have no idea why this is necessary, but it is, and mv instead of cp doesn't work
+      sudo mv $Z3_PATH_ALT/* "$Z3_PATH" # merge z3 directories (I'm not sure why they're separate to begin with)
+      sudo rm -r "$Z3_PATH_ALT"
+      cd ~
+      CMD="cp -r /vagrant maedmax-build; cd maedmax-build"
+      echo "$CMD" >> buildlocal.sh
+      eval "$CMD"
+      make
+      mv maedmax ..
+      cd ..
+      rm -rf maedmax-build
+    }
+    exit
+  SHELL
+end
diff --git a/src/ckb_AC.ml b/src/ckb_AC.ml
index c748ffd..3eac898 100644
--- a/src/ckb_AC.ml
+++ b/src/ckb_AC.ml
@@ -60,8 +60,8 @@ let max_constraints s =
 ;;
 
 (* shorthands for settings *)
-let termination_strategy s = 
-  match s.heuristic.strategy with 
+let termination_strategy s =
+  match s.heuristic.strategy with
   | [] -> failwith "no termination strategy found"
   | (s, _, _, _, _) :: _ -> s
 ;;
@@ -112,7 +112,7 @@ let rewrite rr aa =
   L.fold_left rew_nf (NS.empty (), NS.empty ()) (NS.to_list aa)
 ;;
 
-let reduced rr aa = 
+let reduced rr aa =
  let ls_old, ls_new = rewrite rr (NS.of_list aa) in NS.add_all ls_new ls_old
 ;;
 
@@ -193,7 +193,7 @@ let max_k s =
   let ctx, cc = s.context, s.equations in
   let k = s.heuristic.k !(A.iterations) in
   let cc_eq = [ Lit.terms n | n <- NS.to_list cc ] in
-  let cc_symm = [n | n <- NS.to_list (NS.symmetric cc)] in 
+  let cc_symm = [n | n <- NS.to_list (NS.symmetric cc)] in
   let cc_symml = [Lit.terms c | c <- cc_symm] in
   L.iter (fun n -> ignore (C.store_rule_var ctx n)) cc_symml;
   (* lookup is not for free: get these variables only once *)
@@ -273,6 +273,7 @@ let preorient state es =
 ;;
 
 let complete (settings, heuristic) es =
+  A.restart ();
   let es = [Lit.make_axiom (normalize (Lit.terms e)) | e <- es] in
   let ctx = Logic.mk_context () in
   let ss = L.map (fun (ts,_,_,_,_) -> ts) heuristic.strategy in
diff --git a/src/logic/z3x.ml b/src/logic/z3x.ml
index ed2754c..9583c8a 100755
--- a/src/logic/z3x.ml
+++ b/src/logic/z3x.ml
@@ -7,6 +7,7 @@ module Arith = Arithmetic
 module I = Arith.Integer
 module Real = Arith.Real
 module BV = BitVector
+module Big_int = Big_int_Z
 
 (*** TYPES *******************************************************************)
 type context = {
diff --git a/src/main.ml b/src/main.ml
index f28a5de..57369e3 100755
--- a/src/main.ml
+++ b/src/main.ml
@@ -553,7 +553,7 @@ let run file ((es, gs) as input) =
   let timer = Timer.start () in
   check_order_params [Lit.terms e | e <- es @ gs];
   let ans, proof =
-    if gs = [] && !settings.unfailing && not !settings.complete_if_no_goal then
+    if gs = [] && !settings.unfailing && not !settings.complete_if_no_goal && not !Settings.interactive then
       (SAT, GroundCompletion ([], [], Order.default))
     else if !settings.modulo_ac then
       Ckb_AC.complete (!settings, !heuristic) (fst input)
diff --git a/src/rewriting/rewriting.ml b/src/rewriting/rewriting.ml
index 7f73d28..f84060b 100755
--- a/src/rewriting/rewriting.ml
+++ b/src/rewriting/rewriting.ml
@@ -13,15 +13,13 @@ let rec rewrite_aux rules = function
   | F (f, ts) ->
       let tpls = [ rewrite_aux rules ti | ti <- ts ] in
       let ls = [ ti | _, ti <- tpls ] in
-      let used_rules = Listx.unique (List.flatten (List.map fst tpls)) in 
+      let used_rules = Listx.unique (List.flatten (List.map fst tpls)) in
       if used_rules <> [] then used_rules, F (f, ls)
       else
        let opt, u = rewrite_at_root (F (f, ls)) rules in
        match opt with
         | None -> used_rules, u
-        | Some lr -> 
-	  if List.mem lr used_rules 
-	  then used_rules, u else (lr :: used_rules), u
+        | Some lr -> [lr], u
 ;;
 
 let step_at_with t p (l,r) =
@@ -32,7 +30,7 @@ let step_at_with t p (l,r) =
 
 let rec nf rules t =
  let used, u = rewrite_aux rules t in
- match used with 
+ match used with
  | [] -> t
  | _ -> nf rules u
 
diff --git a/src/rewriting/term.mli b/src/rewriting/term.mli
index b5697fa..226694e 100755
--- a/src/rewriting/term.mli
+++ b/src/rewriting/term.mli
@@ -8,7 +8,6 @@ module Sub : sig
   val is_empty : 'a t -> bool
   val mem : key -> 'a t -> bool
   val add : key -> 'a -> 'a t -> 'a t
-  val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
   val find : key -> 'a t -> 'a
   val filter : (key -> 'a -> bool) -> 'a t -> 'a t
   val iter : (key -> 'a -> unit) -> 'a t -> unit
@@ -18,7 +17,7 @@ module Sub : sig
 end
 (** Term operations *)
 
-type t = 
+type t =
   | V of Signature.var
   | F of Signature.sym * t list
 
diff --git a/yices.tar.gz b/yices.tar.gz
new file mode 100644
index 0000000..210714e
Binary files /dev/null and b/yices.tar.gz differ