From d4ec8075a4a9ef63dbda9c21c482caca968c0615 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Tue, 31 Dec 2019 22:32:16 +0100 Subject: [PATCH] Verification; Fix false positive in while loops --- lib/exprengine.cpp | 2 +- test/testexprengine.cpp | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 4368b6478..3ee619099 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -1563,7 +1563,7 @@ static void execute(const Token *start, const Token *end, Data &data) if (changedVariables.find(varid) != changedVariables.end()) continue; changedVariables.insert(varid); - data.assignValue(tok2, varid, createVariableValue(*tok2->astOperand1()->variable(), data)); + data.assignValue(tok2, varid, getValueRangeFromValueType(data.getNewSymbolName(), tok2->astOperand1()->valueType(), *data.settings)); } else if (Token::Match(tok2, "++|--") && tok2->astOperand1() && tok2->astOperand1()->variable()) { // give variable "any" value const Token *vartok = tok2->astOperand1(); diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 715c39900..d5cedf168 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -318,9 +318,9 @@ private: " x = x + 34;\n" " x == 340;\n" "}"; - ASSERT_EQUALS("(declare-fun $4 () Int)\n" - "(assert (and (>= $4 (- 2147483648)) (<= $4 2147483647)))\n" - "(assert (= (+ $4 34) 340))\n" + ASSERT_EQUALS("(declare-fun $2 () Int)\n" + "(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n" + "(assert (= (+ $2 34) 340))\n" "z3::sat", expr(code, "==")); }