diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg
index 302616ce0..d1e2e567d 100644
--- a/src/params/smt_parallel_params.pyg
+++ b/src/params/smt_parallel_params.pyg
@@ -24,5 +24,5 @@ def_module_params('smt_parallel',
                         ('inprocessing_delay', UINT, 0, 'number of undef before invoking simplification'),
                         ('param_tuning', BOOL, False, 'whether to tune params online during solving'),
                         ('enable_parallel_smt', BOOL, True, 'whether to run the parallel solver (set to FALSE to test param tuning only)'),
-                        ('tunable_params', STRING, '', 'comma-separated key=value list for online param tuning, e.g. smt.arith.nl.horner=false,smt.arith.nl.delay=8'),
+                        ('tunable_params', STRING, '', 'comma-separated key=value list for online param tuning, e.g. \"smt.arith.nl.horner=false,smt.arith.nl.delay=8\"')
               ))
\ No newline at end of file
diff --git a/src/util/search_tree.h b/src/util/search_tree.h
index 2b9a41b59..7c51d138d 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -211,7 +211,7 @@ namespace search_tree {
                 if (lit != lit_l && !res.contains(lit))
                     res.push_back(lit);
             for (auto const &lit : core_r)
-                if (lit != lit_l && !res.contains(lit))
+                if (lit != lit_r && !res.contains(lit))
                     res.push_back(lit);
             return res;
         }