summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-04-26 17:20:20 +0100
committerAlasdair Armstrong2019-04-26 17:20:20 +0100
commit094c8e254abde44d45097aca7a36203704fe2ef4 (patch)
treec38fa2db7f554209be9ec0c11f87813c0b028d52 /lib
parent383bf94704813ad3f417b6eaf59d329388ff5af6 (diff)
Fix some broken interpreter tests
Diffstat (limited to 'lib')
-rw-r--r--lib/smt.sail3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/smt.sail b/lib/smt.sail
index 4d250bef..f58c008f 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -6,6 +6,7 @@ $define _SMT
/*! Euclidean division */
val ediv_int = {
ocaml: "quotient",
+ interpreter: "quotient",
lem: "integerDiv",
c: "ediv_int",
coq: "ediv_with_eq"
@@ -13,6 +14,7 @@ val ediv_int = {
val emod_int = {
ocaml: "modulus",
+ interpreter: "modulus",
lem: "integerMod",
c: "emod_int",
coq: "emod_with_eq"
@@ -20,6 +22,7 @@ val emod_int = {
val abs_int = {
ocaml: "abs_int",
+ interpreter: "abs_int",
lem: "abs_int",
c: "abs_int",
coq: "abs_with_eq"