diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index cbcfd33f6..593ddf027 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -286,6 +286,16 @@ namespace {
             constraints.push_back(std::make_shared<ExprEngine::BinOpResult>(equals?"==":"!=", lhsValue, rhsValue));
         }
 
+        void addConstraints(ExprEngine::ValuePtr value, const Token *tok) {
+            MathLib::bigint low;
+            if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::LOW, &low))
+                addConstraint(std::make_shared<ExprEngine::BinOpResult>(">=", value, std::make_shared<ExprEngine::IntRange>(std::to_string(low), low, low)), true);
+
+            MathLib::bigint high;
+            if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::HIGH, &high))
+                addConstraint(std::make_shared<ExprEngine::BinOpResult>("<=", value, std::make_shared<ExprEngine::IntRange>(std::to_string(high), high, high)), true);
+        }
+
     private:
         TrackExecution * const mTrackExecution;
         const int mDataIndex;
@@ -1455,8 +1465,11 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
     }
     if (var.isArray())
         return std::make_shared<ExprEngine::ArrayValue>(&data, &var);
-    if (valueType->isIntegral())
-        return getValueRangeFromValueType(data.getNewSymbolName(), valueType, *data.settings);
+    if (valueType->isIntegral()) {
+        auto value = getValueRangeFromValueType(data.getNewSymbolName(), valueType, *data.settings);
+        data.addConstraints(value, var.nameToken());
+        return value;
+    }
     if (valueType->type == ValueType::Type::RECORD)
         return createStructVal(valueType->typeScope, var.isLocal() && !var.isStatic(), data);
     if (valueType->smartPointerType) {
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index bde03372e..b346681f7 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -33,6 +33,8 @@ public:
 private:
     void run() OVERRIDE {
 #ifdef USE_Z3
+        TEST_CASE(annotation1);
+
         TEST_CASE(expr1);
         TEST_CASE(expr2);
         TEST_CASE(expr3);
@@ -143,6 +145,20 @@ private:
         return ret.str();
     }
 
+    void annotation1() {
+        const char code[] = "void f(__cppcheck_low__(100) short x) {\n"
+                            "    return x < 10;\n"
+                            "}";
+
+        const char expected[] = "(declare-fun $1 () Int)\n"
+                                "(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n"
+                                "(assert (>= $1 100))\n" // <- annotation
+                                "(assert (< $1 10))\n"
+                                "z3::unsat";
+
+        ASSERT_EQUALS(expected, expr(code, "<"));
+    }
+
     void expr1() {
         ASSERT_EQUALS("-32768:32767", getRange("void f(short x) { a = x; }", "x"));
     }