diff --git a/include/utap/common.h b/include/utap/common.h
index 7ba0392..1341e60 100644
--- a/include/utap/common.h
+++ b/include/utap/common.h
@@ -182,10 +182,11 @@ enum kind_t {
     LOAD_STRAT,
 
     /*******************************************************
-     * Get supremum or infimum of variables/clocks
+     * Get supremum, infimum or (generalized) bounds for variable/clock values
      */
     SUP_VAR,
     INF_VAR,
+    BOUNDS_VAR,
 
     /*******************************************************
      * Verify a LSC scenario
diff --git a/include/utap/property.h b/include/utap/property.h
index 49d4f3e..dedaa79 100644
--- a/include/utap/property.h
+++ b/include/utap/property.h
@@ -99,9 +99,10 @@ enum class quant_t {
     strategy_load,
     strategy_save,
 
-    /* Extensions for getting supremum/infimum of variables/clocks */
+    /* Extensions for getting supremum/infimum/bounds for variable/clock values */
     supremum,
     infimum,
+    bounds,
 
     /* Prob properties */
     PMax,
diff --git a/src/expression.cpp b/src/expression.cpp
index a9e9abd..af2e749 100644
--- a/src/expression.cpp
+++ b/src/expression.cpp
@@ -356,6 +356,7 @@ size_t expression_t::get_size() const
     case SUM:
     case SUP_VAR:
     case INF_VAR:
+    case BOUNDS_VAR:
     case FRACTION:
     case FMOD_F:
     case FMAX_F:
@@ -868,7 +869,8 @@ int expression_t::get_precedence(kind_t kind)
     case CONTROL_TOPT_DEF1:
     case CONTROL_TOPT_DEF2:
     case SUP_VAR:
-    case INF_VAR: return 3;
+    case INF_VAR:
+    case BOUNDS_VAR: return 3;
 
     case SYNC: return 0;
 
@@ -1590,6 +1592,12 @@ std::ostream& expression_t::print(std::ostream& os, bool old) const
         get(1).print(os, old);
         break;
 
+    case BOUNDS_VAR:
+        os << "bounds{";
+        get(0).print(os, old) << "}: ";
+        get(1).print(os, old);
+        break;
+
     case MITL_FORMULA:
         os << "MITL: ";
         get(0).print(os, old);
diff --git a/src/keywords.cpp b/src/keywords.cpp
index 39ec9eb..9c2903b 100644
--- a/src/keywords.cpp
+++ b/src/keywords.cpp
@@ -76,6 +76,7 @@ namespace UTAP {
             {"sat",           Keyword{T_SCENARIO, syntax_t::PROPERTY}},
             {"inf",           Keyword{T_INF, syntax_t::PROPERTY}},
             {"sup",           Keyword{T_SUP, syntax_t::PROPERTY}},
+            {"bounds",        Keyword{T_BOUNDS, syntax_t::PROPERTY}},
             {"Pmax",          Keyword{T_PMAX, syntax_t::PROPERTY_PROB}},
             {"Pr",            Keyword{T_PROBA, syntax_t::PROPERTY}},
             {"X",             Keyword{T_MITL_NEXT, syntax_t::PROPERTY}},
diff --git a/src/parser.y b/src/parser.y
index 52b20d6..265b992 100644
--- a/src/parser.y
+++ b/src/parser.y
@@ -188,7 +188,7 @@ const char* utap_msg(const char *msg)
 %token T_KW_AND T_KW_OR T_KW_XOR T_KW_IMPLY T_KW_NOT
 
 /* Special */
-%token T_SUP T_INF
+%token T_SUP T_INF T_BOUNDS
 
 /* Math functions */
 %token T_ABS T_FABS T_FMOD T_FMA T_FMAX T_FMIN T_FDIM
@@ -756,6 +756,7 @@ NonTypeId:
         | 'M' { strncpy($$, "M", MAXLEN); }
         | T_SUP { strncpy($$, "sup", MAXLEN); }
         | T_INF { strncpy($$, "inf", MAXLEN); }
+        | T_BOUNDS { strncpy($$, "bounds", MAXLEN); }
         | T_SIMULATION { strncpy($$, "simulation", MAXLEN); }
         ;
 
@@ -1942,16 +1943,23 @@ SupPrefix:
         T_SUP ':' {
 	    CALL(@1, @2, expr_true());
 	}
-        | T_SUP '{' Expression '}' ':'
+	| T_SUP '{' Expression '}' ':'
 	;
 
 InfPrefix:
 	T_INF ':' {
 	    CALL(@1, @2, expr_true());
 	}
-        | T_INF '{' Expression '}' ':'
+	| T_INF '{' Expression '}' ':'
 	;
-        
+
+BoundsPrefix:
+	T_BOUNDS ':' {
+	    CALL(@1, @2, expr_true());
+	}
+	| T_BOUNDS '{' Expression '}' ':'
+	;
+
             
 StrategyAssignment: 
     T_STRATEGY Id T_ASSIGNMENT AssignablePropperty { 
@@ -1964,14 +1972,19 @@ Property:
         | PropertyExpr
 	| SupPrefix NonEmptyExpressionList Subjection {
 	    CALL(@1, @2, expr_nary(LIST,$2));
-            CALL(@1, @2, expr_binary(SUP_VAR));
+	    CALL(@1, @2, expr_binary(SUP_VAR));
 	    CALL(@1, @2, property());
         }
 	| InfPrefix NonEmptyExpressionList Subjection {
 	    CALL(@1, @2, expr_nary(LIST,$2));
-            CALL(@1, @2, expr_binary(INF_VAR));
+	    CALL(@1, @2, expr_binary(INF_VAR));
 	    CALL(@1, @2, property());
-        };
+	}
+	| BoundsPrefix NonEmptyExpressionList Subjection {
+	    CALL(@1, @2, expr_nary(LIST,$2));
+	    CALL(@1, @2, expr_binary(BOUNDS_VAR));
+	    CALL(@1, @2, property());
+	};
 
 %%
 
diff --git a/src/property.cpp b/src/property.cpp
index 3aa3c9e..6f17419 100644
--- a/src/property.cpp
+++ b/src/property.cpp
@@ -170,6 +170,7 @@ static bool symbolicProperty(const expression_t& expr)
     case CONTROL_TOPT_DEF2:
     case SUP_VAR:
     case INF_VAR:
+    case BOUNDS_VAR:
     case SCENARIO:
     case SCENARIO2: return true;
     default: return false;
@@ -195,6 +196,7 @@ void PropertyBuilder::typeProperty(expression_t expr)  // NOLINT
         break;
     case SUP_VAR: properties.back().type = quant_t::supremum; break;
     case INF_VAR: properties.back().type = quant_t::infimum; break;
+    case BOUNDS_VAR: properties.back().type = quant_t::bounds; break;
     case PROBA_MIN_BOX:
         properties.back().type = quant_t::probaMinBox;
         prob = true;
diff --git a/src/typechecker.cpp b/src/typechecker.cpp
index 645667f..c27b1fb 100644
--- a/src/typechecker.cpp
+++ b/src/typechecker.cpp
@@ -1057,11 +1057,12 @@ void TypeChecker::visitProperty(expression_t expr)
                 }
             }
             */
