Make nexp simplification a little smarter

(should really make the Lem pretty printer use the solver properly,
but this is a useful stopgap)

1 files changed, 7 insertions, 0 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index f7574b9d..968cb320 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -244,6 +244,13 @@ and nexp_simp_aux = function
          when Big_int.equal c1 (Big_int.negate c2) -> n
        | _, _ -> Nexp_minus (n1, n2)
      end
+  | Nexp_neg n ->
+     begin
+       let (Nexp_aux (n_simp, _) as n) = nexp_simp n in
+       match n_simp with
+       | Nexp_constant c -> Nexp_constant (Big_int.negate c)
+       | _ -> Nexp_neg n
+     end
   | Nexp_app (Id_aux (Id "div",_) as id,[n1;n2]) ->
      begin
        let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in