From 01920abf46a2558e5cf9f08260547b723a47bdd5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Aug 2019 11:57:30 -0700
Subject: [PATCH] introduce fresh term when none is available in context or
 model to fix #2456

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_model_checker.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index b9e93cac9..539ecf9d7 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -81,8 +81,8 @@ namespace smt {
     expr * model_checker::get_type_compatible_term(expr * val) {
         for (auto const& kv : m_value2expr) {
             if (m.get_sort(kv.m_key) == m.get_sort(val) &&
-                !contains_model_value(kv.m_key)) {
-                return kv.m_key;
+                !contains_model_value(kv.m_value)) {
+                return kv.m_value;
             }
         }
         app* fresh_term = m.mk_fresh_const("sk", m.get_sort(val));