fix: Add missing model for to_int coercion (#221)

src/model/real.ml

@@ -92,6 +92,7 @@ let builtins ~eval env (cst : Dolmen.Std.Expr.Term.Const.t) =
   | B.Modulo_f `Real -> op2 ~cst mod_f
   | B.Is_rat `Real -> Some (Bool.mk true)
   | B.Floor `Real -> op1 ~cst floor
+  | B.Floor_to_int `Real -> Some (fun1 ~cst (fun x -> Int.mk (Int.floor x)))
   | B.Ceiling `Real -> op1 ~cst ceil
   | B.Truncate `Real -> op1 ~cst truncate
   | B.Round `Real -> op1 ~cst round

tests/model/coercion/dune

@@ -33,4 +33,36 @@
   (action (diff int_to_real.expected int_to_real.full)))
 
 
+; Test for real_to_int.smt2
+; Incremental test
+
+(rule
+   (target  real_to_int.incremental)
+   (deps    (:response real_to_int.rsmt2) (:input real_to_int.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff real_to_int.expected real_to_int.incremental)))
+
+; Full mode test
+
+(rule
+   (target  real_to_int.full)
+   (deps    (:response real_to_int.rsmt2) (:input real_to_int.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff real_to_int.expected real_to_int.full)))
+
+
 ; Auto-generated part end

tests/model/coercion/real_to_int.rsmt2

@@ -0,0 +1,4 @@
+sat
+(
+  (define-fun x () Real 2.2)
+)

tests/model/coercion/real_to_int.smt2

@@ -0,0 +1,6 @@
+(set-option :produce-models)
+(set-logic QF_LIRA)
+(declare-const x Real)
+(assert (= (to_int x) 2))
+(check-sat)
+(get-model)