diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol
new file mode 100644
index 000000000..3acc9b53b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol
@@ -0,0 +1,27 @@
+contract D {
+	constructor(uint _x) { x = _x; }
+	uint public x;
+}
+
+contract E {
+	constructor() { x = 2; }
+	uint public x;
+}
+
+contract C {
+	constructor() {
+		address d = address(new D(42));
+		assert(D(d).x() == 42); // should hold
+		assert(D(d).x() == 43); // should fail
+		uint y = E(d).x();
+		assert(y == 2); // should fail, it would still call D.x() == 42
+		assert(y == 42); // should hold, but fails due to false positive
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 6328: (231-253): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0119\ny = 0\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x188b\ny = 0\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (359-374): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0217\ny = 0\n\nTransaction trace:\nC.constructor()
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol
new file mode 100644
index 000000000..831805ae3
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol
@@ -0,0 +1,25 @@
+contract D {
+	constructor(uint _x) { x = _x; }
+	function setD(uint _x) public { x = _x; }
+	uint public x;
+}
+
+contract C {
+	constructor() {
+		address d = address(new D(42));
+		assert(D(d).x() == 42); // should hold
+		assert(D(d).x() == 21); // should fail
+		d.call(abi.encodeCall(D.setD, (21)));
+		assert(D(d).x() == 21); // should hold, but false positive cus low level calls are not handled precisely
+		assert(D(d).x() == 42); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// ----
+// Warning 9302: (257-293): Return value of low-level calls not used.
+// Warning 6031: (279-285): Internal error: Expression undefined for SMT solver.
+// Warning 6328: (216-238): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0119\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (297-319): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x1720\n\nTransaction trace:\nC.constructor()
+// Warning 6328: (404-426): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0217\n\nTransaction trace:\nC.constructor()
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_1.sol
new file mode 100644
index 000000000..2dc5dd0fb
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_1.sol
@@ -0,0 +1,28 @@
+contract D {
+	constructor(uint _x) { x = _x; }
+	uint public x;
+}
+
+contract E {
+	constructor() { x = 2; }
+	uint public x;
+}
+
+contract C {
+	function f() public {
+		address d = address(new D(42));
+		assert(D(d).x() == 42); // should hold
+		assert(D(d).x() == 43); // should fail
+		uint y = E(d).x();
+		assert(y == 2); // should fail, it would still call D.x() == 42
+		assert(y == 42); // should hold, but fails due to false positive
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (237-259): CHC: Assertion violation happens here.
+// Warning 6328: (299-313): CHC: Assertion violation happens here.
+// Warning 6328: (365-380): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol
new file mode 100644
index 000000000..5aeb52284
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol
@@ -0,0 +1,27 @@
+contract D {
+	constructor(uint _x) { x = _x; }
+	function setD(uint _x) public { x = _x; }
+	uint public x;
+}
+
+contract C {
+	function f() public {
+		address d = address(new D(42));
+		assert(D(d).x() == 42); // should hold
+		assert(D(d).x() == 21); // should fail
+		d.call(abi.encodeCall(D.setD, (21)));
+		assert(D(d).x() == 21); // should hold, but false positive cus low level calls are not handled precisely
+		assert(D(d).x() == 42); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTIgnoreCex: yes
+// ----
+// Warning 9302: (263-299): Return value of low-level calls not used.
+// Warning 6031: (285-291): Internal error: Expression undefined for SMT solver.
+// Warning 6328: (222-244): CHC: Assertion violation happens here.
+// Warning 6328: (303-325): CHC: Assertion violation happens here.
+// Warning 6328: (410-432): CHC: Assertion violation happens here.
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(D(d).x() == 42)\n<errorCode> = 2 -> Assertion failed at assert(D(d).x() == 21)\n<errorCode> = 4 -> Assertion failed at assert(D(d).x() == 21)\n<errorCode> = 5 -> Assertion failed at assert(D(d).x() == 42)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol
new file mode 100644
index 000000000..785e17aef
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol
@@ -0,0 +1,31 @@
+contract D {
+	constructor(uint _x) { x = _x; }
+	function setD(uint _x) public { x = _x; }
+	uint public x;
+}
+
+contract C {
+	uint x;
+
+	function f() public {
+		x = 666;
+		address d = address(new D(42));
+		assert(D(d).x() == 42); // should hold
+		assert(D(d).x() == 21); // should fail
+		d.call(abi.encodeCall(D.setD, (21)));
+		assert(D(d).x() == 21); // should hold, but false positive cus low level calls are not handled precisely
+		assert(D(d).x() == 42); // should fail
+		assert(x == 666); // should hold, C's storage should not have been havoced
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTIgnoreCex: yes
+// ----
+// Warning 9302: (284-320): Return value of low-level calls not used.
+// Warning 6031: (306-312): Internal error: Expression undefined for SMT solver.
+// Warning 6328: (243-265): CHC: Assertion violation happens here.
+// Warning 6328: (324-346): CHC: Assertion violation happens here.
+// Warning 6328: (431-453): CHC: Assertion violation happens here.
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((((x' + ((- 1) * x)) = 0) || !(x' <= 665)) && (!(x' >= 667) || ((x' + ((- 1) * x)) = 0)) && !(<errorCode> >= 6))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(D(d).x() == 42)\n<errorCode> = 2 -> Assertion failed at assert(D(d).x() == 21)\n<errorCode> = 4 -> Assertion failed at assert(D(d).x() == 21)\n<errorCode> = 5 -> Assertion failed at assert(D(d).x() == 42)\n<errorCode> = 6 -> Assertion failed at assert(x == 666)\n