diff --git a/regression/external_abstract/ExternalAbstract_v1.sol b/regression/external_abstract/ExternalAbstract_v1.sol
index 8e686c45..5f75cd79 100644
--- a/regression/external_abstract/ExternalAbstract_v1.sol
+++ b/regression/external_abstract/ExternalAbstract_v1.sol
@@ -8,14 +8,21 @@ abstract contract D {
 contract ExternalAbstract {
 	uint x;
 	D d;
+
+	constructor(D _d) {
+		d = _d;
+	}
+
 	function f() public {
 		if (x < 10)
 			++x;
 	}
+	
 	function g() public {
 		require(x < 10);
 		d.d();
 	}
+
 	function getX() public view returns (uint) {
 		return x;
 	}
diff --git a/regression/external_abstract/README.md b/regression/external_abstract/README.md
index 25af5184..308c6769 100644
--- a/regression/external_abstract/README.md
+++ b/regression/external_abstract/README.md
@@ -51,7 +51,7 @@ We cannot trust `d.d` call because `d` could be implemented to call the function
 #### Z3
 |        | x-abstract-call |
 |--------|-----------------|
-| **v1** | TN!             |
+| **v1** | TN              |
  
 
 #### ELD
diff --git a/regression/external_abstract/hardhat/Makefile b/regression/external_abstract/hardhat/Makefile
new file mode 100644
index 00000000..c49b2687
--- /dev/null
+++ b/regression/external_abstract/hardhat/Makefile
@@ -0,0 +1,33 @@
+SHELL := /bin/bash
+
+.PHONY: init test clean 
+
+default: test
+
+init:
+	@if [ -f hardhat.config.js ]; then \
+		echo "Skipping: Hardhat already initialized."; \
+	else \
+		echo "Initializing Hardhat project..."; \
+		npm init -y >/dev/null && \
+		npm install --save-dev hardhat --silent --no-progress >/dev/null && \
+		printf '3\n' | npx hardhat init  && \
+		npm install --save-dev @nomicfoundation/hardhat-toolbox --silent --no-progress >/dev/null && \
+		if ! grep -q '@nomicfoundation/hardhat-toolbox' hardhat.config.js; then \
+			sed -i '1irequire("@nomicfoundation/hardhat-toolbox")\n' hardhat.config.js; \
+		fi; \
+		echo "Done."; \
+	fi
+
+test: init
+	npx hardhat test
+
+
+clean:
+	@echo "Cleaning project (preserving Makefile, contracts/, and test/)..."
+	@find . -mindepth 1 -maxdepth 1 \
+		! -name 'Makefile' \
+		! -name 'contracts' \
+		! -name 'test' \
+		-exec rm -rf {} +
+	@echo "Clean complete."
diff --git a/regression/external_abstract/hardhat/contracts/D_impl_v1.sol b/regression/external_abstract/hardhat/contracts/D_impl_v1.sol
new file mode 100644
index 00000000..246c549f
--- /dev/null
+++ b/regression/external_abstract/hardhat/contracts/D_impl_v1.sol
@@ -0,0 +1,14 @@
+pragma solidity ^0.8.25;
+
+import "./ExternalAbstract_v1.sol";
+
+contract DImpl is D {
+    ExternalAbstract ext;
+    function d() external override {
+        ext.f();
+    }
+
+    function set_ext(ExternalAbstract e) public{
+        ext = e;
+    }
+}
\ No newline at end of file
diff --git a/regression/external_abstract/hardhat/contracts/ExternalAbstract_v1.sol b/regression/external_abstract/hardhat/contracts/ExternalAbstract_v1.sol
new file mode 100644
index 00000000..41779cbb
--- /dev/null
+++ b/regression/external_abstract/hardhat/contracts/ExternalAbstract_v1.sol
@@ -0,0 +1,29 @@
+//https://github.com/leonardoalt/cav_2022_artifact/blob/main/regression/external_calls/external.sol
+pragma solidity ^0.8.25;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract ExternalAbstract {
+	uint x;
+	D d;
+
+	constructor(D _d) {
+		d = _d;
+	}
+
+	function f() public {
+		if (x < 10)
+			++x;
+	}
+
+	function g() public {
+		require(x < 10);
+		d.d();
+	}
+	
+	function getX() public view returns (uint) {
+		return x;
+	}
+}
\ No newline at end of file
diff --git a/regression/external_abstract/hardhat/test/test.js b/regression/external_abstract/hardhat/test/test.js
new file mode 100644
index 00000000..44946551
--- /dev/null
+++ b/regression/external_abstract/hardhat/test/test.js
@@ -0,0 +1,26 @@
+const {
+    loadFixture
+} = require("@nomicfoundation/hardhat-toolbox/network-helpers");
+const { expect } = require("chai");
+
+describe("ExternalAbstract", function () {
+    async function deployContract () {
+        const DImpl = await ethers.deployContract("DImpl");
+        const ExternalAbstract = await ethers.deployContract(
+            "ExternalAbstract", [ DImpl ]
+        );
+
+        await DImpl.set_ext(ExternalAbstract);
+
+        return { ExternalAbstract };
+    }
+
+    it("If an implementation of `D` which calls `f()` is used in the contract, when `g()` is called the value of `x` will change", async function () {
+        const { ExternalAbstract } = await loadFixture(deployContract);
+
+        const x_before = await ExternalAbstract.getX();
+        await ExternalAbstract.g();
+
+        expect(await ExternalAbstract.getX()).to.not.equal(x_before);
+    })
+})
\ No newline at end of file
diff --git a/regression/external_abstract/solcmc/ExternalAbstract_x-abstract-call_v1.sol b/regression/external_abstract/solcmc/ExternalAbstract_x-abstract-call_v1.sol
index a467c48e..8995e6ea 100644
--- a/regression/external_abstract/solcmc/ExternalAbstract_x-abstract-call_v1.sol
+++ b/regression/external_abstract/solcmc/ExternalAbstract_x-abstract-call_v1.sol
@@ -8,13 +8,23 @@ abstract contract D {
 contract ExternalAbstract {
 	uint x;
 	D d;
+
+	constructor(D _d) {
+		d = _d;
+	}
+
 	function f() public {
 		if (x < 10)
 			++x;
 	}
+
 	function g() public {
 		require(x < 10);
 		d.d();
 		assert(x < 10);
 	}
+
+	function getX() public view returns (uint) {
+		return x;
+	}
 }
\ No newline at end of file