From f3fced0b3277ec9cb716df46186828719a3b354f Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Fri, 27 Sep 2024 16:52:25 -0500 Subject: [PATCH] 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 | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/certif/certifChecker.ml b/src/certif/certifChecker.ml index 477c3c2db..2a2b6291e 100644 --- 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 =