From ed81e3b9d80890e83a70b7bf5b8add6e2a5f85fb Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 20 Mar 2015 17:07:32 +0000
Subject: [PATCH] Bugfix for BV-SLS initialization

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/tactic/sls/sls_engine.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp
index 98f659fe0..fc7358f3d 100644
--- a/src/tactic/sls/sls_engine.cpp
+++ b/src/tactic/sls/sls_engine.cpp
@@ -555,8 +555,12 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
         mc = 0;
 }
 
-lbool sls_engine::operator()() {
+lbool sls_engine::operator()() {    
     m_tracker.initialize(m_assertions);
+    m_tracker.reset(m_assertions);
+    if (m_restart_init)
+        m_tracker.randomize(m_assertions);
+
     lbool res = l_undef;
 
     do {