diff options
Diffstat (limited to 'src/constraint.ml')
| -rw-r--r-- | src/constraint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/constraint.ml b/src/constraint.ml index d8241e1d..1a4129ff 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -181,7 +181,7 @@ let to_smt l vars constr = | Nexp_minus (nexp1, nexp2) -> sfun "-" [smt_nexp nexp1; smt_nexp nexp2] | Nexp_exp nexp -> begin match nexp_simp nexp with - | Nexp_aux (Nexp_constant c, _) when Big_int.greater c Big_int.zero -> + | Nexp_aux (Nexp_constant c, _) when Big_int.greater_equal c Big_int.zero -> Atom (Big_int.to_string (Big_int.pow_int_positive 2 (Big_int.to_int c))) | nexp when !opt_solver.uninterpret_power -> sfun "sailexp" [smt_nexp nexp] | nexp -> sfun "^" [Atom "2"; smt_nexp nexp] |