diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg
index ad7a22675..bf5bd181a 100644
--- a/src/tactic/sls/sls_params.pyg
+++ b/src/tactic/sls/sls_params.pyg
@@ -19,7 +19,7 @@ def_module_params('sls',
 						('restart_base', UINT, 100, 'base restart interval given by moves per run'),
 						('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'),
 						('early_prune', BOOL, 1, 'use early pruning for score prediction'),
-						('random_offset', BOOL, 1, 'use random offset vor candidate evaluation'),
+						('random_offset', BOOL, 1, 'use random offset for candidate evaluation'),
 						('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
 						('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
 						('random_seed', UINT, 0, 'random seed')
diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h
index 4356bcc9b..d58f94af2 100644
--- a/src/tactic/sls/sls_tracker.h
+++ b/src/tactic/sls/sls_tracker.h
@@ -831,7 +831,9 @@ public:
             app * a = to_app(n);
             SASSERT(a->get_num_args() == 1);
             expr * child = a->get_arg(0);
-            if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF.
+            // Precondition: Assertion set is in NNF.
+            // Also: careful about the unsat assertion scaling further down.
+            if (m_manager.is_and(child) || m_manager.is_or(child)) 
                 NOT_IMPLEMENTED_YET();
             res = score_bool(child, true);
         }