diff --git a/bap-vibes/src/compiler.ml b/bap-vibes/src/compiler.ml
index 89bfcc94..259dc0bb 100644
--- a/bap-vibes/src/compiler.ml
+++ b/bap-vibes/src/compiler.ml
@@ -61,20 +61,24 @@ let create_vibes_ir
   ir, exclude_regs
 
 (* Compile one patch from BIR to VIBES IR *)
-let compile_one_vibes_ir
-  (isel_model_filepath : string option) 
+let compile_one_vibes_ir 
+  (isel_model_filepath : string option)
   (count : int KB.t)
   (patch : Data.Patch.t) : int KB.t =
-  count >>= fun n -> Data.Patch.get_assembly patch >>= begin function
-    | Some _asm ->
-      Events.(send @@ Info "The patch has no IR to translate.\n");
-      KB.return () (* Assembly already set. Presumably by the user. *)
-    | None ->
+  count >>= fun n ->
+  Data.Patch.get_patch_code_exn patch >>= (fun code ->
+  match code with
+    | ASMCode _asm ->
+         Events.(send @@ Info "Assembly patch has no IR to translate.\n");
+         KB.return ()
+    | PrimusCode _ | CCode _ ->
+  begin
       let info_str =
-        Format.sprintf "Translating patch %d BIR to VIBES IR..." n
+        Format.asprintf "Translating patch %s BIR to VIBES IR..."
+          (string_of_int n)
       in
       Events.(send @@ Info info_str);
-      Data.Patch.get_bir patch >>= fun bir ->
+      Data.Patch.get_sem patch >>= fun bir ->
 
       let info_str = Format.asprintf "\nPatch: %a\n\n%!" KB.Value.pp bir in
       Events.(send @@ Info info_str);
@@ -91,7 +95,7 @@ let compile_one_vibes_ir
       Events.(send @@ Info (Ir.pretty_ir ir));
       Events.(send @@ Rule);
       KB.return ()
-  end >>= fun () -> KB.return (n + 1)
+  end) >>= fun () -> KB.return (n + 1)
 
 (* Compile one patch from VIBES IR to assembly *)
 let compile_one_assembly
@@ -103,34 +107,36 @@ let compile_one_assembly
      Ir.t ->
      (Ir.t * Minizinc.sol) KB.t)
     (count : int KB.t) (patch : Data.Patch.t) : int KB.t =
-  count >>= fun n -> Data.Patch.get_assembly patch >>= begin function
-    | Some _asm ->
-      Events.(send @@ Info "The patch already has assembly\n");
-      Events.(send @@ Rule);
-      KB.return () (* Assembly already set. Presumably by the user. *)
-    | None ->
-      let info_str =
-        Format.asprintf "Translating patch %s VIBES IR to assembly..."
-          (string_of_int n)
-      in
-      Events.(send @@ Info info_str);
-      Data.Patch.get_raw_ir_exn patch >>= fun ir ->
-      Data.Patch.get_exclude_regs patch >>= fun exclude_regs ->
-      let exclude_regs = Option.value exclude_regs ~default:String.Set.empty in
-      Data.Patch.get_minizinc_solutions patch >>= fun prev_sols ->
-      Data.Patch.get_target patch >>= fun target ->
-      Data.Patch.get_lang patch >>= fun lang ->
-      let prev_sols = Set.to_list prev_sols in
-      create_assembly
-        (solver target lang prev_sols ~exclude_regs)
-        ir >>= fun (assembly, new_sol) ->
-      Data.Patch.set_assembly patch (Some assembly) >>= fun () ->
-      Events.(send @@ Info "The patch has the following assembly:\n");
-      Events.(send @@ Rule);
-      Events.(send @@ Info (String.concat ~sep:"\n" assembly));
-      Events.(send @@ Rule);
-      Data.Patch.add_minizinc_solution patch new_sol 
-  end >>= fun () -> KB.return (n + 1)
+  count >>= fun n ->
+    Data.Patch.get_patch_code_exn patch >>= (fun asm ->
+    match asm with
+    | ASMCode asm -> KB.return [asm]
+    | PrimusCode _ | CCode _ ->
+      begin
+        let info_str =
+          Format.asprintf "Translating patch %s VIBES IR to assembly..."
+            (string_of_int n)
+        in
+        Events.(send @@ Info info_str);
+        Data.Patch.get_raw_ir_exn patch >>= fun ir ->
+        Data.Patch.get_exclude_regs patch >>= fun exclude_regs ->
+        let exclude_regs = Option.value exclude_regs ~default:String.Set.empty in
+        Data.Patch.get_minizinc_solutions patch >>= fun prev_sols ->
+        Data.Patch.get_target patch >>= fun target ->
+        Data.Patch.get_lang patch >>= fun lang ->
+        let prev_sols = Set.to_list prev_sols in
+        create_assembly
+          (solver target lang prev_sols ~exclude_regs)
+          ir >>= fun (assembly, new_sol) ->
+        Data.Patch.add_minizinc_solution patch new_sol >>= fun () -> 
+        KB.return assembly
+      end) >>= fun assembly ->
+  Data.Patch.set_assembly patch (Some assembly) >>= fun () ->
+  Events.(send @@ Info "The patch has the following assembly:\n");
+  Events.(send @@ Rule);
+  Events.(send @@ Info (String.concat ~sep:"\n" assembly));
+  Events.(send @@ Rule);
+  KB.return (n + 1)
 
 (* Converts the patch (as BIR) to VIBES IR instructions. *)
 let compile_ir ?(isel_model_filepath = None) (obj : Data.t) : unit KB.t =
