diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index a5e2bd76b..2d78425c7 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -678,7 +678,7 @@ term       : variable_name
            | DEC_Token '(' term ')'   { init($$, "dec"); mto($$, $3); }
            | ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
            | SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
-           | NUMBER_Token             { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); }
+           | number_expr
            | TRUE_Token               { init($$, ID_constant); stack_expr($$).set(ID_value, ID_true); stack_expr($$).type()=typet(ID_bool); }
            | FALSE_Token              { init($$, ID_constant); stack_expr($$).set(ID_value, ID_false); stack_expr($$).type()=typet(ID_bool); }
            | case_Token cases esac_Token { $$=$2; }
@@ -770,11 +770,19 @@ term       : variable_name
            }
            ;
 
+number_expr: NUMBER_Token
+           {
+             init($$, ID_constant);
+             stack_expr($$).set(ID_value, stack_expr($1).id());
+             stack_expr($$).type()=integer_typet();
+           }
+           ;
+
 bound      : '[' NUMBER_Token ',' NUMBER_Token ']'
            { init($$); mto($$, $2); mto($$, $4); }
            ;
 
-range      : NUMBER_Token DOTDOT_Token NUMBER_Token
+range      : number_expr DOTDOT_Token number_expr
            { init($$); mto($$, $1); mto($$, $3); }
            ;
 
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 0bec5d149..78051cec4 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -86,7 +86,7 @@ class smv_typecheckt:public typecheckt
 
   void convert(smv_parse_treet::modulet::itemt &);
   void typecheck(smv_parse_treet::modulet::itemt &);
-  void typecheck_expr_rec(exprt &, modet);
+  void typecheck_expr_node(exprt &, modet);
   void convert_expr_to(exprt &, const typet &dest);
 
   smv_parse_treet::modulet *modulep;
@@ -614,7 +614,10 @@ Function: smv_typecheckt::typecheck
 
 void smv_typecheckt::typecheck(exprt &expr, modet mode)
 {
-  typecheck_expr_rec(expr, mode);
+  // We use visit_post instead of recursion to avoid
+  // stack overflows on very deep nestings of DEFINE definitions.
+  expr.visit_post([this, mode](exprt &expr)
+                  { typecheck_expr_node(expr, mode); });
 }
 
 /*******************************************************************\
@@ -629,8 +632,10 @@ Function: smv_typecheckt::typecheck_expr_rec
 
 \*******************************************************************/
 
-void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
+void smv_typecheckt::typecheck_expr_node(exprt &expr, modet mode)
 {
+  // now post-traversal
+
   if(expr.id()==ID_symbol || 
      expr.id()==ID_next_symbol)
   {
@@ -668,9 +673,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   {
     PRECONDITION(!expr.operands().empty());
 
-    for(auto &op : expr.operands())
-      typecheck_expr_rec(op, mode);
-
     auto &op0_type = to_multi_ary_expr(expr).op0().type();
 
     // boolean or bit-wise?
@@ -708,9 +710,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_smv_iff)
   {
     auto &binary_expr = to_binary_expr(expr);
-    typecheck_expr_rec(binary_expr.lhs(), mode);
-    typecheck_expr_rec(binary_expr.rhs(), mode);
-
     auto &op0_type = binary_expr.op0().type();
 
     if(op0_type.id() == ID_signedbv || op0_type.id() == ID_unsignedbv)
@@ -731,9 +730,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   }
   else if(expr.id()==ID_constraint_select_one)
   {
-    for(auto &op : expr.operands())
-      typecheck_expr_rec(op, mode);
-
     typet op_type;
     op_type.make_nil();
 
@@ -757,9 +753,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     exprt &op0 = to_binary_expr(expr).op0();
     exprt &op1 = to_binary_expr(expr).op1();
 
-    typecheck_expr_rec(op0, mode);
-    typecheck_expr_rec(op1, mode);
-
     typet op_type = type_union(op0.type(), op1.type(), expr.source_location());
 
     convert_expr_to(op0, op_type);
@@ -784,10 +777,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     auto &if_expr = to_if_expr(expr);
     auto &true_case = if_expr.true_case();
     auto &false_case = if_expr.false_case();
-    typecheck_expr_rec(if_expr.cond(), mode);
     convert_expr_to(if_expr.cond(), bool_typet{});
-    typecheck_expr_rec(true_case, mode);
-    typecheck_expr_rec(false_case, mode);
     expr.type() =
       type_union(true_case.type(), false_case.type(), expr.source_location());
     convert_expr_to(true_case, expr.type());
@@ -800,9 +790,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     auto &op0 = to_binary_expr(expr).op0();
     auto &op1 = to_binary_expr(expr).op1();
 
-    typecheck_expr_rec(op0, mode);
-    typecheck_expr_rec(op1, mode);
-
     if(op0.type().id() == ID_range || op0.type().id() == ID_bool)
     {
       // find proper type for precise arithmetic
@@ -873,9 +860,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id()==ID_cond)
   {
     // case ... esac
-    for(auto &op : expr.operands())
-      typecheck_expr_rec(op, mode);
-
     bool condition = true;
 
     expr.type().make_nil();
@@ -911,7 +895,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
         << "CTL operator not permitted here";
     expr.type() = bool_typet();
     auto &op = to_unary_expr(expr).op();
-    typecheck_expr_rec(op, mode);
     convert_expr_to(op, expr.type());
   }
   else if(
@@ -923,7 +906,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
         << "CTL operator not permitted here";
     expr.type() = bool_typet();
     auto &op2 = to_ternary_expr(expr).op2();
-    typecheck_expr_rec(op2, mode);
     convert_expr_to(op2, expr.type());
   }
   else if(expr.id() == ID_smv_ABU || expr.id() == ID_smv_EBU)
@@ -934,7 +916,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     expr.type() = bool_typet();
     for(std::size_t i = 0; i < expr.operands().size(); i++)
     {
-      typecheck_expr_rec(expr.operands()[i], mode);
       if(i == 0 || i == 3)
         convert_expr_to(expr.operands()[i], expr.type());
     }
@@ -949,7 +930,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
         << "LTL operator not permitted here";
     expr.type() = bool_typet{};
     auto &op = to_unary_expr(expr).op();
-    typecheck_expr_rec(op, mode);
     convert_expr_to(op, expr.type());
   }
   else if(
@@ -961,8 +941,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
         << "CTL operator not permitted here";
     auto &binary_expr = to_binary_expr(expr);
     expr.type() = bool_typet{};
-    typecheck_expr_rec(binary_expr.lhs(), mode);
-    typecheck_expr_rec(binary_expr.rhs(), mode);
     convert_expr_to(binary_expr.lhs(), expr.type());
     convert_expr_to(binary_expr.rhs(), expr.type());
   }
@@ -975,8 +953,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
         << "LTL operator not permitted here";
     auto &binary_expr = to_binary_expr(expr);
     expr.type() = bool_typet{};
-    typecheck_expr_rec(binary_expr.lhs(), mode);
-    typecheck_expr_rec(binary_expr.rhs(), mode);
     convert_expr_to(binary_expr.lhs(), expr.type());
     convert_expr_to(binary_expr.rhs(), expr.type());
   }
@@ -996,7 +972,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_unary_minus)
   {
     auto &uminus_expr = to_unary_minus_expr(expr);
-    typecheck_expr_rec(uminus_expr.op(), mode);
     auto &op_type = uminus_expr.op().type();
 
     if(op_type.id() == ID_range)
@@ -1024,8 +999,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_smv_swconst)
   {
     auto &binary_expr = to_binary_expr(expr);
-    typecheck_expr_rec(binary_expr.lhs(), mode);
-    typecheck_expr_rec(binary_expr.rhs(), mode);
     PRECONDITION(binary_expr.lhs().is_constant());
     PRECONDITION(binary_expr.rhs().is_constant());
     auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.rhs()));
