diff --git a/src/test/bit_blaster.cpp b/src/test/bit_blaster.cpp
index 034131eb3d..9798357814 100644
--- a/src/test/bit_blaster.cpp
+++ b/src/test/bit_blaster.cpp
@@ -45,7 +45,7 @@ void display(std::ostream & out, expr_ref_vector & r, bool ll=true) {
 }
 
 static unsigned to_int(model_core & mdl, expr_ref_vector & out) {
-    SASSERT(out.size() <= sizeof(unsigned) * 8);
+    ENSURE(out.size() <= sizeof(unsigned) * 8);
     ast_manager & m = mdl.get_manager();
     model_evaluator eval(mdl);
     expr_ref bit(m);
diff --git a/src/test/diff_logic.cpp b/src/test/diff_logic.cpp
index d8f1ee11c3..ba98f0d144 100644
--- a/src/test/diff_logic.cpp
+++ b/src/test/diff_logic.cpp
@@ -16,7 +16,6 @@ Author:
 Revision History:
 
 --*/
-#ifdef _WINDOWS
 #include "util/rational.h"
 #include "smt/diff_logic.h"
 #include "smt/smt_literal.h"
@@ -169,7 +168,3 @@ void tst_diff_logic() {
     //tst2();
     //tst3();
 }
-#else
-void tst_diff_logic() {
-}
-#endif
diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp
index 942714560b..9d841e421e 100644
--- a/src/test/dl_product_relation.cpp
+++ b/src/test/dl_product_relation.cpp
@@ -351,7 +351,6 @@ namespace datalog {
 
 using namespace datalog;
 
-#ifdef _WINDOWS
 void tst_dl_product_relation() {
     smt_params fparams;
     params_ref params;
@@ -362,7 +361,3 @@ void tst_dl_product_relation() {
     test_finite_product_relation(fparams, params);
     
 }
-#else
-void tst_dl_product_relation() {}
-
-#endif
diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp
index 3e472b838b..3c99edafce 100644
--- a/src/test/dlist.cpp
+++ b/src/test/dlist.cpp
@@ -30,28 +30,28 @@ public:
 // Test the prev() method
 void test_prev() {
     TestNode node(1);
-    SASSERT(node.prev() == &node);
+    ENSURE(node.prev() == &node);
     std::cout << "test_prev passed." << std::endl;
 }
 
 // Test the next() method
 static void test_next() {
     TestNode node(1);
-    SASSERT(node.next() == &node);
+    ENSURE(node.next() == &node);
     std::cout << "test_next passed." << std::endl;
 }
 
 // Test the const prev() method
 static void test_const_prev() {
     const TestNode node(1);
-    SASSERT(node.prev() == &node);
+    ENSURE(node.prev() == &node);
     std::cout << "test_const_prev passed." << std::endl;
 }
 
 // Test the const next() method
 static void test_const_next() {
     const TestNode node(1);
-    SASSERT(node.next() == &node);
+    ENSURE(node.next() == &node);
     std::cout << "test_const_next passed." << std::endl;
 }
 
@@ -59,9 +59,9 @@ static void test_const_next() {
 static void test_init() {
     TestNode node(1);
     node.init(&node);
-    SASSERT(node.next() == &node);
-    SASSERT(node.prev() == &node);
-    SASSERT(node.invariant());
+    ENSURE(node.next() == &node);
+    ENSURE(node.prev() == &node);
+    ENSURE(node.invariant());
     std::cout << "test_init passed." << std::endl;
 }
 
@@ -71,10 +71,10 @@ static void test_pop() {
     TestNode node1(1);
     TestNode::push_to_front(list, &node1);
     [[maybe_unused]] TestNode* popped = TestNode::pop(list);
-    SASSERT(popped == &node1);
-    SASSERT(list == nullptr);
-    SASSERT(popped->next() == popped);
-    SASSERT(popped->prev() == popped);
+    ENSURE(popped == &node1);
+    ENSURE(list == nullptr);
+    ENSURE(popped->next() == popped);
+    ENSURE(popped->prev() == popped);
     std::cout << "test_pop passed." << std::endl;
 }
 
@@ -83,12 +83,12 @@ static void test_insert_after() {
     TestNode node1(1);
     TestNode node2(2);
     node1.insert_after(&node2);
-    SASSERT(node1.next() == &node2);
-    SASSERT(node2.prev() == &node1);
-    SASSERT(node1.prev() == &node2);
-    SASSERT(node2.next() == &node1);
-    SASSERT(node1.invariant());
-    SASSERT(node2.invariant());
+    ENSURE(node1.next() == &node2);
+    ENSURE(node2.prev() == &node1);
+    ENSURE(node1.prev() == &node2);
+    ENSURE(node2.next() == &node1);
+    ENSURE(node1.invariant());
+    ENSURE(node2.invariant());
     std::cout << "test_insert_after passed." << std::endl;
 }
 
@@ -97,12 +97,12 @@ static void test_insert_before() {
     TestNode node1(1);
     TestNode node2(2);
     node1.insert_before(&node2);
-    SASSERT(node1.prev() == &node2);
-    SASSERT(node2.next() == &node1);
-    SASSERT(node1.next() == &node2);
-    SASSERT(node2.prev() == &node1);
-    SASSERT(node1.invariant());
-    SASSERT(node2.invariant());
+    ENSURE(node1.prev() == &node2);
+    ENSURE(node2.next() == &node1);
+    ENSURE(node1.next() == &node2);
+    ENSURE(node2.prev() == &node1);
+    ENSURE(node1.invariant());
+    ENSURE(node2.invariant());
     std::cout << "test_insert_before passed." << std::endl;
 }
 
@@ -115,9 +115,9 @@ static void test_remove_from() {
     TestNode::push_to_front(list, &node1);
     TestNode::push_to_front(list, &node2);
     TestNode::remove_from(list, &node1);
-    SASSERT(list == &node2);
-    SASSERT(node2.next() == &node2);
-    SASSERT(node2.prev() == &node2);
+    ENSURE(list == &node2);
+    ENSURE(node2.next() == &node2);
+    ENSURE(node2.prev() == &node2);
     std::cout << "test_remove_from passed." << std::endl;
 }
 #endif
@@ -127,9 +127,9 @@ static void test_push_to_front() {
     TestNode* list = nullptr;
     TestNode node1(1);
     TestNode::push_to_front(list, &node1);
-    SASSERT(list == &node1);
-    SASSERT(node1.next() == &node1);
-    SASSERT(node1.prev() == &node1);
+    ENSURE(list == &node1);
+    ENSURE(node1.next() == &node1);
+    ENSURE(node1.prev() == &node1);
     std::cout << "test_push_to_front passed." << std::endl;
 }
 
@@ -137,20 +137,20 @@ static void test_push_to_front() {
 static void test_detach() {
     TestNode node(1);
     TestNode::detach(&node);
-    SASSERT(node.next() == &node);
-    SASSERT(node.prev() == &node);
-    SASSERT(node.invariant());
+    ENSURE(node.next() == &node);
+    ENSURE(node.prev() == &node);
+    ENSURE(node.invariant());
     std::cout << "test_detach passed." << std::endl;
 }
 
 // Test the invariant() method
 static void test_invariant() {
     TestNode node1(1);
-    SASSERT(node1.invariant());
+    ENSURE(node1.invariant());
     TestNode node2(2);
     node1.insert_after(&node2);
-    SASSERT(node1.invariant());
-    SASSERT(node2.invariant());
+    ENSURE(node1.invariant());
+    ENSURE(node2.invariant());
     std::cout << "test_invariant passed." << std::endl;
 }
 
@@ -161,10 +161,10 @@ static void test_contains() {
     TestNode node2(2);
     TestNode::push_to_front(list, &node1);
     TestNode::push_to_front(list, &node2);
-    SASSERT(TestNode::contains(list, &node1));
-    SASSERT(TestNode::contains(list, &node2));
+    ENSURE(TestNode::contains(list, &node1));
+    ENSURE(TestNode::contains(list, &node2));
     TestNode node3(3);
-    SASSERT(!TestNode::contains(list, &node3));
+    ENSURE(!TestNode::contains(list, &node3));
     std::cout << "test_contains passed." << std::endl;
 }
 
diff --git a/src/test/egraph.cpp b/src/test/egraph.cpp
index 916d7e18a6..52fe4c6eaa 100644
--- a/src/test/egraph.cpp
+++ b/src/test/egraph.cpp
@@ -116,12 +116,12 @@ static void test3() {
     g.merge(nx,  nz, justifications + 2);
     g.merge(nx,  nu, justifications + 3);
     g.propagate();
-    SASSERT(!g.inconsistent());
+    ENSURE(!g.inconsistent());
     g.merge(nx, ny, justifications + 4);
     std::cout << g << "\n";
     g.propagate();
     std::cout << g << "\n";
-    SASSERT(g.inconsistent());
+    ENSURE(g.inconsistent());
     ptr_vector<int> js;
     g.begin_explain();
     g.explain<int>(js, nullptr);
diff --git a/src/test/euf_arith_plugin.cpp b/src/test/euf_arith_plugin.cpp
index 92535d31dd..596db671b4 100644
--- a/src/test/euf_arith_plugin.cpp
+++ b/src/test/euf_arith_plugin.cpp
@@ -70,7 +70,7 @@ static void test2() {
     TRACE(plugin, tout << "before propagate\n" << g << "\n");
     g.propagate();
     TRACE(plugin, tout << "after propagate\n" << g << "\n");
-    SASSERT(nx->get_root() == ny->get_root());
+    ENSURE(nx->get_root() == ny->get_root());
     g.merge(get_node(g, a, a.mk_add(x, a.mk_add(y, y))), get_node(g, a, a.mk_add(y, x)), nullptr);
     g.propagate();
     std::cout << g << "\n";
diff --git a/src/test/euf_bv_plugin.cpp b/src/test/euf_bv_plugin.cpp
index b213a269c0..7a8722770f 100644
--- a/src/test/euf_bv_plugin.cpp
+++ b/src/test/euf_bv_plugin.cpp
@@ -51,7 +51,7 @@ static void test1() {
     g.propagate();
     TRACE(bv, tout << "after propagate\n" << g << "\n");
     std::cout << g << "\n";
-    SASSERT(nx->get_root() == ny->get_root());
+    ENSURE(nx->get_root() == ny->get_root());
 }
 
 // propagate values down
@@ -70,10 +70,10 @@ static void test2() {
     expr_ref xx(bv.mk_concat(x1, bv.mk_concat(x2, x3)), m);
     g.merge(get_node(g, bv, xx), get_node(g, bv, bv.mk_numeral((1 << 27) + (1 << 17) + (1 << 3), 32)), nullptr);
     g.propagate();
-    SASSERT(get_node(g, bv, x1)->get_root()->interpreted());
-    SASSERT(get_node(g, bv, x2)->get_root()->interpreted());
-    SASSERT(get_node(g, bv, x3)->get_root()->interpreted());
-    SASSERT(get_node(g, bv, x)->get_root()->interpreted());
+    ENSURE(get_node(g, bv, x1)->get_root()->interpreted());
+    ENSURE(get_node(g, bv, x2)->get_root()->interpreted());
+    ENSURE(get_node(g, bv, x3)->get_root()->interpreted());
+    ENSURE(get_node(g, bv, x)->get_root()->interpreted());
 }
 
 
@@ -96,9 +96,9 @@ static void test3() {
     g.merge(get_node(g, bv, x1), get_node(g, bv, bv.mk_numeral(2, 8)), nullptr);
     g.merge(get_node(g, bv, x2), get_node(g, bv, bv.mk_numeral(8, 8)), nullptr);
     g.propagate();
-    SASSERT(get_node(g, bv, bv.mk_concat(x1, x2))->get_root()->interpreted());
-    SASSERT(get_node(g, bv, x1)->get_root()->interpreted());
-    SASSERT(get_node(g, bv, x2)->get_root()->interpreted());
+    ENSURE(get_node(g, bv, bv.mk_concat(x1, x2))->get_root()->interpreted());
+    ENSURE(get_node(g, bv, x1)->get_root()->interpreted());
+    ENSURE(get_node(g, bv, x2)->get_root()->interpreted());
 }
 
 // propagate extract up
@@ -121,7 +121,7 @@ static void test4() {
     g.merge(get_node(g, bv, x1), get_node(g, bv, a), nullptr);
     g.propagate();
     TRACE(bv, tout << g << "\n");
-    SASSERT(get_node(g, bv, bv.mk_extract(23, 8, x))->get_root() == get_node(g, bv, y)->get_root());
+    ENSURE(get_node(g, bv, bv.mk_extract(23, 8, x))->get_root() == get_node(g, bv, y)->get_root());
 }
 
 // iterative slicing
diff --git a/src/test/fuzzing/expr_delta.cpp b/src/test/fuzzing/expr_delta.cpp
index b087cc35a6..aa583ace7a 100644
--- a/src/test/fuzzing/expr_delta.cpp
+++ b/src/test/fuzzing/expr_delta.cpp
@@ -61,13 +61,13 @@ bool expr_delta::delta_dfs(unsigned& n, expr* e, expr_ref& result) {
     }
     else if (is_app(e)) {        
         if (m.is_bool(e)) {
-            SASSERT(n >= 2);
+            ENSURE(n >= 2);
             n -= 2;
         }
         return delta_dfs(n, to_app(e), result);
     }
     else if (is_quantifier(e)) {
-        SASSERT(n >= 2);
+        ENSURE(n >= 2);
         n -= 2;
         quantifier* q = to_quantifier(e);
         if (delta_dfs(n, q->get_expr(), result)) {
diff --git a/src/test/fuzzing/expr_rand.cpp b/src/test/fuzzing/expr_rand.cpp
index c0ffcc767a..fe0e76a7a3 100644
--- a/src/test/fuzzing/expr_rand.cpp
+++ b/src/test/fuzzing/expr_rand.cpp
@@ -77,7 +77,7 @@ expr* expr_rand::choose_expr(sort* s) {
         if (!m_nodes.find(s, vals)) {
             UNREACHABLE();
         }
-        SASSERT(vals);
+        ENSURE(vals);
     }
     unsigned idx = m_random(vals->size());
     return (*vals)[idx].get();
diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h
index 7d8ab6bfed..2e1a55ee27 100644
--- a/src/test/lp/gomory_test.h
+++ b/src/test/lp/gomory_test.h
@@ -72,7 +72,7 @@ struct gomory_test {
             expl.add_pair(column_lower_bound_constraint(x_j), new_a);
         }
         else {
-            SASSERT(at_upper(x_j));
+            ENSURE(at_upper(x_j));
             if (a.is_pos()) {
                 new_a =   a / f_0; 
                 new_a.neg(); // the upper terms are inverted.
@@ -88,9 +88,9 @@ struct gomory_test {
     }
     
     void int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term & t, explanation& expl, mpq & lcm_den, const mpq& f_0, const mpq& one_minus_f_0) {
-        SASSERT(is_integer(x_j));
-        SASSERT(!a.is_int());
-             SASSERT(f_0 > zero_of_type<mpq>() && f_0 < one_of_type<mpq>());
+        ENSURE(is_integer(x_j));
+        ENSURE(!a.is_int());
+             ENSURE(f_0 > zero_of_type<mpq>() && f_0 < one_of_type<mpq>());
         mpq f_j =  fractional_part(a);
         TRACE(gomory_cut_detail, 
               tout << a << " x_j = " << x_j << ", k = " << k << "\n";
@@ -99,7 +99,7 @@ struct gomory_test {
               tout << "1 - f_0: " << one_minus_f_0 << "\n";
               tout << "at_low(" << x_j << ") = " << at_low(x_j) << std::endl;
               );
-        SASSERT (!f_j.is_zero());
+        ENSURE (!f_j.is_zero());
         mpq new_a;
         if (at_low(x_j)) {
             if (f_j <= one_minus_f_0) {
@@ -112,7 +112,7 @@ struct gomory_test {
             expl.add_pair(column_lower_bound_constraint(x_j), new_a);
         }
         else {
-            SASSERT(at_upper(x_j));
+            ENSURE(at_upper(x_j));
             if (f_j <= f_0) {
                 new_a = f_j / f_0;
             }
@@ -134,13 +134,13 @@ struct gomory_test {
     }
 
     void adjust_term_and_k_for_some_ints_case_gomory(lar_term& t, mpq& k, mpq &lcm_den) {
-        SASSERT(!t.is_empty());
+        ENSURE(!t.is_empty());
         auto pol = t.coeffs_as_vector();
         t.clear();
         if (pol.size() == 1) {
             TRACE(gomory_cut_detail, tout << "pol.size() is 1" << std::endl;);
             unsigned v = pol[0].second;
-            SASSERT(is_integer(v));
+            ENSURE(is_integer(v));
             const mpq& a = pol[0].first;
             k /= a;
             if (a.is_pos()) { // we have av >= k
@@ -162,12 +162,12 @@ struct gomory_test {
                       tout << pol[i].first << " " << pol[i].second << "\n";
                   }
                   tout << "k: " << k << "\n";);
-            SASSERT(lcm_den.is_pos());
+            ENSURE(lcm_den.is_pos());
             if (!lcm_den.is_one()) {
                 // normalize coefficients of integer parameters to be integers.
                 for (auto & pi: pol) {
                     pi.first *= lcm_den;
-                    SASSERT(!is_integer(pi.second) || pi.first.is_int());
+                    ENSURE(!is_integer(pi.second) || pi.first.is_int());
                 }
                 k *= lcm_den;
             }
@@ -183,7 +183,7 @@ struct gomory_test {
             k.neg();
         }
         TRACE(gomory_cut_detail, tout << "k = " << k << std::endl;);
-        SASSERT(k.is_int());
+        ENSURE(k.is_int());
     }
 
     void print_term(lar_term & t, std::ostream & out) {
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 7eaef8543a..374c2e2aea 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -387,7 +387,7 @@ vector<int> allocate_basis_heading(
 
 void init_basic_part_of_basis_heading(vector<unsigned> &basis,
                                       vector<int> &basis_heading) {
-    SASSERT(basis_heading.size() >= basis.size());
+    ENSURE(basis_heading.size() >= basis.size());
     unsigned m = basis.size();
     for (unsigned i = 0; i < m; ++i) {
         unsigned column = basis[i];
@@ -581,7 +581,7 @@ void test_stacked_unsigned() {
     v = 3;
     v = 4;
     v.pop();
-    SASSERT(v == 2);
+    ENSURE(v == 2);
     v++;
     v++;
     std::cout << "before push v=" << v << std::endl;
@@ -591,7 +591,7 @@ void test_stacked_unsigned() {
     v += 1;
     std::cout << "v = " << v << std::endl;
     v.pop(2);
-    SASSERT(v == 4);
+    ENSURE(v == 4);
     const unsigned &rr = v;
     std::cout << rr << std::endl;
 }
@@ -755,22 +755,22 @@ void test_numeric_pair() {
     numeric_pair<lp::mpq> c(0.1, 0.5);
     a += 2 * c;
     a -= c;
-    SASSERT(a == b + c);
+    ENSURE(a == b + c);
     numeric_pair<lp::mpq> d = a * 2;
     std::cout << a << std::endl;
-    SASSERT(b == b);
-    SASSERT(b < a);
-    SASSERT(b <= a);
-    SASSERT(a > b);
-    SASSERT(a != b);
-    SASSERT(a >= b);
-    SASSERT(-a < b);
-    SASSERT(a < 2 * b);
-    SASSERT(b + b > a);
-    SASSERT(lp::mpq(2.1) * b + b > a);
-    SASSERT(-b * lp::mpq(2.1) - b < lp::mpq(0.99) * a);
+    ENSURE(b == b);
+    ENSURE(b < a);
+    ENSURE(b <= a);
+    ENSURE(a > b);
+    ENSURE(a != b);
+    ENSURE(a >= b);
+    ENSURE(-a < b);
+    ENSURE(a < 2 * b);
+    ENSURE(b + b > a);
+    ENSURE(lp::mpq(2.1) * b + b > a);
+    ENSURE(-b * lp::mpq(2.1) - b < lp::mpq(0.99) * a);
     std::cout << -b * lp::mpq(2.1) - b << std::endl;
-    SASSERT(-b * (lp::mpq(2.1) + 1) == -b * lp::mpq(2.1) - b);
+    ENSURE(-b * (lp::mpq(2.1) + 1) == -b * lp::mpq(2.1) - b);
     std::cout << -b * (lp::mpq(2.1) + 1) << std::endl;
 }
 
@@ -859,7 +859,7 @@ void test_evidence_for_total_inf_simple(argument_parser &args_parser) {
     auto status = solver.solve();
     std::cout << lp_status_to_string(status) << std::endl;
     std::unordered_map<lpvar, mpq> model;
-    SASSERT(solver.get_status() == lp_status::INFEASIBLE);
+    ENSURE(solver.get_status() == lp_status::INFEASIBLE);
 }
 void test_bound_propagation_one_small_sample1() {
     /*
@@ -1065,8 +1065,8 @@ void test_total_case_l() {
     // ls.solve();
     // my_bound_propagator bp(ls);
     // ls.propagate_bounds_for_touched_rows(bp);
-    // SASSERT(ev.size() == 4);
-    // SASSERT(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));
+    // ENSURE(ev.size() == 4);
+    // ENSURE(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));
 }
 void test_bound_propagation() {
     test_total_case_u();
@@ -1082,14 +1082,14 @@ void test_int_set() {
     indexed_uint_set s;
     s.insert(1);
     s.insert(2);
-    SASSERT(s.contains(2));
-    SASSERT(s.size() == 2);
+    ENSURE(s.contains(2));
+    ENSURE(s.size() == 2);
     s.remove(2);
-    SASSERT(s.size() == 1);
+    ENSURE(s.size() == 1);
     s.insert(3);
     s.insert(2);
     s.reset();
-    SASSERT(s.size() == 0);
+    ENSURE(s.size() == 0);
     std::cout << "done test_int_set\n";
 }
 
@@ -1197,12 +1197,12 @@ void get_random_interval(bool &neg_inf, bool &pos_inf, int &x, int &y) {
         pos_inf = false;
         if (!neg_inf) {
             y = x + my_random() % (101 - x);
-            SASSERT(y >= x);
+            ENSURE(y >= x);
         } else {
             y = my_random() % 100;
         }
     }
-    SASSERT((neg_inf || (0 <= x && x <= 100)) &&
+    ENSURE((neg_inf || (0 <= x && x <= 100)) &&
             (pos_inf || (0 <= y && y <= 100)));
 }
 
@@ -1633,7 +1633,7 @@ void test_maximize_term() {
     solver.add_var_bound(term_x_min_y, LE, zero_of_type<mpq>());
     solver.add_var_bound(term_2x_pl_2y, LE, mpq(5));
     solver.find_feasible_solution();
-    SASSERT(solver.get_status() == lp_status::OPTIMAL);
+    ENSURE(solver.get_status() == lp_status::OPTIMAL);
     std::cout << solver.constraints();
     std::unordered_map<lpvar, mpq> model;
     solver.get_model(model);
@@ -1707,7 +1707,7 @@ void test_dio() {
     solver.add_var_bound(t1, LE, mpq(0));
     solver.add_var_bound(t1, GE, mpq(0));
 //    solver.find_feasible_solution();
-    //SASSERT(solver.get_status() == lp_status::OPTIMAL);
+    //ENSURE(solver.get_status() == lp_status::OPTIMAL);
     enable_trace("dioph_eq");
     enable_trace("dioph_eq_fresh");
 #ifdef Z3DEBUG     
@@ -1754,14 +1754,14 @@ void test_gomory_cut() {
         matrix.add_rows(mpq(2), 0, 1); // row 1 = row 1 + 2 * row 0
 
         // Verify the results
-        SASSERT(matrix.get_elem(1, 0) == 5); // 3 + 2*1
-        SASSERT(matrix.get_elem(1, 1) == 4); // 0 + 2*2
-        SASSERT(matrix.get_elem(1, 2) == 4); // unchanged
+        ENSURE(matrix.get_elem(1, 0) == 5); // 3 + 2*1
+        ENSURE(matrix.get_elem(1, 1) == 4); // 0 + 2*2
+        ENSURE(matrix.get_elem(1, 2) == 4); // unchanged
 
         matrix.add_rows(mpq(-2), 0, 1);
-        SASSERT(matrix.get_elem(1, 0) == 3); // 5 - 2*1
-        SASSERT(matrix.get_elem(1, 1) == 0); // 4 - 2*2
-        SASSERT(matrix.get_elem(1, 2) == 4); // unchanged
+        ENSURE(matrix.get_elem(1, 0) == 3); // 5 - 2*1
+        ENSURE(matrix.get_elem(1, 1) == 0); // 4 - 2*2
+        ENSURE(matrix.get_elem(1, 2) == 4); // unchanged
     }
     
 void test_nla_order_lemma() { nla::test_order_lemma(); }
@@ -1787,7 +1787,7 @@ void test_restore_x() {
         solver.add_var_bound(t, LE, mpq(15));
 
         auto status = solver.solve();
-        SASSERT(status == lp_status::OPTIMAL);
+        ENSURE(status == lp_status::OPTIMAL);
 
         // Backup the current solution
         solver.backup_x();
@@ -1802,7 +1802,7 @@ void test_restore_x() {
 
         // The solver should find a feasible solution
         status = solver.get_status();
-        SASSERT(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
+        ENSURE(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
         std::cout << "  test 1 (backup shorter): " << lp_status_to_string(status) << " - PASSED" << std::endl;
     }
 
@@ -1829,7 +1829,7 @@ void test_restore_x() {
 
         auto status = solver.solve();
         (void)status;
-        SASSERT(status == lp_status::OPTIMAL);
+        ENSURE(status == lp_status::OPTIMAL);
 
         // Backup with the full system
         solver.backup_x();
@@ -1850,7 +1850,7 @@ void test_restore_x() {
         solver.add_var_bound(y, LE, mpq(10));
 
         auto status = solver.solve();
-        SASSERT(status == lp_status::OPTIMAL);
+        ENSURE(status == lp_status::OPTIMAL);
 
         // Add new constraint: x + y >= 5
         vector<std::pair<mpq, lpvar>> coeffs;
@@ -1867,17 +1867,17 @@ void test_restore_x() {
 
         // Solve expanded system, then move non-basic columns to bounds
         status = solver.solve();
-        SASSERT(status == lp_status::OPTIMAL);
+        ENSURE(status == lp_status::OPTIMAL);
         solver.move_non_basic_columns_to_bounds();
         status = solver.get_status();
-        SASSERT(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
+        ENSURE(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
 
         // Verify the model satisfies the constraints
         std::unordered_map<lpvar, mpq> model;
         solver.get_model(model);
-        SASSERT(model[x] >= mpq(1) && model[x] <= mpq(10));
-        SASSERT(model[y] >= mpq(1) && model[y] <= mpq(10));
-        SASSERT(model[w] >= mpq(2) && model[w] <= mpq(8));
+        ENSURE(model[x] >= mpq(1) && model[x] <= mpq(10));
+        ENSURE(model[y] >= mpq(1) && model[y] <= mpq(10));
+        ENSURE(model[w] >= mpq(2) && model[w] <= mpq(8));
         std::cout << "  test 3 (move_non_basic_columns_to_bounds): " << lp_status_to_string(status) << " - PASSED" << std::endl;
     }
 
@@ -2036,13 +2036,13 @@ void asserts_on_patching(const rational &x, const rational &alpha) {
     auto a2 = denominator(alpha);
     auto x1 = numerator(x);
     auto x2 = denominator(x);
-    SASSERT(a1.is_pos());
-    SASSERT(abs(a1) < abs(a2));
-    SASSERT(coprime(a1, a2));
-    SASSERT(x1.is_pos());
-    SASSERT(x1 < x2);
-    SASSERT(coprime(x1, x2));
-    SASSERT((a2 / x2).is_int());
+    ENSURE(a1.is_pos());
+    ENSURE(abs(a1) < abs(a2));
+    ENSURE(coprime(a1, a2));
+    ENSURE(x1.is_pos());
+    ENSURE(x1 < x2);
+    ENSURE(coprime(x1, x2));
+    ENSURE((a2 / x2).is_int());
 }
 void get_patching_deltas(const rational &x, const rational &alpha, rational &delta_0, rational &delta_1) {
     std::cout << "get_patching_deltas(" << x << ", " << alpha << ")" << std::endl;
@@ -2050,7 +2050,7 @@ void get_patching_deltas(const rational &x, const rational &alpha, rational &del
     auto a2 = denominator(alpha);
     auto x1 = numerator(x);
     auto x2 = denominator(x);
-    SASSERT(divides(x2, a2));
+    ENSURE(divides(x2, a2));
     // delta has to be integral.
     // We need to find delta such that x1/x2 + (a1/a2)*delta is integral.
     // Then a2*x1/x2 + a1*delta is integral, that means that t = a2/x2 is integral.
@@ -2064,17 +2064,17 @@ void get_patching_deltas(const rational &x, const rational &alpha, rational &del
     // We know that a2 and a1 are coprime, and x2 divides a2, so x2 and a1 are coprime.
     rational u, v;
     auto g = gcd(a1, x2, u, v);
-    SASSERT(g.is_one() && u.is_int() && v.is_int() && g == u * a1 + v * x2);
+    ENSURE(g.is_one() && u.is_int() && v.is_int() && g == u * a1 + v * x2);
     std::cout << "u = " << u << ", v = " << v << std::endl;
     std::cout << "x= " << (x1 / x2) << std::endl;
     std::cout << "x + (a1 / a2) * (-u * t) * x1 = " << x + (a1 / a2) * (-u * t) * x1 << std::endl;
-    SASSERT((x + (a1 / a2) * (-u * t) * x1).is_int());
+    ENSURE((x + (a1 / a2) * (-u * t) * x1).is_int());
     // 1 = (u- l*x2 ) * a1 + (v + l*a1)*x2, for every integer l.
     rational d = u * t * x1;
     delta_0 = mod(d, a2);
-    SASSERT(delta_0 > 0);
+    ENSURE(delta_0 > 0);
     delta_1 = delta_0 - a2;
-    SASSERT(delta_1 < 0);
+    ENSURE(delta_1 < 0);
     std::cout << "delta_0 = " << delta_0 << std::endl;
     std::cout << "delta_1 = " << delta_1 << std::endl;
 }
@@ -2102,10 +2102,10 @@ void test_patching_alpha(const rational &x, const rational &alpha) {
     rational delta_0, delta_1;
     get_patching_deltas(x, alpha, delta_0, delta_1);
 
-    SASSERT(delta_0 * delta_1 < 0);
+    ENSURE(delta_0 * delta_1 < 0);
 
-    SASSERT((x - alpha * delta_0).is_int());
-    SASSERT((x - alpha * delta_1).is_int());
+    ENSURE((x - alpha * delta_0).is_int());
+    ENSURE((x - alpha * delta_1).is_int());
     try_find_smaller_delta(x, alpha, delta_0, delta_1);
     // std::cout << "delta_minus = " << delta_minus << ", delta_1 = " << delta_1 << "\n";
     // std::cout << "x + alpha*delta_minus = " << x + alpha * delta_minus << "\n";
@@ -2116,7 +2116,7 @@ void find_a1_x1_x2_and_fix_a2(int &x1, int &x2, int &a1, int &a2) {
     x2 = (rand() % a2) + (int)(a2 / 3);
     auto g = gcd(rational(a2), rational(x2));
     a2 *= (x2 / numerator(g).get_int32());
-    SASSERT(rational(a2, x2).is_int());
+    ENSURE(rational(a2, x2).is_int());
     do {
         x1 = rand() % (unsigned)x2 + 1;
     } while (!coprime(x1, x2));
diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp
index d2e2e2f19f..34e1f90dbc 100644
--- a/src/test/lp/nla_solver_test.cpp
+++ b/src/test/lp/nla_solver_test.cpp
@@ -35,7 +35,7 @@ void add_equality(int n_of_vars, var_eqs<emonics> & var_eqs, random_gen& rand, b
     while (a == b) {
         b = rand() % n_of_vars;
     }
-    SASSERT(a != b);
+    ENSURE(a != b);
     var_eqs.merge_plus(a, b, eq_justification({0}));
 }
 
@@ -262,7 +262,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
 
     VERIFY(nla.get_core().test_check() == l_false);
     auto const& lemma = nla.get_core().lemmas();
-    SASSERT(lemma[0].size() == 4);
+    ENSURE(lemma[0].size() == 4);
     nla.get_core().print_lemma(lemma.back(), std::cout);
 
     lp::lar_term t0, t1, t2, t3;
@@ -348,7 +348,7 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
     VERIFY(nla.get_core().test_check() == l_false);
     auto const& lemma = nla.get_core().lemmas();
     nla.get_core().print_lemma(lemma.back(), std::cout);
-    SASSERT(lemma.size() == 1 && lemma[0].size() == 2);
+    ENSURE(lemma.size() == 1 && lemma[0].size() == 2);
     lp::lar_term t0, t1;
     t0.add_var(lp_b);
     t1.add_var(lp_be);
@@ -697,7 +697,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
    
     // set abef = cdij, while it has to be abef < cdij
     if (sign > 0) {
-        SASSERT(s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
+        ENSURE(s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
         // we have ab < cd
 
         // we need to have ab*ef < cd*ij, so let us make ab*ef > cd*ij
@@ -707,7 +707,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
         
     }
     else {
-        SASSERT(-s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
+        ENSURE(-s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
         // we need to have abef < cdij, so let us make abef < cdij
         s_set_column_value_test(s, lp_cdij, nla.get_core().mon_value_by_vars(mon_cdij));
         s_set_column_value_test(s, lp_abef, nla.get_core().mon_value_by_vars(mon_cdij)
@@ -722,7 +722,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
     // ineq q(llc::EQ, t, rational(0));
    
     nla.get_core().print_lemma(lemma.back(), std::cout);
-    // SASSERT(q == lemma.back());
+    // ENSURE(q == lemma.back());
     // ineq i0(llc::EQ, lp::lar_term(), rational(0));
     // i0.m_term.add_monomial(lp_bde);
     // i0.m_term.add_monomial(rational(1), lp_acd);
@@ -733,7 +733,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
     //     } 
     // }
 
-    // SASSERT(found);
+    // ENSURE(found);
     */
 }
 
diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h
index 7f33d7c40c..97130a6662 100644
--- a/src/test/lp/smt_reader.h
+++ b/src/test/lp/smt_reader.h
@@ -117,13 +117,13 @@ namespace lp {
 
         void fill_simple_elem(lisp_elem & lm) {
             int separator = first_separator();
-            SASSERT(-1 != separator && separator != 0);
+            ENSURE(-1 != separator && separator != 0);
             lm.m_head = m_line.substr(0, separator);
             m_line = m_line.substr(separator);
         }
 
         void fill_nested_elem(lisp_elem & lm) {
-            SASSERT(m_line[0] == '(');
+            ENSURE(m_line[0] == '(');
             m_line = m_line.substr(1);
             int separator = first_separator();
             lm.m_head = m_line.substr(0, separator);
@@ -190,11 +190,11 @@ namespace lp {
         }
 
         void adjust_right_side(formula_constraint & /* c*/, lisp_elem & /*el*/) {
-            // SASSERT(el.m_head == "0"); // do nothing for the time being
+            // ENSURE(el.m_head == "0"); // do nothing for the time being
         }
 
         void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) {
-            SASSERT(el.m_elems.size() == 2);
+            ENSURE(el.m_elems.size() == 2);
             set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]);
             adjust_right_side(c, el.m_elems[1]);
         }
@@ -210,7 +210,7 @@ namespace lp {
                 add_mult_elem(c, el.m_elems);
             } else if (el.m_head == "~") {
                 lisp_elem & minel = el.m_elems[0];
-                SASSERT(minel.is_simple());
+                ENSURE(minel.is_simple());
                 c.m_right_side += mpq(str_to_int(minel.m_head));
             } else {
                 std::cout << "unexpected input " << el.m_head << std::endl;
@@ -220,14 +220,14 @@ namespace lp {
         }
 
         std::string get_name(lisp_elem & name) {
-            SASSERT(name.is_simple());
-            SASSERT(!is_integer(name.m_head));
+            ENSURE(name.is_simple());
+            ENSURE(!is_integer(name.m_head));
             return name.m_head;
         }
 
 
         void add_mult_elem(formula_constraint & c, std::vector<lisp_elem> & els) {
-            SASSERT(els.size() == 2);
+            ENSURE(els.size() == 2);
             mpq coeff = get_coeff(els[0]);
             std::string col_name = get_name(els[1]);
             c.add_pair(coeff, col_name);
@@ -237,16 +237,16 @@ namespace lp {
             if (le.is_simple()) {
                 return mpq(str_to_int(le.m_head));
             } else {
-                SASSERT(le.m_head == "~");
-                SASSERT(le.size() == 1);
+                ENSURE(le.m_head == "~");
+                ENSURE(le.size() == 1);
                 lisp_elem & el = le.m_elems[0];
-                SASSERT(el.is_simple());
+                ENSURE(el.is_simple());
                 return -mpq(str_to_int(el.m_head));
             }
         }
 
         int str_to_int(std::string & s) {
-            SASSERT(is_integer(s));
+            ENSURE(is_integer(s));
             return atoi(s.c_str());
         }
 
@@ -254,7 +254,7 @@ namespace lp {
             if (el.size()) {
                 add_complex_sum_elem(c, el);
             } else {
-                SASSERT(is_integer(el.m_head));
+                ENSURE(is_integer(el.m_head));
                 int v = atoi(el.m_head.c_str());
                 mpq vr(v);
                 c.m_right_side -= vr;
diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp
index 571b229c49..ed748826e6 100644
--- a/src/test/model_evaluator.cpp
+++ b/src/test/model_evaluator.cpp
@@ -78,17 +78,17 @@ void tst_model_evaluator() {
             fi2.insert_entry(args, i == 599 ? one.get() : zero.get());
         }
         fi2.compress();
-        SASSERT(fi2.num_entries() == 1);
+        ENSURE(fi2.num_entries() == 1);
 
         expr_ref removed_arg(a.mk_int(0), m);
         [[maybe_unused]] expr* removed_args[1] = { removed_arg.get() };
-        SASSERT(fi2.get_entry(removed_args) == nullptr);
+        ENSURE(fi2.get_entry(removed_args) == nullptr);
 
         expr_ref kept_arg(a.mk_int(599), m);
         expr* kept_args[1] = { kept_arg.get() };
         [[maybe_unused]] func_entry* kept = fi2.get_entry(kept_args);
-        SASSERT(kept != nullptr);
-        SASSERT(kept->get_result() == one.get());
+        ENSURE(kept != nullptr);
+        ENSURE(kept->get_result() == one.get());
     }
     
 }
diff --git a/src/test/permutation.cpp b/src/test/permutation.cpp
index 9e6a2d6719..abef65668a 100644
--- a/src/test/permutation.cpp
+++ b/src/test/permutation.cpp
@@ -9,8 +9,8 @@
 static void test_constructor() {
     permutation p(5);
     for (unsigned i = 0; i < 5; ++i) {
-        SASSERT(p(i) == i);
-        SASSERT(p.inv(i) == i);
+        ENSURE(p(i) == i);
+        ENSURE(p.inv(i) == i);
     }
 }
 
@@ -19,28 +19,28 @@ static void test_reset() {
     p.swap(0, 2);
     p.reset(3);
     for (unsigned i = 0; i < 3; ++i) {
-        SASSERT(p(i) == i);
-        SASSERT(p.inv(i) == i);
+        ENSURE(p(i) == i);
+        ENSURE(p.inv(i) == i);
     }
 }
 
 static void test_swap() {
     permutation p(4);
     p.swap(1, 3);
-    SASSERT(p(1) == 3);
-    SASSERT(p(3) == 1);
-    SASSERT(p.inv(1) == 3);
-    SASSERT(p.inv(3) == 1);
+    ENSURE(p(1) == 3);
+    ENSURE(p(3) == 1);
+    ENSURE(p.inv(1) == 3);
+    ENSURE(p.inv(3) == 1);
 }
 
 static void test_move_after() {
     permutation p(5);
     p.move_after(1, 3);
-    SASSERT(p(0) == 0);
-    SASSERT(p(1) == 2);
-    SASSERT(p(2) == 3);
-    SASSERT(p(3) == 1);
-    SASSERT(p(4) == 4);
+    ENSURE(p(0) == 0);
+    ENSURE(p(1) == 2);
+    ENSURE(p(2) == 3);
+    ENSURE(p(3) == 1);
+    ENSURE(p(4) == 4);
 }
 
 void apply_permutation_copy(unsigned sz, unsigned const * src, unsigned const * p, unsigned * target) {
@@ -74,18 +74,18 @@ static void test_apply_permutation(unsigned sz, unsigned num_tries, unsigned max
 
 static void test_check_invariant() {
     permutation p(4);
-    SASSERT(p.check_invariant());
+    ENSURE(p.check_invariant());
     p.swap(0, 2);
-    SASSERT(p.check_invariant());
+    ENSURE(p.check_invariant());
     p.move_after(1, 3);
-    SASSERT(p.check_invariant());
+    ENSURE(p.check_invariant());
 }
 
 static void test_display() {
     permutation p(4);
     std::ostringstream out;
     p.display(out);
-    SASSERT(out.str() == "0:0 1:1 2:2 3:3");
+    ENSURE(out.str() == "0:0 1:1 2:2 3:3");
 }
 
 void tst_permutation() {
diff --git a/src/test/psmt.cpp b/src/test/psmt.cpp
index c8cf2da541..9d66c268c9 100644
--- a/src/test/psmt.cpp
+++ b/src/test/psmt.cpp
@@ -62,7 +62,7 @@ static void tst_psmt_worker() {
         expr_dependency_ref core(m);
         std::string         reason_unknown;
         lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
-        SASSERT(r == l_true);
+        ENSURE(r == l_true);
         (void)r;
         std::cout << "psmt SAT: " << r << "\n";
     }
@@ -82,7 +82,7 @@ static void tst_psmt_worker() {
         expr_dependency_ref core(m);
         std::string         reason_unknown;
         lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
-        SASSERT(r == l_false);
+        ENSURE(r == l_false);
         (void)r;
         std::cout << "psmt UNSAT: " << r << "\n";
     }
@@ -131,7 +131,7 @@ static void tst_psmt_worker() {
         lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
         // The result must be l_undef (theory-incomplete).
         // If the fix is absent, this call deadlocks instead of returning.
-        SASSERT(r == l_undef);
+        ENSURE(r == l_undef);
         (void)r;
         std::cout << "psmt UNKNOWN (no deadlock): " << r << "\n";
     }
diff --git a/src/test/rational.cpp b/src/test/rational.cpp
index 8e17d0f987..1413e2bffd 100644
--- a/src/test/rational.cpp
+++ b/src/test/rational.cpp
@@ -457,10 +457,10 @@ static void tst12() {
     std::cout << "test12\n";
     rational r;
     r = 5;
-    SASSERT(r.get_bit(0));
-    SASSERT(!r.get_bit(1));
-    SASSERT(r.get_bit(2));
-    SASSERT(!r.get_bit(3));
+    ENSURE(r.get_bit(0));
+    ENSURE(!r.get_bit(1));
+    ENSURE(r.get_bit(2));
+    ENSURE(!r.get_bit(3));
     r = rational("10000000000000000000000000000000001");
     for (unsigned i = 0; i < r.get_num_bits(); ++i)
         std::cout << i << ": " << r.get_bit(i) << "\n";
diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp
index ce52dcc788..cdbb26df62 100644
--- a/src/test/sat_local_search.cpp
+++ b/src/test/sat_local_search.cpp
@@ -3,6 +3,7 @@
 #include "util/cancel_eh.h"
 #include "util/scoped_ctrl_c.h"
 #include "util/scoped_timer.h"
+#include <cstdio>
 #include <iostream>
 
 static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search)
@@ -16,13 +17,12 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
         return false;
     }
     infile.getline(line, 16383);
-#ifdef _WINDOWS
     int cur_term;
     int num_vars = 0, num_constraints = 0;
-    sscanf_s(line, "%d %d", &num_vars, &num_constraints);
-    //std::cout << "number of variables: " << num_vars << '\n';
-    //std::cout << "number of constraints: " << num_constraints << '\n';
-
+    if (sscanf(line, "%d %d", &num_vars, &num_constraints) != 2) {
+        std::cout << "Failed to parse header (expected: num_vars num_constraints)\n";
+        return false;
+    }
 
     unsigned_vector coefficients;
     sat::literal_vector lits;
@@ -57,15 +57,11 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
             infile >> cur_term;
         }
         infile >> k;
-        //local_search.add_cardinality(lits.size(), lits.c_ptr(), static_cast<unsigned>(lits.size() - k));
         local_search.add_cardinality(lits.size(), lits.data(), static_cast<unsigned>(k));
     }
 
     infile.close();
     return true;
-#else
-    return false;
-#endif
 }
 
 void tst_sat_local_search(char ** argv, int argc, int& i) {
diff --git a/src/test/scoped_vector.cpp b/src/test/scoped_vector.cpp
index 05d98fcf10..2c0cb9ac07 100644
--- a/src/test/scoped_vector.cpp
+++ b/src/test/scoped_vector.cpp
@@ -7,9 +7,9 @@ void test_push_back_and_access() {
     
     sv.push_back(20);
 
-    SASSERT(sv.size() == 2);
-    SASSERT(sv[0] == 10);
-    SASSERT(sv[1] == 20);
+    ENSURE(sv.size() == 2);
+    ENSURE(sv[0] == 10);
+    ENSURE(sv[1] == 20);
     
     std::cout << "test_push_back_and_access passed." << std::endl;
 }
@@ -23,16 +23,16 @@ void test_scopes() {
     sv.push_back(30);
     sv.push_back(40);
 
-    SASSERT(sv.size() == 4);
-    SASSERT(sv[2] == 30);
-    SASSERT(sv[3] == 40);
+    ENSURE(sv.size() == 4);
+    ENSURE(sv[2] == 30);
+    ENSURE(sv[3] == 40);
 
     sv.pop_scope(1);
 
     std::cout << "test_scopes passed." << std::endl;
-    SASSERT(sv.size() == 2);
-    SASSERT(sv[0] == 10);
-    SASSERT(sv[1] == 20);
+    ENSURE(sv.size() == 2);
+    ENSURE(sv[0] == 10);
+    ENSURE(sv[1] == 20);
 
     std::cout << "test_scopes passed." << std::endl;
 }
@@ -45,15 +45,15 @@ void test_set() {
     sv.set(0, 30);
     sv.set(1, 40);
 
-    SASSERT(sv.size() == 2);
-    SASSERT(sv[0] == 30);
-    SASSERT(sv[1] == 40);
+    ENSURE(sv.size() == 2);
+    ENSURE(sv[0] == 30);
+    ENSURE(sv[1] == 40);
 
     sv.push_scope();
     sv.set(0, 50);
-    SASSERT(sv[0] == 50);
+    ENSURE(sv[0] == 50);
     sv.pop_scope(1);
-    SASSERT(sv[0] == 30);
+    ENSURE(sv[0] == 30);
 
     std::cout << "test_set passed." << std::endl;
 }
@@ -63,12 +63,12 @@ void test_pop_back() {
     sv.push_back(10);
     sv.push_back(20);
 
-    SASSERT(sv.size() == 2);
+    ENSURE(sv.size() == 2);
     sv.pop_back();
-    SASSERT(sv.size() == 1);
-    SASSERT(sv[0] == 10);
+    ENSURE(sv.size() == 1);
+    ENSURE(sv[0] == 10);
     sv.pop_back();
-    SASSERT(sv.size() == 0);
+    ENSURE(sv.size() == 0);
 
     std::cout << "test_pop_back passed." << std::endl;
 }
@@ -81,9 +81,9 @@ void test_erase_and_swap() {
 
     sv.erase_and_swap(1);
 
-    SASSERT(sv.size() == 2);
-    SASSERT(sv[0] == 10);
-    SASSERT(sv[1] == 30);
+    ENSURE(sv.size() == 2);
+    ENSURE(sv[0] == 10);
+    ENSURE(sv[1] == 30);
 
     std::cout << "test_erase_and_swap passed." << std::endl;
 }
diff --git a/src/test/sls_seq_plugin.cpp b/src/test/sls_seq_plugin.cpp
index 94d1ce5bb9..117e5bacee 100644
--- a/src/test/sls_seq_plugin.cpp
+++ b/src/test/sls_seq_plugin.cpp
@@ -221,7 +221,7 @@ struct test_seq {
     }
 
     zstring& strval0(expr* e) {
-        SASSERT(seq.is_string(e->get_sort()));
+        ENSURE(seq.is_string(e->get_sort()));
         return get_eval(e).val0.svalue;
     }
 
diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp
index 18955fe825..293372052f 100644
--- a/src/test/sls_test.cpp
+++ b/src/test/sls_test.cpp
@@ -86,7 +86,7 @@ namespace bv {
                     verbose_stream() << mk_pp(e, m) << " computed value " << val << "\n";
                     verbose_stream() << "should be " << n2 << "\n";
                 }
-                SASSERT(n1 == n2);
+                ENSURE(n1 == n2);
                 VERIFY(n1 == n2);
             }
             else if (m.is_bool(e)) {
@@ -96,7 +96,7 @@ namespace bv {
                     verbose_stream() << mk_pp(e, m) << " computed value " << val1 
                         << " at odds with definition " << val2 << "\n";
                 }
-                SASSERT(val1 == val2);
+                ENSURE(val1 == val2);
                 VERIFY(val1 == val2);
             }
         }
@@ -193,7 +193,7 @@ namespace bv {
             ev.init();
 
             if (m.is_bool(e1)) {
-                SASSERT(m.is_true(r) || m.is_false(r));
+                ENSURE(m.is_true(r) || m.is_false(r));
                 auto val = m.is_true(r);
                 auto val2 = ev.bval1(to_app(e2));
                 if (val != val2) {
@@ -208,7 +208,7 @@ namespace bv {
                         ev.display(std::cout);
                         exit(0);
                     }
-                    //SASSERT(rep1);
+                    //ENSURE(rep1);
                 }
             }
             if (bv.is_bv(e1)) {
@@ -226,7 +226,7 @@ namespace bv {
                     if (!val3.eq(val1)) {
                         verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n";
                     }
-                    //SASSERT(rep2);
+                    //ENSURE(rep2);
                 }
             }
         }
diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp
index bf78d890b1..d0620f9cea 100644
--- a/src/test/sorting_network.cpp
+++ b/src/test/sorting_network.cpp
@@ -539,7 +539,7 @@ static void test_pb(unsigned max_w, unsigned sz, unsigned_vector& ws) {
         }        
     }
     else {
-        SASSERT(ws.size() == sz);
+        ENSURE(ws.size() == sz);
         ast_manager m;
         reg_decl_plugins(m);
         expr_ref_vector xs(m), nxs(m);
diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp
index fe33baba58..1d3f912d82 100644
--- a/src/test/tbv.cpp
+++ b/src/test/tbv.cpp
@@ -103,7 +103,7 @@ static void test_dc() {
         todo.pop_back();
         bool found = false;
         tbit tvalue = eval[t];
-        SASSERT(tvalue != BIT_z);
+        ENSURE(tvalue != BIT_z);
         for (unsigned j = 0; j < 2*num_bits; ++j) {
             tbit tb = (*t)[j];
             if (tb == BIT_x)