summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp_lib.lem3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index c84588ef..8b390b8a 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -118,6 +118,9 @@ let rec most_significant v =
match detaint v with
| V_vector _ _ (v::vs) -> v
| V_vector_sparse _ _ _ _ _ -> most_significant (fill_in_sparse v)
+ | V_lit (L_aux L_one _) -> v
+ | V_lit (L_aux L_zero _) -> v
+ | V_lit (L_aux L_undef _) -> v
| V_unknown -> V_unknown
| _ -> Assert_extra.failwith ("most_significant given non-vector " ^ (string_of_value v))
end;;