From 4f184b6aa9d42da757fba16cf7e5dd7882ed54aa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jul 2021 19:20:35 +0200 Subject: [PATCH] fix #5376 --- src/smt/smt_model_checker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 4598a9a3f..9569ec3a8 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -218,7 +218,7 @@ namespace smt { TRACE("model_checker", tout << "Got some value " << sk_value << "\n";); if (use_inv) { - unsigned sk_term_gen; + unsigned sk_term_gen = 0; expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen); if (sk_term != nullptr) { TRACE("model_checker", tout << "Found inverse " << mk_pp(sk_term, m) << "\n";);