@@ -1038,8 +1011,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_smv_uwconst)
   {
     auto &binary_expr = to_binary_expr(expr);
-    typecheck_expr_rec(binary_expr.lhs(), mode);
-    typecheck_expr_rec(binary_expr.rhs(), mode);
     PRECONDITION(binary_expr.lhs().is_constant());
     PRECONDITION(binary_expr.rhs().is_constant());
     auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.rhs()));
@@ -1056,8 +1027,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     auto &binary_expr = to_binary_expr(expr);
 
     // The LHS must be a word type.
-    typecheck_expr_rec(binary_expr.lhs(), mode);
-
     binary_expr.type() = binary_expr.lhs().type();
 
     if(binary_expr.type().id() == ID_signedbv)
@@ -1077,8 +1046,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     }
 
     // The RHS must be an integer constant
-    typecheck_expr_rec(binary_expr.rhs(), mode);
-
     if(
       binary_expr.rhs().type().id() != ID_range &&
       binary_expr.rhs().type().id() != ID_natural)
@@ -1112,9 +1079,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   {
     auto &binary_expr = to_binary_expr(expr);
 
-    typecheck_expr_rec(binary_expr.lhs(), mode);
-    typecheck_expr_rec(binary_expr.rhs(), mode);
-
     if(
       binary_expr.lhs().type().id() != ID_signedbv &&
       binary_expr.lhs().type().id() != ID_unsignedbv)
@@ -1139,7 +1103,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_smv_sizeof)
   {
     auto &op = to_unary_expr(expr).op();
-    typecheck_expr_rec(op, mode);
     if(op.type().id() == ID_signedbv || op.type().id() == ID_unsignedbv)
     {
       auto bits = to_bitvector_type(op.type()).get_width();
@@ -1154,8 +1117,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_smv_resize)
   {
     auto &binary_expr = to_binary_expr(expr);
-    typecheck_expr_rec(binary_expr.lhs(), mode);
-    typecheck_expr_rec(binary_expr.rhs(), mode);
     PRECONDITION(binary_expr.rhs().is_constant());
     auto &lhs_type = binary_expr.lhs().type();
     auto new_bits =
@@ -1174,8 +1135,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_smv_extend)
   {
     auto &binary_expr = to_binary_expr(expr);
-    typecheck_expr_rec(binary_expr.lhs(), mode);
-    typecheck_expr_rec(binary_expr.rhs(), mode);
     PRECONDITION(binary_expr.rhs().is_constant());
     auto &lhs_type = binary_expr.lhs().type();
     auto old_bits = to_bitvector_type(lhs_type).get_width();
@@ -1196,7 +1155,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   {
     // a reinterpret cast
     auto &op = to_unary_expr(expr).op();
-    typecheck_expr_rec(op, mode);
     if(op.type().id() == ID_signedbv)
       expr.type() = unsignedbv_typet{to_signedbv_type(op.type()).get_width()};
     else
@@ -1209,7 +1167,6 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   {
     // a reinterpret cast
     auto &op = to_unary_expr(expr).op();
-    typecheck_expr_rec(op, mode);
     if(op.type().id() == ID_unsignedbv)
       expr.type() = signedbv_typet{to_unsignedbv_type(op.type()).get_width()};
     else