diff --git a/bap-vibes/src/config.ml b/bap-vibes/src/config.ml
index fdf594d5..d3ed61e8 100644
--- a/bap-vibes/src/config.ml
+++ b/bap-vibes/src/config.ml
@@ -5,7 +5,7 @@ open !Core_kernel
 module Hvar = Higher_var
 module Wp_params = Bap_wp.Run_parameters
 
-type patch_code = CCode of Cabs.definition | ASMCode of string
+type patch_code = CCode of Cabs.definition | ASMCode of string | PrimusCode of string
 
 (* A type to represent a patch. *)
 type patch =
@@ -104,7 +104,8 @@ let string_of_hvar (v : Hvar.t) : string =
 let patch_to_string (p : patch) : string =
   let code = match p.patch_code with
   | CCode ccode -> Utils.print_c Cprint.print_def ccode
-  | ASMCode asmcode -> asmcode in
+  | ASMCode asmcode -> asmcode
+  | PrimusCode funname -> funname in
   let h_vars =
     String.concat ~sep:"\n" (List.map p.patch_vars ~f:string_of_hvar)
   in
diff --git a/bap-vibes/src/config.mli b/bap-vibes/src/config.mli
index 4f9d257e..33cff49a 100644
--- a/bap-vibes/src/config.mli
+++ b/bap-vibes/src/config.mli
@@ -13,7 +13,7 @@ type patch
 type t
 
 (** A type to represent patch cody which may either be C or literal assembly *)
-type patch_code = CCode of Cabs.definition | ASMCode of string
+type patch_code = CCode of Cabs.definition | ASMCode of string  | PrimusCode of string
 
 (** A type to represent known regions that may be overwritten with patch code *)
 type patch_space = {
diff --git a/bap-vibes/src/data.ml b/bap-vibes/src/data.ml
index f84c4882..dea6199a 100644
--- a/bap-vibes/src/data.ml
+++ b/bap-vibes/src/data.ml
@@ -2,7 +2,6 @@
    We expect much evolution here... *)
 
 open !Core_kernel
-open Bap.Std
 open Bap_knowledge
 open Bap_core_theory
 open Knowledge.Syntax
@@ -44,7 +43,7 @@ let sexp_domain : Sexp.t option KB.Domain.t = KB.Domain.optional
     "sexp-domain"
 
 (* Optional C definition domain for the patch code. *)
-let source_domain : Cabs.definition option KB.Domain.t = KB.Domain.optional
+let source_domain : Config.patch_code option KB.Domain.t = KB.Domain.optional
     ~equal:Poly.equal
     "source-domain"
 
@@ -101,7 +100,7 @@ module Patch = struct
   let patch_name : (patch_cls, string option) KB.slot =
     KB.Class.property ~package patch "patch-name" string_domain
 
-  let patch_code : (patch_cls, Cabs.definition option) KB.slot =
+  let patch_code : (patch_cls, Config.patch_code option) KB.slot =
     KB.Class.property ~package patch "patch-code" source_domain
 
   let patch_label : (patch_cls, Theory.label option) KB.slot =