-        } else if (auto k = expr.get_kind(); k != SUP_VAR && k != INF_VAR && k != SCENARIO && k != PROBA_MIN_BOX &&
-                                             k != PROBA_MIN_DIAMOND && k != PROBA_BOX && k != PROBA_DIAMOND &&
-                                             k != PROBA_EXP && k != PROBA_CMP && k != SIMULATE && k != SIMULATEREACH &&
-                                             k != MITL_FORMULA && k != MIN_EXP &&  // ALREADY CHECKED IN PARSE
-                                             k != MAX_EXP)                         // ALREADY CHECKED IN PARSE
+        } else if (auto k = expr.get_kind(); k != SUP_VAR && k != INF_VAR && k != BOUNDS_VAR && k != SCENARIO &&
+                                             k != PROBA_MIN_BOX && k != PROBA_MIN_DIAMOND && k != PROBA_BOX &&
+                                             k != PROBA_DIAMOND && k != PROBA_EXP && k != PROBA_CMP && k != SIMULATE &&
+                                             k != SIMULATEREACH && k != MITL_FORMULA &&
+                                             k != MIN_EXP &&  // ALREADY CHECKED IN PARSE
+                                             k != MAX_EXP)    // ALREADY CHECKED IN PARSE
         {
             for (uint32_t i = 0; i < expr.get_size(); i++) {
                 /* No nesting except for constraints */
@@ -2307,6 +2308,7 @@ bool TypeChecker::checkExpression(expression_t expr)
 
     case SUP_VAR:
     case INF_VAR:
+    case BOUNDS_VAR:
         if (!is_integral(expr[0]) && !is_constraint(expr[0])) {
             handleError(expr[0], "$Boolean_expected");
             return false;
diff --git a/test/models/simpleSystem.xml b/test/models/simpleSystem.xml
index 5b18ac3..fa934e8 100644
--- a/test/models/simpleSystem.xml
+++ b/test/models/simpleSystem.xml
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="utf-8"?>
-<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/researoh/group/darts/uppaal/flat-1_2.dtd'>
+<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
 <nta>
 	<declaration>clock c;</declaration>
 	<template>
diff --git a/test/test_expression.cpp b/test/test_expression.cpp
index c72a3e8..1ab244b 100644
--- a/test/test_expression.cpp
+++ b/test/test_expression.cpp
@@ -153,7 +153,7 @@ TEST_CASE("Expression")
             MINUS, PLUS, MULT, DIV, MOD, BIT_AND, BIT_OR, BIT_XOR, BIT_LSHIFT, BIT_RSHIFT,
             AND, OR, XOR, POW, LT, LE, EQ, NEQ, GE, GT, MIN, MAX, ARRAY, COMMA,
             ASSIGN, ASS_PLUS, ASS_MINUS, ASS_DIV, ASS_MOD, ASS_MULT, ASS_AND, ASS_OR, ASS_XOR,
-            ASS_LSHIFT, ASS_RSHIFT, FORALL, EXISTS, SUM, SUP_VAR, INF_VAR, FRACTION,
+            ASS_LSHIFT, ASS_RSHIFT, FORALL, EXISTS, SUM, SUP_VAR, INF_VAR, BOUNDS_VAR, FRACTION,
             FMOD_F, FMAX_F, FMIN_F, FDIM_F, POW_F, HYPOT_F, ATAN2_F, LDEXP_F, NEXT_AFTER_F, COPY_SIGN_F,
             RANDOM_ARCSINE_F, RANDOM_BETA_F, RANDOM_GAMMA_F, RANDOM_NORMAL_F, RANDOM_WEIBULL_F,
         };  // clang-format on
diff --git a/test/test_prettyprint.cpp b/test/test_prettyprint.cpp
index ea4cad9..fb1f6c5 100644
--- a/test/test_prettyprint.cpp
+++ b/test/test_prettyprint.cpp
@@ -8,77 +8,137 @@
 
 using namespace UTAP;
 
+TEST_CASE("Symbolic queries")
+{
+    auto doc = read_document("simpleSystem.xml");
+    REQUIRE(doc->get_errors().empty());
+    auto builder = std::make_unique<QueryBuilder>(*doc);
+    auto* pb = builder.get();
+    auto os = std::stringstream{};
+    // the redundant white-space is there to stress the parser
+    SUBCASE("Reachability")
+    {
+        auto res = parseProperty("E<> \t Process.L3", pb);
+        REQUIRE(res == 0);
+        pb->typecheck();
+        REQUIRE(doc->get_errors().empty());
+        pb->getQuery().print(os);
+        CHECK(os.str() == "E<> Process.L3");
+    }
+    SUBCASE("Safety")
+    {
+        auto res = parseProperty("A[] \t Process.L3", pb);
+        REQUIRE(res == 0);
+        pb->typecheck();
+        REQUIRE(doc->get_errors().empty());
+        pb->getQuery().print(os);
+        CHECK(os.str() == "A[] Process.L3");
+    }
+    SUBCASE("Liveness")
+    {
+        auto res = parseProperty("Process.L2 \t --> \t Process.L3", pb);
+        REQUIRE(res == 0);
+        pb->typecheck();
+        REQUIRE(doc->get_errors().empty());
+        pb->getQuery().print(os);
+        CHECK(os.str() == "Process.L2 --> Process.L3");
+    }
+    SUBCASE("Infimum")
+    {
+        auto res = parseProperty("inf {  Process.L2  }  :  c", pb);
+        REQUIRE(res == 0);
+        pb->typecheck();
+        REQUIRE(doc->get_errors().empty());
+        pb->getQuery().print(os);
+        CHECK(os.str() == "inf{Process.L2}: c");
+    }
+    SUBCASE("Supremum")
+    {
+        auto res = parseProperty("sup {  Process.L2  }  :  c", pb);
+        REQUIRE(res == 0);
+        pb->typecheck();
+        REQUIRE(doc->get_errors().empty());
+        pb->getQuery().print(os);
+        CHECK(os.str() == "sup{Process.L2}: c");
+    }
+    SUBCASE("Bounds")
+    {
+        auto res = parseProperty("bounds {  Process.L2  }  :  c", pb);
+        REQUIRE(res == 0);
+        pb->typecheck();
+        REQUIRE(doc->get_errors().empty());
+        pb->getQuery().print(os);
+        CHECK(os.str() == "bounds{Process.L2}: c");
+    }
+}
+
 TEST_CASE("Minimization pretty printing")
 {
     auto doc = read_document("simpleSystem.xml");
+    REQUIRE(doc->get_errors().empty());
     auto builder = std::make_unique<QueryBuilder>(*doc);
+    auto* pb = builder.get();
+    auto os = std::ostringstream{};
     SUBCASE("global time bound")
     {
-        auto res = parseProperty("minE(c)[<=20] {} -> {} : <> c >= 20", builder.get());
+        auto res = parseProperty("minE(c)[<=20] {} -> {} : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "minE(c)[<=20] {} -> {} : <> c >= 20");
     }
     SUBCASE("step bound")
     {
-        auto res = parseProperty("minE(c)[#<=20] {} -> {} : <> c >= 20", builder.get());
+        auto res = parseProperty("minE(c)[#<=20] {} -> {} : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "minE(c)[#<=20] {} -> {} : <> c >= 20");
     }
     SUBCASE("cost bound without features")
     {
-        auto res = parseProperty("minE(c)[c<=20] : <> c >= 20", builder.get());
+        auto res = parseProperty("minE(c)[c<=20] : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "minE(c)[c<=20] : <> c >= 20");
     }
     SUBCASE("empty features")
     {
-        auto res = parseProperty("minE(c)[c<=20] {} -> {} : <> c >= 20", builder.get());
+        auto res = parseProperty("minE(c)[c<=20] {} -> {} : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "minE(c)[c<=20] {} -> {} : <> c >= 20");
     }
     SUBCASE("one discrete feature")
     {
-        auto res = parseProperty("minE(c)[c<=20] { Process.location } -> {} : <> c >= 20", builder.get());
+        auto res = parseProperty("minE(c)[c<=20] { Process.location } -> {} : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "minE(c)[c<=20] {Process.location} -> {} : <> c >= 20");
     }
     SUBCASE("one continuous feature")
     {
-        auto res = parseProperty("minE(c)[c<=20] {} -> { c } : <> c >= 20", builder.get());
+        auto res = parseProperty("minE(c)[c<=20] {} -> { c } : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "minE(c)[c<=20] {} -> {c} : <> c >= 20");
     }
     SUBCASE("discrete and continuous features")
     {
-        auto res = parseProperty("minE(c)[c<=20] { Process.location } -> { c } : <> c >= 20", builder.get());
+        auto res = parseProperty("minE(c)[c<=20] { Process.location } -> { c } : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "minE(c)[c<=20] {Process.location} -> {c} : <> c >= 20");
     }
@@ -87,74 +147,70 @@ TEST_CASE("Minimization pretty printing")
 TEST_CASE("Maximization pretty printing")
 {
     auto doc = read_document("simpleSystem.xml");
+    REQUIRE(doc->get_errors().empty());
     auto builder = std::make_unique<QueryBuilder>(*doc);
+    auto* pb = builder.get();
+    auto os = std::ostringstream{};
     SUBCASE("global time bound")
     {
-        auto res = parseProperty("maxE(c)[<=20] {} -> {} : <> c >= 20", builder.get());
+        auto res = parseProperty("maxE(c)[<=20] {} -> {} : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "maxE(c)[<=20] {} -> {} : <> c >= 20");
     }
     SUBCASE("step bound")
     {
-        auto res = parseProperty("maxE(c)[#<=20] {} -> {} : <> c >= 20", builder.get());
+        auto res = parseProperty("maxE(c)[#<=20] {} -> {} : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "maxE(c)[#<=20] {} -> {} : <> c >= 20");
     }
     SUBCASE("cost bound without features")
     {
-        auto res = parseProperty("maxE(c)[c<=20] : <> c >= 20", builder.get());
+        auto res = parseProperty("maxE(c)[c<=20] : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "maxE(c)[c<=20] : <> c >= 20");
     }
     SUBCASE("empty features")
     {
-        auto res = parseProperty("maxE(c)[c<=20] {} -> {} : <> c >= 20", builder.get());
+        auto res = parseProperty("maxE(c)[c<=20] {} -> {} : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "maxE(c)[c<=20] {} -> {} : <> c >= 20");
     }
     SUBCASE("one discrete feature")
     {
-        auto res = parseProperty("maxE(c)[c<=20] { Process.location } -> {} : <> c >= 20", builder.get());
+        auto res = parseProperty("maxE(c)[c<=20] { Process.location } -> {} : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "maxE(c)[c<=20] {Process.location} -> {} : <> c >= 20");
     }
     SUBCASE("one continuous feature")
     {
-        auto res = parseProperty("maxE(c)[c<=20] {} -> { c } : <> c >= 20", builder.get());
+        auto res = parseProperty("maxE(c)[c<=20] {} -> { c } : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "maxE(c)[c<=20] {} -> {c} : <> c >= 20");
     }
     SUBCASE("discrete and continuous features")
     {
-        auto res = parseProperty("maxE(c)[c<=20] { Process.location } -> { c } : <> c >= 20", builder.get());
+        auto res = parseProperty("maxE(c)[c<=20] { Process.location } -> { c } : <> c >= 20", pb);
         REQUIRE(res == 0);
         builder->typecheck();
         REQUIRE(doc->get_errors().empty());
-        auto os = std::ostringstream{};
         builder->getQuery().print(os);
         CHECK(os.str() == "maxE(c)[c<=20] {Process.location} -> {c} : <> c >= 20");
     }
@@ -227,7 +283,7 @@ TEST_CASE("Chaining conjunctions")
     CHECK(query1.str() == "E<> true && true && true");
 }
 
-TEST_CASE("Chaining disjuntive conjunctions")
+TEST_CASE("Chaining disjunctive conjunctions")
 {
     auto f = document_fixture{}.add_default_process().build_query_fixture();
     REQUIRE(f.get_errors().empty());
@@ -236,7 +292,7 @@ TEST_CASE("Chaining disjuntive conjunctions")
     CHECK(query1.str() == "E<> true && true || true && true");
 }
 
-TEST_CASE("Chaining disjuntive conjunctions")
+TEST_CASE("Chaining disjunctive conjunctions")
 {
     auto f = document_fixture{}.add_default_process().build_query_fixture();
     REQUIRE(f.get_errors().empty());
@@ -245,7 +301,7 @@ TEST_CASE("Chaining disjuntive conjunctions")
     CHECK(query1.str() == "E<> true || true && true || true");
 }
 
-TEST_CASE("Chaining disjuntive conjunctions with outer conjunction")
+TEST_CASE("Chaining disjunctive conjunctions with outer conjunction")
 {
     auto f = document_fixture{}.add_default_process().build_query_fixture();
     REQUIRE(f.get_errors().empty());
@@ -257,7 +313,7 @@ TEST_CASE("Chaining disjuntive conjunctions with outer conjunction")
     CHECK(query2.str() == "E<> false && (true || true && true || true)");
 }
 
-TEST_CASE("Post incrementing an indentifier should not require paranthesis")
+TEST_CASE("Post incrementing an identifier should not require parenthesis")
 {
     auto frame = frame_t::create();
     auto test_symbol = frame.add_symbol("foo", type_t::create_primitive(Constants::INT), {});