diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 93ef209f9..b5f18fbee 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -1029,16 +1029,10 @@ std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const
 
 #ifdef USE_Z3
 
-class ExprData {
-public:
+struct ExprData {
     typedef std::map<std::string, z3::expr> ValueExpr;
     typedef std::vector<z3::expr> AssertionList;
 
-    class BailoutValueException {
-    public:
-        BailoutValueException() {}
-    };
-
     z3::context context;
     ValueExpr valueExpr;
     AssertionList assertionList;
@@ -1048,15 +1042,6 @@ public:
             solver.add(assertExpr);
     }
 
-    void addConstraints(z3::solver &solver, const Data* data) {
-        for (auto constraint : data->constraints) {
-            try {
-                solver.add(getConstraintExpr(constraint));
-            } catch (const BailoutValueException &) {
-            }
-        }
-    }
-
     z3::expr addInt(const std::string &name, int128_t minValue, int128_t maxValue) {
         z3::expr e = context.int_const(name.c_str());
         valueExpr.emplace(name, e);
@@ -1123,8 +1108,6 @@ public:
     z3::expr getExpr(ExprEngine::ValuePtr v) {
         if (!v)
             throw ExprEngineException(nullptr, "Can not solve expressions, operand value is null");
-        if (v->type == ExprEngine::ValueType::BailoutValue)
-            throw BailoutValueException();
         if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) {
             if (intRange->name[0] != '$')
 #if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1)
@@ -1179,6 +1162,7 @@ public:
     }
 
 private:
+
     z3::expr bool_expr(z3::expr e) {
         if (e.is_bool())
             return e;
@@ -1207,7 +1191,8 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const
     z3::solver solver(exprData.context);
     try {
         z3::expr e = exprData.addInt(name, minValue, maxValue);
-        exprData.addConstraints(solver, data);
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         solver.add(e == value);
         return solver.check() == z3::sat;
@@ -1235,7 +1220,8 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const
     z3::solver solver(exprData.context);
     try {
         z3::expr e = exprData.addInt(name, minValue, maxValue);
-        exprData.addConstraints(solver, data);
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         solver.add(e > value);
         return solver.check() == z3::sat;
@@ -1263,7 +1249,8 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
     z3::solver solver(exprData.context);
     try {
         z3::expr e = exprData.addInt(name, minValue, maxValue);
-        exprData.addConstraints(solver, data);
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         solver.add(e < value);
         return solver.check() == z3::sat;
@@ -1292,7 +1279,8 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
     z3::solver solver(exprData.context);
     try {
         z3::expr e = exprData.addFloat(name);
-        exprData.addConstraints(solver, data);
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         solver.add(e >= value && e <= value);
         return solver.check() != z3::unsat;
@@ -1322,7 +1310,8 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const
     z3::solver solver(exprData.context);
     try {
         z3::expr e = exprData.addFloat(name);
-        exprData.addConstraints(solver, data);
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         solver.add(e > value);
         return solver.check() == z3::sat;
@@ -1352,7 +1341,8 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
     z3::solver solver(exprData.context);
     try {
         z3::expr e = exprData.addFloat(name);
-        exprData.addConstraints(solver, data);
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         solver.add(e < value);
         return solver.check() == z3::sat;
@@ -1373,7 +1363,8 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value)
     ExprData exprData;
     z3::solver solver(exprData.context);
     z3::expr e = exprData.getExpr(this);
-    exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
+    for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+        solver.add(exprData.getConstraintExpr(constraint));
     exprData.addAssertions(solver);
     solver.add(e == value);
     return solver.check() == z3::sat;
@@ -1391,7 +1382,8 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int
         ExprData exprData;
         z3::solver solver(exprData.context);
         z3::expr e = exprData.getExpr(this);
-        exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         solver.add(e > value);
         return solver.check() == z3::sat;
@@ -1413,7 +1405,8 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val
         ExprData exprData;
         z3::solver solver(exprData.context);
         z3::expr e = exprData.getExpr(this);
-        exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         solver.add(e < value);
         return solver.check() == z3::sat;
@@ -1435,7 +1428,8 @@ bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const
         ExprData exprData;
         z3::solver solver(exprData.context);
         z3::expr e = exprData.getExpr(this);
-        exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         return solver.check() == z3::sat;
     } catch (const z3::exception &exception) {
@@ -1455,7 +1449,8 @@ std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) con
         ExprData exprData;
         z3::solver solver(exprData.context);
         z3::expr e = exprData.getExpr(this);
-        exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
+        for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
+            solver.add(exprData.getConstraintExpr(constraint));
         exprData.addAssertions(solver);
         solver.add(e);
         std::ostringstream os;
@@ -1772,11 +1767,7 @@ static void checkContract(Data &data, const Token *tok, const Function *function
     z3::solver solver(exprData.context);
     try {
         // Invert contract, we want to know if the contract might not be met
-        try {
-            solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true)));
-        } catch (const ExprData::BailoutValueException &) {
-            throw ExprEngineException(tok, "Internal error: Bailout value used");
-        }
+        solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true)));
 
         bool bailoutValue = false;
         for (nonneg int i = 0; i < argValues.size(); ++i) {
@@ -1823,7 +1814,7 @@ static void checkContract(Data &data, const Token *tok, const Function *function
         }
     } catch (const z3::exception &exception) {
         std::cerr << "z3: " << exception << std::endl;
-    } catch (const ExprEngineException &) {
+    } catch (const ExprEngineException &e) {
         const char id[] = "internalErrorInExprEngine";
         const auto contractIt = data.settings->functionContracts.find(function->fullName());
         const std::string functionName = contractIt->first;