diff --git a/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol b/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol
index facedf003..71fdcceeb 100644
--- a/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol
@@ -20,7 +20,7 @@ contract C {
 // ----
 // Warning 8364: (b.sol:95-96): Assertion checker does not yet implement type module "a.sol"
 // Warning 8364: (b.sol:103-104): Assertion checker does not yet implement type module "a.sol"
-// Warning 6328: (b.sol:208-222): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        a.sol::f(2) -- internal call\n        a.sol::f([97, 98, 99]) -- internal call
-// Warning 6328: (b.sol:274-288): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        a.sol::f(2) -- internal call\n        a.sol::f([97, 98, 99]) -- internal call
+// Warning 6328: (b.sol:208-222): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        a.sol:f(2) -- internal call\n        a.sol:f([97, 98, 99]) -- internal call
+// Warning 6328: (b.sol:274-288): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        a.sol:f(2) -- internal call\n        a.sol:f([97, 98, 99]) -- internal call
 // Warning 8364: (b.sol:95-96): Assertion checker does not yet implement type module "a.sol"
 // Warning 8364: (b.sol:103-104): Assertion checker does not yet implement type module "a.sol"
diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
index 13f93ccec..1da78ef51 100644
--- a/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
@@ -11,5 +11,5 @@ function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[]
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    ::fun(_x, []) -- internal call
-// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    ::fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call
+// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    fun(_x, []) -- internal call
+// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol b/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol
index da222be4f..43d6a63d8 100644
--- a/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol
@@ -31,7 +31,7 @@ contract C {
 // ----
 // Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.
 // Warning 8364: (s2.sol:182-183): Assertion checker does not yet implement type module "s1.sol"
-// Warning 6328: (s2.sol:334-349): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 90\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        s1.sol::fre() -- internal call
+// Warning 6328: (s2.sol:334-349): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 90\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n        s1.sol:fre() -- internal call
 // Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.
 // Warning 8364: (s2.sol:182-183): Assertion checker does not yet implement type module "s1.sol"
 // Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression.