Use get_var_values to get model in certifChecker

Previously, models were retrieved using get-model, which could cause issues when
minimizing invariants for Lustre models with arrays encoded as values of
an uninterpreted sort, FArray, with arity 2.
If the Lustre model includes arrays for two different element types (e.g.,
FArray Int Bool and FArray Int Int), Z3 returns models where the universes for
FArray Int Bool and FArray Int Int may contain constants with
the same name (e.g. FArray!val!3).

src/certif/certifChecker.ml

@@ -723,7 +723,12 @@ let rec cherry_pick solver trans
        (* Not enough invariants *)
 
        (* Get the full model *)
-       let model = SMTSolver.get_model solver in
+       let model =
+         SMTSolver.get_var_values
+          solver
+          (TransSys.get_state_var_bounds trans)
+          (TransSys.vars_of_bounds trans Numeral.zero Numeral.one)
+       in
 
        (* Evaluation function. *)
        let eval term =