[SMTChecker] updates to the tests

This commit is contained in:
Martin Blicha 2021-02-03 11:56:12 +01:00
parent d99256aae7
commit 4bcdac71df
2 changed files with 8 additions and 8 deletions

View File

@ -20,8 +20,8 @@ contract C
// ----
// Warning 2072: (224-240): Unused local variable.
// Warning 4588: (244-256): Assertion checker does not yet implement this type of function call.
// Warning 6328: (260-275): CHC: Assertion violation happens here.
// Warning 6328: (279-293): CHC: Assertion violation happens here.
// Warning 6328: (297-316): CHC: Assertion violation happens here.
// Warning 6328: (320-344): CHC: Assertion violation happens here.
// Warning 6328: (260-275): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (279-293): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (297-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (320-344): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 4588: (244-256): Assertion checker does not yet implement this type of function call.

View File

@ -20,8 +20,8 @@ contract C
// ----
// Warning 2072: (224-240): Unused local variable.
// Warning 4588: (244-264): Assertion checker does not yet implement this type of function call.
// Warning 6328: (268-283): CHC: Assertion violation happens here.
// Warning 6328: (287-301): CHC: Assertion violation happens here.
// Warning 6328: (305-324): CHC: Assertion violation happens here.
// Warning 6328: (328-352): CHC: Assertion violation happens here.
// Warning 6328: (268-283): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (287-301): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (305-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 6328: (328-352): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, data)
// Warning 4588: (244-264): Assertion checker does not yet implement this type of function call.