@@ -150,13 +149,13 @@ module Patch = struct
     | None -> Kb_error.fail Kb_error.Missing_patch_name
     | Some value -> KB.return value
 
-  let set_patch_code (obj : t) (data : Cabs.definition option) : unit KB.t =
+  let set_patch_code (obj : t) (data : Config.patch_code option) : unit KB.t =
     KB.provide patch_code obj data
 
-  let get_patch_code (obj : t) : Cabs.definition option KB.t =
+  let get_patch_code (obj : t) : Config.patch_code option KB.t =
     KB.collect patch_code obj
 
-  let get_patch_code_exn (obj : t) : Cabs.definition KB.t =
+  let get_patch_code_exn (obj : t) : Config.patch_code KB.t =
     get_patch_code obj >>= fun result ->
     match result with
     | None -> Kb_error.fail Kb_error.Missing_patch_code
@@ -190,13 +189,13 @@ module Patch = struct
     KB.Object.create Theory.Program.cls >>= fun lab ->
     KB.provide patch_label obj (Some lab)
 
-  let set_bir (obj : t) (sem : Insn.t) : unit KB.t =
+  let set_sem (obj : t) (sem : Theory.Semantics.t) : unit KB.t =
     KB.collect patch_label obj >>= fun olab ->
     (* FIXME: fail more gracefully *)
     let lab = Option.value_exn olab in
     KB.provide Theory.Semantics.slot lab sem
 
-  let get_bir (obj : t) : Insn.t KB.t =
+  let get_sem (obj : t) : Theory.Semantics.t KB.t =
     KB.collect patch_label obj >>= fun olab ->
     (* FIXME: fail more gracefully *)
     let lab = Option.value_exn olab in
diff --git a/bap-vibes/src/data.mli b/bap-vibes/src/data.mli
index 51cd80c0..6e3132cb 100644
--- a/bap-vibes/src/data.mli
+++ b/bap-vibes/src/data.mli
@@ -2,7 +2,6 @@
     properties that the VIBES toolchain defines and manipulates *)
 
 open !Core_kernel
-open Bap.Std
 open Bap_knowledge
 open Bap_core_theory
 
@@ -14,7 +13,7 @@ val int_domain       : int option KB.Domain.t
 val int64_domain     : int64 option KB.Domain.t
 val bitvec_domain    : Bitvec.t option KB.Domain.t
 val sexp_domain      : Sexp.t option KB.Domain.t
-val source_domain    : Cabs.definition option KB.Domain.t
+val source_domain    : Config.patch_code option KB.Domain.t
 val assembly_domain  : string list option KB.Domain.t
 val unit_domain      : unit KB.Domain.t
 val higher_vars_domain : Hvar.t list option KB.Domain.t
@@ -49,7 +48,7 @@ module Patch : sig
   include Knowledge.Object.S with type t := t
 
   val patch_name : (patch_cls, string option) KB.slot
-  val patch_code : (patch_cls, Cabs.definition option) KB.slot
+  val patch_code : (patch_cls, Config.patch_code option) KB.slot
   val patch_point : (patch_cls, Bitvec.t option) KB.slot
   val patch_size : (patch_cls, int option) KB.slot
   val patch_label : (patch_cls, Theory.label option) KB.slot
@@ -70,9 +69,9 @@ module Patch : sig
   val get_patch_name : t -> string option KB.t
   val get_patch_name_exn : t -> string KB.t
 
-  val set_patch_code : t -> Cabs.definition option -> unit KB.t
-  val get_patch_code : t -> Cabs.definition option KB.t
-  val get_patch_code_exn : t -> Cabs.definition KB.t
+  val set_patch_code : t -> Config.patch_code option -> unit KB.t
+  val get_patch_code : t -> Config.patch_code option KB.t
+  val get_patch_code_exn : t -> Config.patch_code KB.t
 
   val set_patch_point : t -> Bitvec.t option -> unit KB.t
   val get_patch_point : t -> Bitvec.t option KB.t
@@ -86,8 +85,8 @@ module Patch : sig
      that will contain the semantics. This *must* be called before
      set_bir! *)
   val init_sem : t -> unit KB.t
