From 655166b867b521451242256ab9b612d1b34f4117 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Jul 2020 16:34:09 -0700
Subject: [PATCH] randomize generation of 'some value' for user sorts. #4557

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/value_factory.cpp   | 13 ++++++++++++-
 src/smt/smt_model_checker.cpp |  1 +
 src/smt/smt_model_finder.cpp  |  2 +-
 3 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/model/value_factory.cpp b/src/model/value_factory.cpp
index 45a6b2429..050e15c67 100644
--- a/src/model/value_factory.cpp
+++ b/src/model/value_factory.cpp
@@ -18,6 +18,7 @@ Revision History:
 --*/
 
 #include "model/value_factory.h"
+#include "ast/ast_pp.h"
 
 value_factory::value_factory(ast_manager & m, family_id fid):
     m_manager(m), 
@@ -81,7 +82,17 @@ expr * user_sort_factory::get_some_value(sort * s) {
         m_sort2value_set.find(s, set);
         SASSERT(set != 0);
         SASSERT(!set->m_values.empty());
-        return *(set->m_values.begin());
+        unsigned nv = set->m_values.size();
+        random_gen rand(m_manager.get_num_asts());
+        unsigned n = 1;
+        expr* result = nullptr;
+        for (auto v : set->m_values) {
+            if (0 == (rand() % (n++)))
+                result = v;
+            if (n > 10)
+                break;
+        }
+        return result;
     }
     return simple_factory<unsigned>::get_some_value(s);
 }
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index efaea40e3..44039ba36 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -359,6 +359,7 @@ namespace smt {
                 break;
             model_ref cex;
             m_aux_context->get_model(cex);
+            
             if (!add_instance(q, cex.get(), sks, true)) {
                 break;
             }
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 5b6e4638a..843a0c734 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -958,7 +958,7 @@ namespace smt {
                 ptr_vector<node> need_fresh;
                 for (node * n : m_root_nodes) {
                     SASSERT(n->is_root());
-                    instantiation_set const * s           = n->get_instantiation_set();
+                    instantiation_set const * s = n->get_instantiation_set();
                     TRACE("model_finder", s->display(tout););
                     obj_map<expr, unsigned> const & elems = s->get_elems();
                     if (elems.empty()) {