From aced115b7014d1571eb8ce5a5b38af5e0e059dcc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 11 Nov 2020 17:35:09 -0800
Subject: [PATCH] model validation

---
 src/sat/smt/euf_solver.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 9b43810a3..78d428edb 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -144,6 +144,7 @@ namespace euf {
         void dependencies2values(deps_t& deps, model_ref& mdl);
         void collect_dependencies(deps_t& deps);
         void values2model(deps_t const& deps, model_ref& mdl);
+        void validate_model(model& mdl);
 
         // solving
         void propagate_literals();