-  val set_bir : t -> insn -> unit KB.t
-  val get_bir : t -> insn KB.t
+  val set_sem : t -> Theory.Semantics.t -> unit KB.t
+  val get_sem : t -> Theory.Semantics.t KB.t
 
   val set_raw_ir : t -> Ir.t option -> unit KB.t
   val get_raw_ir : t -> Ir.t option KB.t
diff --git a/bap-vibes/src/patch_ingester.ml b/bap-vibes/src/patch_ingester.ml
index 21e3dc09..fb2b41b9 100644
--- a/bap-vibes/src/patch_ingester.ml
+++ b/bap-vibes/src/patch_ingester.ml
@@ -5,31 +5,47 @@ open Bap_knowledge
 open Knowledge.Syntax
 open Core_kernel
 open Bap_core_theory
+open Bap_primus.Std
 
 module KB = Knowledge
 open KB.Let
 
-let provide_bir (tgt : Theory.target) (patch : Data.Patch.t) : unit KB.t =
+let provide_sem (tgt : Theory.target) (patch : Data.Patch.t) : unit KB.t =
   Theory.instance () >>=
   Theory.require >>= fun (module Core) ->
   let module CParser = Core_c.Eval(Core) in
   Data.Patch.init_sem patch >>= fun () ->
   Data.Patch.get_patch_name_exn patch >>= fun name ->
-  Data.Patch.get_patch_code_exn patch >>= fun code ->
   Events.(send @@ Info (Printf.sprintf "Patch %s" name));
-  let code_str = Utils.print_c Cprint.print_def code in
-  Events.(send @@ Info (Printf.sprintf "%s" code_str));
-
+  Data.Patch.get_patch_code_exn patch >>= fun code ->
   (* Get the patch (as BIR). *)
-  let* hvars = Data.Patch.get_patch_vars_exn patch in
-  let* bir = CParser.c_patch_to_eff hvars tgt code in
-
+  let* hvars = Data.Patch.get_patch_vars_exn patch in  
+  let* sem = match code with
+  | CCode code -> 
+        begin
+          let code_str = Utils.print_c Cprint.print_def code in
+          Events.(send @@ Info (Printf.sprintf "%s" code_str));
+          CParser.c_patch_to_eff hvars tgt code
+        end
+  | PrimusCode name -> 
+        begin
+          Primus.Lisp.Unit.create tgt >>= fun unit ->
+          KB.Object.scoped Theory.Program.cls @@ fun obj ->
+          KB.sequence [
+            KB.provide Theory.Label.unit obj (Some unit);
+            KB.provide Primus.Lisp.Semantics.name obj (Some (KB.Name.create name));
+          ] >>= fun () ->
+          KB.collect Theory.Semantics.slot obj
+        end
+  | ASMCode _asm -> Kb_error.fail (Kb_error.Not_implemented 
+                      "[Patch_ingester.provide_sem] called on assembly patch")
+  in
   Events.(send @@ Info "The patch has the following BIL:");
   Events.(send @@ Rule);
-  let bir_str = Format.asprintf "%a" Bil.pp (KB.Value.get Bil.slot bir) in
+  let bir_str = Format.asprintf "%a" Bil.pp (KB.Value.get Bil.slot sem) in
   Events.(send @@ Info bir_str);
   Events.(send @@ Rule);
