diff --git a/src/boolector.c b/src/boolector.c
index 227441a3..9e728978 100644
--- a/src/boolector.c
+++ b/src/boolector.c
@@ -476,7 +476,11 @@ boolector_push (Btor *btor, uint32_t level)
   BTOR_TRAPI ("%u", level);
   BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
               "incremental usage has not been enabled");
-  BTOR_ABORT (level < 1, "context level must be greater than 0");
+
+  if (level == 0)
+  {
+    return;
+  }
 
   uint32_t i;
   for (i = 0; i < level; i++)
@@ -492,7 +496,6 @@ boolector_pop (Btor *btor, uint32_t level)
 {
   BTOR_ABORT_ARG_NULL (btor);
   BTOR_TRAPI ("%u", level);
-  BTOR_ABORT (level < 1, "context level must be greater than 0");
   BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
               "incremental usage has not been enabled");
   BTOR_ABORT (level > BTOR_COUNT_STACK (btor->assertions_trail),
@@ -500,6 +503,11 @@ boolector_pop (Btor *btor, uint32_t level)
               level,
               BTOR_COUNT_STACK (btor->assertions_trail));
 
+  if (level == 0)
+  {
+    return;
+  }
+
   uint32_t i, pos = 0;
   for (i = 0; i < level; i++) pos = BTOR_POP_STACK (btor->assertions_trail);
 
diff --git a/src/parser/btorsmt2.c b/src/parser/btorsmt2.c
index 588f795d..25ea99df 100644
--- a/src/parser/btorsmt2.c
+++ b/src/parser/btorsmt2.c
@@ -4771,7 +4771,7 @@ read_command_smt2 (BtorSMT2Parser *parser)
       break;
 
     case BTOR_PUSH_TAG_SMT2:
-      (void) parse_uint32_smt2 (parser, true, &level);
+      (void) parse_uint32_smt2 (parser, false, &level);
       if (!read_rpar_smt2 (parser, " after 'push'")) return 0;
       for (i = 0; i < level; i++) open_new_scope (parser);
       boolector_push (parser->btor, level);
@@ -4779,7 +4779,7 @@ read_command_smt2 (BtorSMT2Parser *parser)
       break;
 
     case BTOR_POP_TAG_SMT2:
-      (void) parse_uint32_smt2 (parser, true, &level);
+      (void) parse_uint32_smt2 (parser, false, &level);
       if (!read_rpar_smt2 (parser, " after 'pop'")) return 0;
       if (level > parser->scope_level)
       {