diff --git a/backend/cn/lib/solver.ml b/backend/cn/lib/solver.ml index 56a564282..54e047681 100644 --- a/backend/cn/lib/solver.ml +++ b/backend/cn/lib/solver.ml @@ -992,18 +992,17 @@ let rec translate_term s iterm = translate_term s (divisible_ (addr, t.align) loc) (* Maps *) | MapConst (bt, e1) -> - begin match IT.get_term e1 with - (* This is a work-around for the fact the CVC5 only supports `const` on - value, not vairables (see #11485 in the CVC5 repo). Until this is - fixed, with translate `MapConst Default` as just `Default`. Hopefully, - this is OK, as we are getting a weaker term (i.e., we can't assume that - all elements of the array are the same, but they might be). *) - | Const (Default t) -> default (BT.make_map_bt bt t) - | _ -> - let kt = translate_base_type bt in - let vt = translate_base_type (IT.get_bt e1) in - SMT.arr_const kt vt (translate_term s e1) - end + (match IT.get_term e1 with + (* This is a work-around for the fact the CVC5 only supports `const` on + value, not vairables (see #11485 in the CVC5 repo). Until this is + fixed, with translate `MapConst Default` as just `Default`. Hopefully, + this is OK, as we are getting a weaker term (i.e., we can't assume that + all elements of the array are the same, but they might be). *) + | Const (Default t) -> default (BT.make_map_bt bt t) + | _ -> + let kt = translate_base_type bt in + let vt = translate_base_type (IT.get_bt e1) in + SMT.arr_const kt vt (translate_term s e1)) | MapSet (mp, k, v) -> SMT.arr_store (translate_term s mp) (translate_term s k) (translate_term s v) | MapGet (mp, k) -> SMT.arr_select (translate_term s mp) (translate_term s k)