-  Data.Patch.set_bir patch bir
+  Data.Patch.set_sem patch sem
 
 (* Ingests a single patch, populating the relevant fields of the KB,
    most notably the semantics field of the corresponding patch (and
@@ -38,10 +54,10 @@ let ingest_one (tgt : Theory.target) (patch_num : int KB.t) (patch : Data.Patch.
     : int KB.t =
   patch_num >>= fun patch_num ->
   Events.(send @@ Info (Printf.sprintf "\nIngesting patch %d." patch_num));
-  (Data.Patch.get_assembly patch >>= fun asm ->
-  match asm with
-  | Some _asm -> KB.return () (* Assembly is user provided *)
-  | None -> provide_bir tgt patch) >>= fun () ->
+  (Data.Patch.get_patch_code_exn patch >>= fun code ->
+  match code with
+  | ASMCode _asm -> KB.return () (* Assembly is user provided *)
+  | PrimusCode _ | CCode _ -> provide_sem tgt patch) >>= fun () ->
   KB.return @@ patch_num+1
 
 (* Processes the whole patch associated with [obj], populating all the
diff --git a/bap-vibes/src/seeder.ml b/bap-vibes/src/seeder.ml
index b39a8b72..d5294420 100644
--- a/bap-vibes/src/seeder.ml
+++ b/bap-vibes/src/seeder.ml
@@ -69,10 +69,7 @@ let create_patches
         ~addr:(Config.patch_point p)
     in
     let* () = Data.Patch.set_patch_name obj (Some patch_name) in
-    let* () = match Config.patch_code p with
-      | CCode ccode -> Data.Patch.set_patch_code obj (Some ccode)
-      | ASMCode asmcode -> Data.Patch.set_assembly obj (Some [asmcode])
-    in
+    let* () = Data.Patch.set_patch_code obj (Some (Config.patch_code p)) in
     let* () = Data.Patch.set_patch_point obj (Some (Config.patch_point p)) in
     let* () = Data.Patch.set_patch_size obj (Some (Config.patch_size p)) in
     let* () = Data.Patch.set_lang obj lang in
diff --git a/bap-vibes/tests/integration/test_minizinc.ml b/bap-vibes/tests/integration/test_minizinc.ml
index 67d60ff3..2a5f0dfc 100644
--- a/bap-vibes/tests/integration/test_minizinc.ml
+++ b/bap-vibes/tests/integration/test_minizinc.ml
@@ -110,7 +110,7 @@ let test_minizinc_ex1 (ctxt : test_ctxt) : unit =
     KB.Object.create Data.Patch.patch >>= fun patch ->
     Data.Patch.init_sem patch >>= fun () ->
     Patches.get_bir "ret-3" 32 >>= fun bil ->
-    Data.Patch.set_bir patch bil >>= fun () ->
+    Data.Patch.set_sem patch bil >>= fun () ->
     Data.Patched_exe.set_patches obj
       (Data.Patch_set.singleton patch) >>= fun () ->
     (* Now run the compiler. *)
diff --git a/bap-vibes/tests/unit/test_compiler.ml b/bap-vibes/tests/unit/test_compiler.ml
index b7c6d4fc..c1c3b2a3 100644
--- a/bap-vibes/tests/unit/test_compiler.ml
+++ b/bap-vibes/tests/unit/test_compiler.ml
@@ -26,7 +26,7 @@ let test_compile (_ : test_ctxt) : unit =
       obj (Some H.minizinc_model_filepath) >>= fun () ->
     Patches.get_bir H.patch 32 >>= fun bil ->
     KB.Object.create Data.Patch.patch >>= fun patch ->
-    Data.Patch.set_bir patch bil >>= fun _ ->
+    Data.Patch.set_sem patch bil >>= fun _ ->
     Data.Patched_exe.set_patches obj
       (Data.Patch_set.singleton patch) >>= fun _ ->
 
diff --git a/bap-vibes/tests/unit/test_patch_ingester.ml b/bap-vibes/tests/unit/test_patch_ingester.ml
index b0d06077..6f328029 100644
--- a/bap-vibes/tests/unit/test_patch_ingester.ml
+++ b/bap-vibes/tests/unit/test_patch_ingester.ml
@@ -27,7 +27,7 @@ let test_ingest (_ : test_ctxt) : unit =
     match Data.Patch_set.to_list patches with
     | [] -> assert_failure "Result patch missing."
     | (p :: []) ->
-      Data.Patch.get_bir p >>= fun bir ->
+      Data.Patch.get_sem p >>= fun bir ->
       Patches.Ret_3.prog 32 >>= fun expected ->
       let open Bap.Std in
       let expected = KB.Value.get Bil.slot expected in
@@ -61,7 +61,7 @@ let test_ingest_with_no_patch (_ : test_ctxt) : unit =
   let result = KB.run Data.cls computation KB.empty in
 
   (* The ingester should diverge with the appropriate error. *)
-  let expected = Kb_error.Problem Kb_error.Missing_patch_name in
+  let expected = Kb_error.Problem Kb_error.Missing_patch_code in
   H.assert_error Data.Patched_exe.patches expected result
 
 (* Test that [Patch_ingester.ingest] errors with no addr_size in the KB. *)
@@ -100,7 +100,7 @@ let test_ingest_with_no_patch_vars (_ : test_ctxt) : unit =
     KB.Object.create Data.Patch.patch >>= fun patch ->
 
     let code = H.dummy_code in
-    Data.Patch.set_patch_code patch (Some code) >>= fun () ->
+    Data.Patch.set_patch_code patch (Some (CCode code)) >>= fun () ->
     Data.Patch.set_patch_name patch (Some H.patch) >>= fun () ->
     Data.Patched_exe.set_patches obj
       (Data.Patch_set.singleton patch) >>= fun () ->
diff --git a/bin/system-tests/tests/test-arm-exes.bash b/bin/system-tests/tests/test-arm-exes.bash
index 9adfbf33..94edbc3a 100644
--- a/bin/system-tests/tests/test-arm-exes.bash
+++ b/bin/system-tests/tests/test-arm-exes.bash
@@ -219,9 +219,26 @@ test_arm_linear_ssa () {
     run_make "make patch.reference -C ${TEST_DIR}" 0
     run_arm_exe "${TEST_PATCH_EXE}" 3
 }
+test_arm_primus () {
+    local TEST_DIR="${EXES_DIR}/arm-simple-primus"
+    local MAIN_EXE="${TEST_DIR}/main.reference"
+    local PATCH_EXE="${TEST_DIR}/main.patched.reference"
+    local TEST_PATCH_EXE="${TEST_DIR}/test.patched.by.vibes"
+
+    print_header "Checking ${TEST_DIR}"
+
+    # Check the precompiled executables.
+    run_arm_exe "${MAIN_EXE}" 5
+    run_arm_exe "${PATCH_EXE}" 3
 
+    # Check that vibes patches correctly.
+    run_make "make clean -C ${TEST_DIR}" 0
+    run_make "make patch.reference -C ${TEST_DIR}" 0
+    run_arm_exe "${TEST_PATCH_EXE}" 3
+}
 test_arm_simple_sum () {
     local TEST_DIR="${EXES_DIR}/arm-simple-sum"
+
     local MAIN_EXE="${TEST_DIR}/main.reference"
     local PATCH_EXE="${TEST_DIR}/main.patched.reference"
     local TEST_PATCH_EXE="${TEST_DIR}/test.patched.by.vibes"
@@ -232,6 +249,7 @@ test_arm_simple_sum () {
     run_arm_exe "${MAIN_EXE}" 5
     run_arm_exe "${PATCH_EXE}" 9
 
+
     # Check that vibes patches correctly.
     run_make "make clean -C ${TEST_DIR}" 0
     run_make "make patch.reference -C ${TEST_DIR}" 0
@@ -276,12 +294,14 @@ test_arm_branch_bsi () {
     run_make "make clean -C ${TEST_DIR}" 0
     run_make "make main.patched -C ${TEST_DIR}" 0
     run_arm_exe "${TEST_PATCH_EXE}" 2
+
 }
 
 # Run all tests
 run_all () {
     test_arm_simple
     test_arm_simple_sum
+    test_arm_primus
     test_arm_simple_inline
     test_arm_simple_cegis
     test_arm_simple_compiled
diff --git a/plugin/lib/vibes_plugin_parameters.ml b/plugin/lib/vibes_plugin_parameters.ml
index c9ae1e21..135ad1b6 100644
--- a/plugin/lib/vibes_plugin_parameters.ml
+++ b/plugin/lib/vibes_plugin_parameters.ml
@@ -87,15 +87,20 @@ let validate_patch_name (obj : Json.t) : (string, error) Stdlib.result =
    into a [Cabs.definition] *)
 let validate_patch_code (nm : string) (obj : Json.t)
   : (Vibes_config.patch_code, error) Stdlib.result =
-  match Json.Util.member "patch-code" obj, Json.Util.member "asm-code" obj with
-  | `String s, `Null ->
-    (match Parse_c.parse_c_patch s with
-     | Ok code -> Ok (Vibes_config.CCode code)
-     | Error msg -> Error (Errors.Invalid_patch_code msg))
-  | `Null, `String s -> Ok (Vibes_config.ASMCode s)
-  | `String s, `String s' -> Error
+  match Json.Util.member "patch-code" obj,
+        Json.Util.member "asm-code" obj,
+        Json.Util.member "lisp-code" obj  with
+  | `String s, `Null, `Null ->
+          (match Parse_c.parse_c_patch s with
+          | Ok code -> Ok (Vibes_config.CCode code)
+          | Error msg -> Error (Errors.Invalid_patch_code msg))
+  | `Null, `String s, `Null -> Ok (Vibes_config.ASMCode s)
+  | `Null, `Null, `String s -> Ok (Vibes_config.PrimusCode s)
+  | `String s, `String s', _
+  |  _, `String s', `String s
+  | `String s,   _, `String s' -> Error
       (Errors.Invalid_patch_code "Specified both assembly and C code in patch")
-  | _, _ -> Err.fail Errors.Missing_patch_code
+  | _, _, _ -> Err.fail Errors.Missing_patch_code
 
 (* Extract the patch point field and parse the hex string into a bitvector, or
    error. *)
diff --git a/resources/exes/arm-simple-primus/Makefile b/resources/exes/arm-simple-primus/Makefile
new file mode 100644
index 00000000..c9c8a24a
--- /dev/null
+++ b/resources/exes/arm-simple-primus/Makefile
@@ -0,0 +1,107 @@
+SRC := main.c
+
+PROG := main
+PATCHED_PROG := main.patched
+
+REF_PROG := main.reference
+PATCHED_REF_PROG := main.patched.reference
+
+PATCHED_PROG_FOR_TESTING := test.patched.by.vibes
+
+
+#####################################################
+# DEFAULT
+#####################################################
+
+.DEFAULT_GOAL := all
+all: clean build patch
+
+
+#####################################################
+# BUILD
+#####################################################
+
+build: $(PROG)
+$(PROG): $(SRC)
+	arm-linux-gnueabi-gcc -marm -o $@ $<
+
+
+#####################################################
+# CLEAN
+#####################################################
+
+.PHONY: clean
+clean:
+	rm -rf $(OBJ) $(PROG) $(PATCHED_PROG) $(PATCHED_PROG_FOR_TESTING)
+
+
+#####################################################
+# PATCH
+#####################################################
+
+$(PATCHED_PROG): $(PROG)
+	bap vibes $(PROG) \
+                --config=config.json \
+				--primus-lisp-load=patch \
+                -o $(PATCHED_PROG) \
+                --verbose
+	chmod +x $(PATCHED_PROG)
+
+patch: $(PATCHED_PROG)
+
+
+#####################################################
+# PATCH THE REFERENCE EXECUTABLE
+#####################################################
+
+$(PATCHED_PROG_FOR_TESTING): $(REF_PROG)
+	bap vibes $(REF_PROG) \
+                --config=config.json \
+				--primus-lisp-load=patch \
+                -o $(PATCHED_PROG_FOR_TESTING) \
+                --verbose
+	chmod +x $(PATCHED_PROG_FOR_TESTING)
+
+patch.reference: $(PATCHED_PROG_FOR_TESTING)
+
+
+#####################################################
+# CREATE REFERENCE FILES
+#####################################################
+
+$(REF_PROG):
+	$(MAKE) $(PROG)
+	cp $(PROG) $(REF_PROG)
+
+$(PATCHED_REF_PROG):
+	$(MAKE) patch.reference
+	cp $(PATCHED_PROG_FOR_TESTING) $(PATCHED_REF_PROG)
+
+reference: 
+	rm -rf $(REF_PROG) $(PATCHED_REF_PROG)
+	$(MAKE) $(REF_PROG)
+	$(MAKE) $(PATCHED_REF_PROG)
+
+
+#####################################################
+# RUN
+#####################################################
+
+.PHONY: run.orig
+run.orig: $(PROG)
+	-QEMU_LD_PREFIX=/usr/arm-linux-gnueabi qemu-arm $(PROG)
+
+.PHONY: run.patched
+run.patched: $(PATCHED_PROG)
+	-QEMU_LD_PREFIX=/usr/arm-linux-gnueabi qemu-arm $(PATCHED_PROG)
+
+.PHONY: run.ref
+run.ref: $(REF_PROG)
+	-QEMU_LD_PREFIX=/usr/arm-linux-gnueabi qemu-arm $(REF_PROG)
+
+.PHONY: run.patched-ref
+run.patched-ref: $(PATCHED_REF_PROG)
+	-QEMU_LD_PREFIX=/usr/arm-linux-gnueabi qemu-arm $(PATCHED_REF_PROG)
+
+.PHONY: run.test
+run.test: run.orig run.patched
diff --git a/resources/exes/arm-simple-primus/README.md b/resources/exes/arm-simple-primus/README.md
new file mode 100644
index 00000000..00168e8e
--- /dev/null
+++ b/resources/exes/arm-simple-primus/README.md
@@ -0,0 +1,31 @@
+# ARM Simple Primus
+
+Testing the primus code specification
+
+To clean, build, and patch:
+
+    make
+
+To build:
+
+    make build
+
+To patch:
+
+    make patch
+
+To run the executable and the patched executable (in qemu):
+
+    make run.test
+
+To create reference versions of the executables:
+
+    make reference
+
+To patch the reference executable:
+
+    make patch.reference
+
+To clean:
+
+    make clean
diff --git a/resources/exes/arm-simple-primus/config.json b/resources/exes/arm-simple-primus/config.json
new file mode 100644
index 00000000..5ebd5cd3
--- /dev/null
+++ b/resources/exes/arm-simple-primus/config.json
@@ -0,0 +1,25 @@
+{
+  "max-tries": 15,
+  "wp-params": {
+    "func": "main",
+    "postcond" : "(assert (= (bvadd R0_mod #x00000002) R0_orig))"
+  },
+  "patches" : [
+    {"patch-name" : "ret-3",
+     "lisp-code" : "ret-3",
+     "patch-point" : "0x103d4",
+     "patch-size" : 8,
+     "patch-vars": [
+         {"name": "retvar",
+	  "at-entry": {
+              "stored-in": "register",
+              "register": "R0"
+          },
+          "at-exit": {
+              "stored-in": "register",
+	      "register": "R12"
+          }}
+     ]
+    }
+  ]
+}
diff --git a/resources/exes/arm-simple-primus/main.c b/resources/exes/arm-simple-primus/main.c
new file mode 100644
index 00000000..98941446
--- /dev/null
+++ b/resources/exes/arm-simple-primus/main.c
@@ -0,0 +1,4 @@
+
+int main() {
+  return 5;
+}
diff --git a/resources/exes/arm-simple-primus/main.patched.reference b/resources/exes/arm-simple-primus/main.patched.reference
new file mode 100755
index 00000000..b1da377c
Binary files /dev/null and b/resources/exes/arm-simple-primus/main.patched.reference differ
diff --git a/resources/exes/arm-simple-primus/main.reference b/resources/exes/arm-simple-primus/main.reference
new file mode 100755
index 00000000..a261444a
Binary files /dev/null and b/resources/exes/arm-simple-primus/main.reference differ
diff --git a/resources/exes/arm-simple-primus/main.s b/resources/exes/arm-simple-primus/main.s
new file mode 100644
index 00000000..94617049
--- /dev/null
+++ b/resources/exes/arm-simple-primus/main.s
@@ -0,0 +1,33 @@
+	.arch armv5t
+	.eabi_attribute 20, 1
+	.eabi_attribute 21, 1
+	.eabi_attribute 23, 3
+	.eabi_attribute 24, 1
+	.eabi_attribute 25, 1
+	.eabi_attribute 26, 2
+	.eabi_attribute 30, 6
+	.eabi_attribute 34, 0
+	.eabi_attribute 18, 4
+	.file	"main.c"
+	.text
+	.align	2
+	.global	main
+	.syntax unified
+	.arm
+	.fpu softvfp
+	.type	main, %function
+main:
+	@ args = 0, pretend = 0, frame = 0
+	@ frame_needed = 1, uses_anonymous_args = 0
+	@ link register save eliminated.
+	str	fp, [sp, #-4]!
+	add	fp, sp, #0
+	mov	r3, #5
+	mov	r0, r3
+	add	sp, fp, #0
+	@ sp needed
+	ldr	fp, [sp], #4
+	bx	lr
+	.size	main, .-main
+	.ident	"GCC: (Ubuntu/Linaro 7.5.0-3ubuntu1~18.04) 7.5.0"
+	.section	.note.GNU-stack,"",%progbits
diff --git a/resources/exes/arm-simple-primus/patch.lisp b/resources/exes/arm-simple-primus/patch.lisp
new file mode 100644
index 00000000..e5531601
--- /dev/null
+++ b/resources/exes/arm-simple-primus/patch.lisp
@@ -0,0 +1,3 @@
+(defun ret-3 ()
+    (set R0 3)
+)