diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index 92d5bb72e..851dc63ec 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -22,6 +22,18 @@ Abstract:
 #include "ast/ast_pp.h"
 #include <iostream>
 
+class dummy_simple_solver : public seq::simple_solver {
+public:
+    dummy_simple_solver() : seq::simple_solver() {}
+    void push() override {}
+    void pop(unsigned n) override {}
+    void assert(expr *constraint) override {}
+    lbool check() override {
+        return l_true;
+    }
+
+};
+
 // test dep_tracker (uint_set) basic operations
 static void test_dep_tracker() {
     std::cout << "test_dep_tracker\n";
@@ -173,7 +185,8 @@ static void test_nielsen_node() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -215,7 +228,8 @@ static void test_nielsen_edge() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -250,7 +264,8 @@ static void test_nielsen_graph_populate() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -289,7 +304,8 @@ static void test_nielsen_subst_apply() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -323,7 +339,8 @@ static void test_nielsen_graph_reset() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -346,7 +363,8 @@ static void test_nielsen_expansion() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -395,7 +413,8 @@ static void test_run_idx() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
     SASSERT(ng.run_idx() == 0);
 
     ng.inc_run_idx();
@@ -415,7 +434,8 @@ static void test_multiple_memberships() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
 
@@ -451,7 +471,8 @@ static void test_backedge() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -474,7 +495,8 @@ static void test_eq_split_basic() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -504,7 +526,8 @@ static void test_eq_split_solve_sat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -526,7 +549,7 @@ static void test_eq_split_solve_unsat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -548,7 +571,8 @@ static void test_eq_split_same_var_det() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* a = sg.mk_char('A');
@@ -570,7 +594,7 @@ static void test_eq_split_commutation_sat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -592,7 +616,8 @@ static void test_const_nielsen_char_var() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -615,7 +640,8 @@ static void test_const_nielsen_var_char() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* b = sg.mk_char('B');
@@ -640,7 +666,8 @@ static void test_const_nielsen_solve_sat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -661,7 +688,8 @@ static void test_const_nielsen_solve_unsat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -683,7 +711,8 @@ static void test_const_nielsen_priority_over_eq_split() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -710,7 +739,8 @@ static void test_const_nielsen_not_applicable_both_vars() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -736,7 +766,8 @@ static void test_const_nielsen_multi_char_solve() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -764,7 +795,8 @@ static void test_regex_char_split_basic() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
 
@@ -799,7 +831,8 @@ static void test_regex_char_split_solve_sat() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
 
@@ -823,7 +856,8 @@ static void test_regex_char_split_solve_multi_char() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
 
@@ -850,7 +884,8 @@ static void test_regex_char_split_union() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
 
@@ -878,7 +913,8 @@ static void test_regex_char_split_star_sat() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
 
@@ -903,7 +939,8 @@ static void test_regex_char_split_concat_str() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -932,7 +969,8 @@ static void test_regex_char_split_with_eq() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -959,7 +997,8 @@ static void test_regex_char_split_ground_skip() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('A');
 
@@ -987,7 +1026,8 @@ static void test_var_nielsen_basic() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1010,7 +1050,8 @@ static void test_var_nielsen_same_var_det() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* a = sg.mk_char('A');
@@ -1032,7 +1073,8 @@ static void test_var_nielsen_not_applicable_char() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1054,7 +1096,8 @@ static void test_var_nielsen_solve_sat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1076,7 +1119,8 @@ static void test_var_nielsen_solve_unsat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1098,7 +1142,8 @@ static void test_var_nielsen_commutation_sat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1120,7 +1165,7 @@ static void test_var_nielsen_priority() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1145,7 +1190,7 @@ static void test_generate_extensions_det_priority() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1169,7 +1214,7 @@ static void test_generate_extensions_no_applicable() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -1193,7 +1238,7 @@ static void test_generate_extensions_regex_only() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     // Build regex to_re("A")
@@ -1223,7 +1268,7 @@ static void test_generate_extensions_mixed_det_first() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1257,7 +1302,7 @@ static void test_solve_empty_graph() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     SASSERT(!ng.root());
     auto result = ng.solve();
     SASSERT(result == seq::nielsen_graph::search_result::sat);
@@ -1271,7 +1316,7 @@ static void test_solve_trivially_satisfied() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     ng.add_str_eq(x, x);
     auto result = ng.solve();
@@ -1286,7 +1331,7 @@ static void test_solve_node_status_unsat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     // A = B is an immediate conflict
@@ -1308,7 +1353,7 @@ static void test_solve_conflict_deps() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     // Add two constraints: A = B (unsat) and a dummy x = x
@@ -1372,7 +1417,7 @@ static void test_explain_conflict_single_eq() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     // eq[0]: A = B (conflict)
@@ -1397,7 +1442,7 @@ static void test_explain_conflict_multi_eq() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* x = sg.mk_var(symbol("x"));
@@ -1428,7 +1473,7 @@ static void test_solve_node_extended_flag() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
     euf::snode* xy = sg.mk_concat(x, y);
@@ -1455,7 +1500,7 @@ static void test_solve_mixed_eq_mem_sat() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
     euf::snode* a = sg.mk_char('A');
@@ -1484,7 +1529,7 @@ static void test_solve_children_failed_reason() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
     euf::snode* a = sg.mk_char('A');
@@ -1506,7 +1551,7 @@ static void test_solve_eval_idx_tracking() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* a = sg.mk_char('A');
     // x = A·x would be infinite without depth bound, but
@@ -1538,7 +1583,8 @@ static void test_simplify_prefix_cancel() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;   
+    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* x = sg.mk_var(symbol("x"));
@@ -1568,7 +1614,7 @@ static void test_simplify_symbol_clash() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* x = sg.mk_var(symbol("x"));
@@ -1596,7 +1642,7 @@ static void test_simplify_empty_propagation() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* e = sg.mk_empty();
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1619,7 +1665,7 @@ static void test_simplify_empty_vs_char() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* e = sg.mk_empty();
     euf::snode* a = sg.mk_char('A');
 
@@ -1641,7 +1687,7 @@ static void test_simplify_multi_pass_clash() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* c = sg.mk_char('C');
@@ -1667,7 +1713,7 @@ static void test_simplify_trivial_removal() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
     euf::snode* e = sg.mk_empty();
@@ -1690,7 +1736,7 @@ static void test_simplify_all_trivial_satisfied() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* e = sg.mk_empty();
 
@@ -1712,7 +1758,7 @@ static void test_simplify_regex_infeasible() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* e = sg.mk_empty();
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -1739,7 +1785,7 @@ static void test_simplify_nullable_removal() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* e = sg.mk_empty();
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -1767,7 +1813,7 @@ static void test_simplify_brzozowski_sat() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* e = sg.mk_empty();
 
@@ -1793,7 +1839,7 @@ static void test_simplify_multiple_eqs() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -1831,7 +1877,7 @@ static void test_det_cancel_child_eq() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -1853,7 +1899,7 @@ static void test_const_nielsen_child_substitutions() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* x = sg.mk_var(symbol("x"));
@@ -1889,7 +1935,7 @@ static void test_var_nielsen_substitution_types() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
 
@@ -1919,7 +1965,7 @@ static void test_explain_conflict_mem_only() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* e = sg.mk_empty();
 
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -1949,7 +1995,7 @@ static void test_explain_conflict_mixed_eq_mem() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
     euf::snode* e = sg.mk_empty();
@@ -1989,7 +2035,7 @@ static void test_subsumption_pruning_unsat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
 
@@ -2011,7 +2057,7 @@ static void test_subsumption_reason_set() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
     euf::snode* a = sg.mk_char('A');
@@ -2061,7 +2107,7 @@ static void test_length_constraints_basic() {
     euf::snode* lhs = sg.mk_concat(x, y);
     euf::snode* rhs = sg.mk_concat(a, b);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_eq(lhs, rhs);
 
     vector<seq::length_constraint> constraints;
@@ -2096,7 +2142,7 @@ static void test_length_constraints_trivial_skip() {
     euf::snode* x = sg.mk_var(symbol("x"));
 
     // trivial equation: x = x (same snode)
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_eq(x, x);
 
     vector<seq::length_constraint> constraints;
@@ -2115,7 +2161,7 @@ static void test_length_constraints_empty() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     vector<seq::length_constraint> constraints;
     ng.generate_length_constraints(constraints);
@@ -2144,7 +2190,7 @@ static void test_length_constraints_concat_chain() {
     euf::snode* lhs = sg.mk_concat(sg.mk_concat(x, y), z);
     euf::snode* rhs = sg.mk_concat(sg.mk_concat(a, b), c);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_eq(lhs, rhs);
 
     vector<seq::length_constraint> constraints;
@@ -2172,7 +2218,7 @@ static void test_length_constraints_multi_eq() {
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_eq(x, a);           // x = A
     ng.add_str_eq(y, b);           // y = B
 
@@ -2205,7 +2251,7 @@ static void test_length_constraints_shared_var() {
     euf::snode* lhs = sg.mk_concat(x, a);
     euf::snode* rhs = sg.mk_concat(a, x);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_eq(lhs, rhs);
 
     vector<seq::length_constraint> constraints;
@@ -2230,7 +2276,7 @@ static void test_length_constraints_deps() {
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* a = sg.mk_char('A');
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_eq(x, a);  // eq index 0
 
     vector<seq::length_constraint> constraints;
@@ -2260,7 +2306,7 @@ static void test_length_constraints_empty_side() {
     euf::snode* e = sg.mk_empty();
 
     // x = ε
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_eq(x, e);
 
     vector<seq::length_constraint> constraints;
@@ -2294,7 +2340,7 @@ static void test_length_kind_tagging() {
     euf::snode* a = sg.mk_char('A');
 
     // equation: x = a (one eq + one nonneg)
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_eq(x, a);
 
     // membership: y in to_re("AB") (bounds + nonneg)
@@ -2352,7 +2398,7 @@ static void test_power_epsilon_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* a = sg.mk_char('A');
@@ -2376,7 +2422,7 @@ static void test_num_cmp_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -2401,7 +2447,7 @@ static void test_star_intr_no_backedge() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -2434,7 +2480,7 @@ static void test_star_intr_with_backedge() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     expr_ref ch_a(seq.str.mk_char('A'), m);
@@ -2473,7 +2519,7 @@ static void test_gpower_intr_self_cycle() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* a1 = sg.mk_char('A');
@@ -2501,7 +2547,7 @@ static void test_gpower_intr_no_cycle() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -2531,7 +2577,7 @@ static void test_regex_var_split_basic() {
     seq_util seq(m);
     sort_ref str_sort(seq.str.mk_string_sort(), m);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
 
@@ -2566,7 +2612,7 @@ static void test_power_split_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -2592,7 +2638,7 @@ static void test_var_num_unwinding_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -2615,7 +2661,7 @@ static void test_const_num_unwinding_no_power() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('A');
     euf::snode* b = sg.mk_char('B');
@@ -2642,7 +2688,7 @@ static void test_priority_chain_order() {
     {
         euf::egraph eg(m);
         euf::sgraph sg(m, eg);
-        seq::nielsen_graph ng(sg);
+        dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
         euf::snode* x = sg.mk_var(symbol("x"));
         euf::snode* y = sg.mk_var(symbol("y"));
@@ -2659,7 +2705,7 @@ static void test_priority_chain_order() {
     {
         euf::egraph eg(m);
         euf::sgraph sg(m, eg);
-        seq::nielsen_graph ng(sg);
+        dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
         euf::snode* x = sg.mk_var(symbol("x"));
         euf::snode* y = sg.mk_var(symbol("y"));
@@ -2675,7 +2721,7 @@ static void test_priority_chain_order() {
     {
         euf::egraph eg(m);
         euf::sgraph sg(m, eg);
-        seq::nielsen_graph ng(sg);
+        dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
         euf::snode* a = sg.mk_char('A');
         euf::snode* y = sg.mk_var(symbol("y"));
@@ -2696,7 +2742,7 @@ static void test_gpower_intr_solve_sat() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* a1 = sg.mk_char('A');
@@ -2734,7 +2780,7 @@ static void test_parikh_exact_length() {
     expr_ref to_re_ab(seq.re.mk_to_re(ab), m);
     euf::snode* regex = sg.mk(to_re_ab);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -2781,7 +2827,7 @@ static void test_parikh_star_unbounded() {
     expr_ref re_star(seq.re.mk_star(to_re_a), m);
     euf::snode* regex = sg.mk(re_star);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -2836,7 +2882,7 @@ static void test_parikh_union_interval() {
     expr_ref re_union(seq.re.mk_union(to_re_ab, to_re_cde), m);
     euf::snode* regex = sg.mk(re_union);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -2875,7 +2921,7 @@ static void test_parikh_loop_bounded() {
     expr_ref re_loop(seq.re.mk_loop(to_re_a, 3, 5), m);
     euf::snode* regex = sg.mk(re_loop);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -2911,7 +2957,7 @@ static void test_parikh_empty_regex() {
     expr_ref re_empty(seq.re.mk_empty(seq.re.mk_re(str_sort)), m);
     euf::snode* regex = sg.mk(re_empty);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -2950,7 +2996,7 @@ static void test_parikh_full_char() {
     expr_ref re_range(seq.re.mk_range(unit_a, unit_z), m);
     euf::snode* regex = sg.mk(re_range);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -2986,7 +3032,7 @@ static void test_parikh_mixed_eq_mem() {
     euf::snode* a = sg.mk_char('A');
 
     // equation: x = A
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_eq(x, a);
 
     // membership: y in to_re("BC")
@@ -3034,7 +3080,7 @@ static void test_parikh_full_seq_no_bounds() {
     expr_ref re_all(seq.re.mk_full_seq(str_sort), m);
     euf::snode* regex = sg.mk(re_all);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;
@@ -3071,7 +3117,7 @@ static void test_parikh_dep_tracking() {
     expr_ref to_re_a(seq.re.mk_to_re(unit_a), m);
     euf::snode* regex = sg.mk(to_re_a);
 
-    seq::nielsen_graph ng(sg);
+    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver);
     ng.add_str_mem(x, regex);
 
     vector<seq::length_constraint> constraints;