Merge pull request #1099 from daniel-larraz/certif-get-values

Use get_var_values to get model in certifChecker
kind2-mc · Sep 28, 2024 · a0ce37b · a0ce37b
2 parents fd7e8ab + f3fced0
commit a0ce37b
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/certif/certifChecker.ml b/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 =