Set tests that CVC4 can't handle to Z3 only

This commit is contained in:
Leonardo Alt 2019-12-04 16:39:34 +01:00
parent 8d5f5a5cbe
commit beed0f6a27
61 changed files with 122 additions and 5 deletions

View File

@ -14,3 +14,5 @@ contract C is B {
assert(x == 2);
}
}
// ====
// SMTSolvers: z3

View File

@ -18,3 +18,5 @@ contract C is B {
assert(x == 0);
}
}
// ====
// SMTSolvers: z3

View File

@ -9,3 +9,5 @@ contract Simple {
assert(y == x);
}
}
// ====
// SMTSolvers: z3

View File

@ -7,4 +7,5 @@ contract Simple {
assert(y == x);
}
}
// ----
// ====
// SMTSolvers: z3

View File

@ -15,3 +15,5 @@ contract Simple {
assert(y == x);
}
}
// ====
// SMTSolvers: z3

View File

@ -12,3 +12,5 @@ contract Simple {
assert(y == x);
}
}
// ====
// SMTSolvers: z3

View File

@ -30,3 +30,5 @@ contract C {
assert(x < 9);
}
}
// ====
// SMTSolvers: z3

View File

@ -28,5 +28,7 @@ contract C {
assert(x < 2);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (311-324): Assertion violation happens here

View File

@ -11,6 +11,8 @@ contract C
assert(x < 14);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (179-193): Assertion violation happens here

View File

@ -13,5 +13,7 @@ contract C
assert(x > 0);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here

View File

@ -10,6 +10,8 @@ contract C {
assert(x == 0);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (104-109): Unreachable code.
// Warning: (122-128): Unreachable code.

View File

@ -14,6 +14,8 @@ contract C {
assert(a == 1);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (128-133): Unreachable code.
// Warning: (147-151): Unreachable code.

View File

@ -14,6 +14,8 @@ contract C {
assert(a == 2);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (128-133): Unreachable code.
// Warning: (147-151): Unreachable code.

View File

@ -10,6 +10,8 @@ contract C {
assert(x == 1);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (104-109): Unreachable code.
// Warning: (122-128): Unreachable code.

View File

@ -10,5 +10,7 @@ contract C {
assert(x == 0);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (107-112): Unreachable code.

View File

@ -15,3 +15,5 @@ contract C
assert(x >= 10);
}
}
// ====
// SMTSolvers: z3

View File

@ -14,5 +14,7 @@ contract C
assert(x >= 10);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (201-216): Assertion violation happens here

View File

@ -13,3 +13,5 @@ contract C
assert(x > 0);
}
}
// ====
// SMTSolvers: z3

View File

@ -14,5 +14,7 @@ contract C
assert(x > 15);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (185-199): Assertion violation happens here

View File

@ -11,6 +11,8 @@ contract C
assert(x < 14);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (189-203): Assertion violation happens here

View File

@ -13,6 +13,8 @@ contract C
assert(x > 0);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (296-309): Error trying to invoke SMT solver.
// Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here

View File

@ -8,5 +8,7 @@ contract C
assert(x == 0);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (102-105): Unreachable code.

View File

@ -6,3 +6,5 @@ contract C {
assert(x == 2);
}
}
// ====
// SMTSolvers: z3

View File

@ -6,3 +6,5 @@ contract C {
}
}
}
// ====
// SMTSolvers: z3

View File

@ -6,3 +6,5 @@ contract C {
}
}
}
// ====
// SMTSolvers: z3

View File

@ -6,5 +6,7 @@ contract C {
}
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (136-150): Assertion violation happens here

View File

@ -8,5 +8,7 @@ contract C {
assert(y == 3);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (167-181): Assertion violation happens here

View File

@ -9,4 +9,5 @@ contract C {
assert(y < 4);
}
}
// ----
// ====
// SMTSolvers: z3

View File

