summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKathy Gray2014-12-09 22:33:14 +0000
committerKathy Gray2014-12-09 22:33:14 +0000
commit2b62a85d0d73f4293b27a26f0d57c171168ff68b (patch)
tree61b977532a3d3d2e72f5aeddc7a59d3d2b478990 /src
parentfe3f10440010c7626f3cec8da4ed45599ec27f9a (diff)
Add quite important detaint
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp_lib.lem2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 890372f2..033057c3 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -79,7 +79,7 @@ let is_unknown v = match v with
| _ -> false
end
-let has_unknown v = match v with
+let has_unknown v = match detaint v with
| V_vector _ _ vs -> List.any is_unknown vs
end