kind2-mc/kind2

Simplification of to-real

Closed this issue · 0 comments

Seems that some case is missing:

diff --git a/src/simplify.ml b/src/simplify.ml
index 6f2e73ec..fc43b180 100644
--- a/src/simplify.ml
+++ b/src/simplify.ml
@@ -1909,6 +1909,8 @@ let rec simplify_term_node default_of_var uf_defs model fterm args =
                 (* New polynomial with integer value as atom *)
                 Dec (Decimal.zero, [Decimal.one, [Term.mk_to_int (term_of_nf a)]])
 
+              | [Dec _ as a] -> a
+
               (* Conversion is only unary *)
               | _ -> assert false