introduce fresh term when none is available in context or model to fix #2456

NikolajBjorner · NikolajBjorner · commit 01920abf46a2 · 2019-08-04T11:57:30.000-07:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git 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));

Original file line number	Diff line number	Diff line change
`@@ -81,8 +81,8 @@ namespace smt {`
`81`	`81`	`expr * model_checker::get_type_compatible_term(expr * val) {`
`82`	`82`	`for (auto const& kv : m_value2expr) {`
`83`	`83`	`if (m.get_sort(kv.m_key) == m.get_sort(val) &&`
`84`		`- !contains_model_value(kv.m_key)) {`
`85`		`- return kv.m_key;`
	`84`	`+ !contains_model_value(kv.m_value)) {`
	`85`	`+ return kv.m_value;`
`86`	`86`	`}`
`87`	`87`	`}`
`88`	`88`	`app* fresh_term = m.mk_fresh_const("sk", m.get_sort(val));`