diff --git a/src/test/arith_rewriter.cpp b/src/test/arith_rewriter.cpp
index d0a110c4f..da49e58dc 100644
--- a/src/test/arith_rewriter.cpp
+++ b/src/test/arith_rewriter.cpp
@@ -1,4 +1,3 @@
-
 /*++
 Copyright (c) 2015 Microsoft Corporation
 
@@ -26,8 +25,8 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
            << "(assert " << str << ")\n";
     std::istringstream is(buffer.str());
     VERIFY(parse_smt2_commands(ctx, is));
-    ENSURE(ctx.begin_assertions() != ctx.end_assertions());
-    result = *ctx.begin_assertions();
+    ENSURE(!ctx.assertions().empty());
+    result = ctx.assertions().get(0);
     return result;
 }
 
diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp
index ef01bd27d..58481938b 100644
--- a/src/test/polynorm.cpp
+++ b/src/test/polynorm.cpp
@@ -25,8 +25,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
            << "(assert " << str << ")\n";
     std::istringstream is(buffer.str());
     VERIFY(parse_smt2_commands(ctx, is));
-    ENSURE(ctx.begin_assertions() != ctx.end_assertions());
-    result = *ctx.begin_assertions();
+    result = ctx.assertions().get(0);
     return result;
 }
 
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index 031912c46..2b1b9686c 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -37,8 +37,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
            << "(assert " << str << ")\n";
     std::istringstream is(buffer.str());
     VERIFY(parse_smt2_commands(ctx, is));
-    ENSURE(ctx.begin_assertions() != ctx.end_assertions());
-    result = *ctx.begin_assertions();
+    result = ctx.assertions().get(0);
     return result;
 }
 
diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp
index 04a75c42e..d0c616166 100644
--- a/src/test/quant_solve.cpp
+++ b/src/test/quant_solve.cpp
@@ -131,8 +131,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
            << "(assert " << str << ")\n";
     std::istringstream is(buffer.str());
     VERIFY(parse_smt2_commands(ctx, is));
-    ENSURE(ctx.begin_assertions() != ctx.end_assertions());
-    result = *ctx.begin_assertions();
+    result = ctx.assertions().get(0);
     return result;
 }