randomize generation of 'some value' for user sorts. #4557

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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);
 }

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;
             }