[sledge] Translate __llair_choice intrinsic to nondet

Summary:
Currently __llair_choice is left undefined, and so executed as skip.
This has the correct behavior, but makes it hard to distinguish from
calls to unintentionally-undefined procedures.

Reviewed By: ngorogiannis

Differential Revision: D24989068

fbshipit-source-id: f62981857

sledge/cli/frontend.ml

@@ -1013,6 +1013,10 @@ let xlate_instr :
       | Some intrinsic -> inline_or_move (intrinsic x)
       | None -> (
         match String.split_on_char fname ~by:'.' with
+        | ["__llair_choice"] ->
+            let reg = xlate_name x instr in
+            let msg = "__llair_choice" in
+            emit_inst (Inst.nondet ~reg:(Some reg) ~msg ~loc)
         | ["__llair_throw"] ->
             let pre, exc = xlate_value x (Llvm.operand instr 0) in
             emit_term ~prefix:(pop loc @ pre) (Term.throw ~exc ~loc)