Do not change SMT tests

This commit is contained in:
Alex Beregszaszi 2018-06-18 19:25:22 +02:00
parent d44743c87f
commit c7f842d4cc

View File

@ -427,21 +427,21 @@ BOOST_AUTO_TEST_CASE(storage_value_vars)
string text = R"( string text = R"(
contract C contract C
{ {
uint a; address a;
bool b; bool b;
uint c; uint c;
function f(uint x) public { function f(uint x) public {
if (x == 0) if (x == 0)
{ {
a = 100; a = 0x0000000000000000000000000000000000000100;
b = true; b = true;
} }
else else
{ {
a = 200; a = 0x0000000000000000000000000000000000000200;
b = false; b = false;
} }
assert(a > 0 && b); assert(a > 0x0000000000000000000000000000000000000000 && b);
} }
} }
)"; )";
@ -449,7 +449,7 @@ BOOST_AUTO_TEST_CASE(storage_value_vars)
text = R"( text = R"(
contract C contract C
{ {
uint a; address a;
bool b; bool b;
uint c; uint c;
function f() public view { function f() public view {
@ -464,22 +464,22 @@ BOOST_AUTO_TEST_CASE(storage_value_vars)
function f(uint x) public { function f(uint x) public {
if (x == 0) if (x == 0)
{ {
a = 100; a = 0x0000000000000000000000000000000000000100;
b = true; b = true;
} }
else else
{ {
a = 200; a = 0x0000000000000000000000000000000000000200;
b = false; b = false;
} }
assert(b == (a < 200)); assert(b == (a < 0x0000000000000000000000000000000000000200));
} }
function g() public view { function g() public view {
require(a < 100); require(a < 0x0000000000000000000000000000000000000100);
assert(c >= 0); assert(c >= 0);
} }
uint a; address a;
bool b; bool b;
uint c; uint c;
} }