@ -14,6 +14,8 @@ contract LoopFor2 {
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (281-301): Assertion violation happens here
// Warning: (305-324): Assertion violation happens here

View File

@ -16,6 +16,8 @@ contract LoopFor2 {
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (274-294): Assertion violation happens here
// Warning: (321-340): Assertion violation happens here

View File

@ -17,5 +17,7 @@ contract LoopFor2 {
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (312-331): Assertion violation happens here

View File

@ -17,6 +17,8 @@ contract LoopFor2 {
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (290-309): Assertion violation happens here
// Warning: (313-332): Assertion violation happens here

View File

@ -6,5 +6,7 @@ contract C {
assert(x == 2);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (122-128): Condition is always true.

View File

@ -9,5 +9,7 @@ contract C {
assert(x == 2);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (138-144): Condition is always true.

View File

@ -13,5 +13,7 @@ contract C {
assert(x == 2);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (115-121): Unused local variable.

View File

@ -6,5 +6,7 @@ contract C {
assert(x == 2);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (122-127): Condition is always false.

View File

@ -13,4 +13,6 @@ contract C
assert(x > 0);
}
}
// ====
// SMTSolvers: z3
// ----

View File

@ -15,3 +15,5 @@ contract C
assert(x >= 10);
}
}
// ====
// SMTSolvers: z3

View File

@ -15,5 +15,7 @@ contract C
assert(x >= 10);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (218-233): Assertion violation happens here

View File

@ -14,3 +14,5 @@ contract C
assert(x >= 10);
}
}
// ====
// SMTSolvers: z3

View File

@ -17,6 +17,8 @@ contract C
assert(x >= 17);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (169-176): Unreachable code.
// Warning: (227-242): Assertion violation happens here

View File

@ -10,5 +10,7 @@ contract C
assert(x < 14);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (139-153): Assertion violation happens here

View File

@ -18,4 +18,5 @@ contract C
assert(x > 0);
}
}
// ----
// ====
// SMTSolvers: z3

View File

@ -11,3 +11,5 @@ contract C {
assert(x < 2);
}
}
// ====
// SMTSolvers: z3

View File

@ -12,5 +12,7 @@ contract C
assert(x == 1);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (128-131): Unreachable code.

View File

@ -11,6 +11,8 @@ contract C
assert(x == 2);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (120-123): Unreachable code.
// Warning: (131-145): Assertion violation happens here

View File

@ -11,4 +11,6 @@ contract C {
assert(x == 2);
}
}
// ====
// SMTSolvers: z3
// ----

View File

@ -9,5 +9,7 @@ contract C
assert(x == 0);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (98-104): Condition is always true.

View File

@ -16,6 +16,8 @@ contract LoopFor2 {
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (281-301): Assertion violation happens here
// Warning: (305-324): Assertion violation happens here

View File

@ -20,6 +20,8 @@ contract LoopFor2 {
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (362-382): Assertion violation happens here
// Warning: (409-428): Assertion violation happens here

View File

@ -9,5 +9,7 @@ contract C {
assert(x == 2);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (194-208): Assertion violation happens here

View File

@ -7,3 +7,5 @@ contract C {
}
}
}
// ====
// SMTSolvers: z3

View File

@ -7,5 +7,7 @@ contract C {
assert(x == 2);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (187-201): Assertion violation happens here

View File

@ -7,4 +7,5 @@ contract C {
assert(x != 2);
}
}
// ----
// ====
// SMTSolvers: z3

View File

@ -8,5 +8,7 @@ contract C {
assert(x == 7);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (216-230): Assertion violation happens here

View File

@ -28,3 +28,5 @@ contract C
assert(x >= 15);
}
}
// ====
// SMTSolvers: z3

View File

@ -28,6 +28,8 @@ contract C
assert(x >= 20);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (329-344): Assertion violation happens here
// Warning: (380-395): Assertion violation happens here

View File

@ -26,3 +26,5 @@ contract C
assert(x >= 15);
}
}
// ====
// SMTSolvers: z3

View File

@ -26,6 +26,8 @@ contract C
assert(x >= 20);
}
}
// ====
// SMTSolvers: z3
// ----
// Warning: (323-338): Assertion violation happens here
// Warning: (362-377): Assertion violation happens here

View File

@ -13,3 +13,5 @@ contract C
assert(a[1][1] == 0);
}
}
// ====
// SMTSolvers: z3

View File

@ -8,4 +8,5 @@ contract C
assert(x != map[x]);
}
}
// ----
// ====
// SMTSolvers: z3