diff --git a/regression/no_intervening_calls/Makefile b/regression/no_intervening_calls/Makefile
new file mode 100644
index 00000000..4a69d141
--- /dev/null
+++ b/regression/no_intervening_calls/Makefile
@@ -0,0 +1,132 @@
+MAKEFLAGS = --no-print-directory
+
+# CHANGE THIS PATHS
+# Original contract path
+CONTRACT = ./NoInterveningCalls_v1.sol
+# Contract with solcmc instrumentation path
+SOLCMC_CONTRACT = ./solcmc
+# Certora specifications path
+CERTORA_SPEC = ./certora
+
+SKELETON = ./skeleton.json
+GROUND_TRUTH = ./ground-truth.csv
+README = ./README.md
+BUILD_DIR = ./build
+
+# SOLCMC params
+to = 10m
+Z3_DIR = $(BUILD_DIR)/z3
+Z3_OUT = $(Z3_DIR)/out.csv
+Z3_CM = $(Z3_DIR)/cm.csv
+Z3_TABLE = $(Z3_DIR)/table.md
+Z3_LOGS = $(Z3_DIR)/logs
+ELD_DIR = $(BUILD_DIR)/eld
+ELD_OUT = $(ELD_DIR)/out.csv
+ELD_CM = $(ELD_DIR)/cm.csv
+ELD_TABLE = $(ELD_DIR)/table.md
+ELD_LOGS = $(ELD_DIR)/logs
+
+# Certora params
+CERTORA_DIR = $(BUILD_DIR)/certora
+CERTORA_OUT = $(CERTORA_DIR)/out.csv
+CERTORA_CM = $(CERTORA_DIR)/cm.csv
+CERTORA_TABLE = $(CERTORA_DIR)/table.md
+CERTORA_LOGS = $(CERTORA_DIR)/logs
+
+PYTHON = python3
+
+.PHONY: all certora solcmc plain clean cleanr
+
+all: plain solcmc certora
+	@echo "Adding Solcmc table to README..."
+	@echo "### SolCMC" >> $(README)
+	@cat $(Z3_TABLE) >> $(README)
+	@cat $(ELD_TABLE) >> $(README)
+	@echo "" >> $(README)
+	@echo "Adding Certora table to README..."
+	@cat $(CERTORA_TABLE) >> $(README)
+
+#---------------------------- CERTORA ----------------------------#
+certora: $(CERTORA_TABLE)
+
+$(CERTORA_TABLE): $(CERTORA_CM)
+	@echo "Generating Certora results table ($(CERTORA_TABLE))..."
+	@echo "### Certora" > $(CERTORA_TABLE)
+	@$(PYTHON) ../../scripts/mdtable_gen.py --input $(CERTORA_CM) >> $(CERTORA_TABLE)
+
+$(CERTORA_CM): $(GROUND_TRUTH) $(CERTORA_OUT) 
+	@echo "Generating Certora confusion matrix ($(CERTORA_CM))..."
+	@$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(CERTORA_OUT) > $(CERTORA_CM)
+
+$(CERTORA_OUT): setup
+	@echo "Running Certora experiments..."
+	@$(PYTHON) ../../scripts/run_certora.py --contracts $(CONTRACT) --specs $(CERTORA_SPEC) --output $(CERTORA_DIR)
+
+#---------------------------- SOLCMC -----------------------------#
+solcmc: $(Z3_TABLE) $(ELD_TABLE)
+
+# Solcmc with Z3
+# Make markdown table
+$(Z3_TABLE): $(Z3_CM)
+	@echo "Generating SolCMC results table ($(Z3_TABLE))..."
+	echo "#### Z3" > $(Z3_TABLE)
+	@$(PYTHON) ../../scripts/mdtable_gen.py --input $(Z3_CM) >> $(Z3_TABLE)
+
+# Build confusion matrix with ground truths
+$(Z3_CM): $(GROUND_TRUTH) $(Z3_OUT)
+	@echo "Generating Solcmc confusion matrix ($(Z3_CM))..."
+	@$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(Z3_OUT) > $(Z3_CM)
+
+# Run experiments
+$(Z3_OUT): setup
+	@echo "Running SolCMC ($(solver)) experiments..."
+	@$(PYTHON) ../../scripts/run_solcmc.py --contracts $(SOLCMC_CONTRACT) --output $(Z3_DIR) --timeout $(to) --solver z3
+
+# Solcmc with eldarica
+# Make markdown table
+$(ELD_TABLE): $(ELD_CM)
+	@echo "Generating SolCMC results table ($(ELD_TABLE))..."
+	echo "#### ELD" > $(ELD_TABLE)
+	@$(PYTHON) ../../scripts/mdtable_gen.py --input $(ELD_CM) >> $(ELD_TABLE)
+
+# Build confusion matrix with ground truths
+$(ELD_CM): $(GROUND_TRUTH) $(ELD_OUT)
+	@echo "Generating Solcmc confusion matrix ($(ELD_CM))..."
+	@$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(ELD_OUT) > $(ELD_CM)
+
+# Run experiments
+$(ELD_OUT): setup
+	@echo "Running SolCMC ($(solver)) experiments..."
+	@$(PYTHON) ../../scripts/run_solcmc.py --contracts $(SOLCMC_CONTRACT) --output $(ELD_DIR) --timeout $(to) --solver eld
+
+#---------------------------- SETUP ------------------------------#
+setup: $(Z3_LOGS) $(ELD_LOGS) $(CERTORA_LOGS)
+
+# Create build logs/ dirs, and build/ dirs with them
+$(Z3_LOGS):
+	@mkdir -p $@
+
+$(ELD_LOGS):
+	@mkdir -p $@
+
+$(CERTORA_LOGS):
+	@mkdir -p $@
+
+#---------------------------- README -----------------------------#
+plain: cleanr $(README)
+	
+# Create plain README, without experiments results
+$(README): $(VERSIONS_DIR) $(SKELETON) $(GROUND_TRUTH)
+	@echo "Generating plain README..."
+	@$(PYTHON) ../../scripts/readme_gen.py -d . > $(README)
+	@echo "## Experiments" >> $(README)
+
+#---------------------------- CLEAN ------------------------------#
+clean: cleanr
+	@echo "Removing $(BUILD_DIR)..."
+	@rm -rf $(BUILD_DIR)
+
+# Remove README.md
+cleanr:
+	@echo "Removing README..."
+	@rm -f $(README)
diff --git a/regression/no_intervening_calls/NoInterveningCalls_v1.sol b/regression/no_intervening_calls/NoInterveningCalls_v1.sol
new file mode 100644
index 00000000..c892b180
--- /dev/null
+++ b/regression/no_intervening_calls/NoInterveningCalls_v1.sol
@@ -0,0 +1,14 @@
+pragma solidity ^0.8.25;
+
+contract NoInterveningCalls {
+	bool b = true;
+
+    function f() public{}
+    function g() public {
+        b = false;
+    }
+
+    function getB() public view returns (bool) {
+        return b;
+    }
+}
\ No newline at end of file
diff --git a/regression/no_intervening_calls/README.md b/regression/no_intervening_calls/README.md
new file mode 100644
index 00000000..5e6cf58f
--- /dev/null
+++ b/regression/no_intervening_calls/README.md
@@ -0,0 +1,41 @@
+# No Intervening Calls
+
+## Specification
+The `NoInterveningCalls` contract manages a boolean state variable `b` with two functions:
+
+- `f()`: A no-op function that performs no state changes.
+- `g()`: A function that modifies the state by setting `b` to `false`.
+
+When `f()` is called two times in a row and `g()` is not called, the value of `b` should not change.
+
+## Properties
+- **explicit-g-call**: `b` is `true` after `g()` is explicitly called between the two `f()` calls.
+- **no-explicit-g-call**: `b` is `true` after two consecutive calls to `f()`, without any intervening calls to `g()`.
+
+## Ground truth
+|        | explicit-g-call    | no-explicit-g-call |
+|--------|--------------------|--------------------|
+| **v1** | 0                  | 1                  |
+ 
+
+## Experiments
+### SolCMC
+#### Z3
+|        | explicit-g-call    | no-explicit-g-call |
+|--------|--------------------|--------------------|
+| **v1** | TN!                | TP!                |
+ 
+
+#### ELD
+|        | explicit-g-call    | no-explicit-g-call |
+|--------|--------------------|--------------------|
+| **v1** | TN!                | TP!                |
+ 
+
+
+### Certora
+|        | explicit-g-call    | no-explicit-g-call |
+|--------|--------------------|--------------------|
+| **v1** | TN                 | TP!                |
+ 
+
diff --git a/regression/no_intervening_calls/certora/explicit-g-call.spec b/regression/no_intervening_calls/certora/explicit-g-call.spec
new file mode 100644
index 00000000..541fee1c
--- /dev/null
+++ b/regression/no_intervening_calls/certora/explicit-g-call.spec
@@ -0,0 +1,12 @@
+methods {
+    function f() external envfree;
+    function g() external;
+}
+rule explicit_g_call {
+    env e;
+	require(currentContract.b);
+    f();
+    g(e);
+    f(); 
+    assert (currentContract.b);
+}
\ No newline at end of file
diff --git a/regression/no_intervening_calls/certora/no-explicit-g-call.spec b/regression/no_intervening_calls/certora/no-explicit-g-call.spec
new file mode 100644
index 00000000..0d1df87c
--- /dev/null
+++ b/regression/no_intervening_calls/certora/no-explicit-g-call.spec
@@ -0,0 +1,9 @@
+methods {
+    function f() external envfree;
+}
+rule no_explicit_g_call {
+	require(currentContract.b);
+    f();
+    f(); 
+    assert (currentContract.b);
+}
\ No newline at end of file
diff --git a/regression/no_intervening_calls/ground-truth.csv b/regression/no_intervening_calls/ground-truth.csv
new file mode 100644
index 00000000..57cce307
--- /dev/null
+++ b/regression/no_intervening_calls/ground-truth.csv
@@ -0,0 +1,3 @@
+property,version,truth,footnote-md
+no-explicit-g-call,v1,1
+explicit-g-call,v1,0
\ No newline at end of file
diff --git a/regression/no_intervening_calls/hardhat/Makefile b/regression/no_intervening_calls/hardhat/Makefile
new file mode 100644
index 00000000..c49b2687
--- /dev/null
+++ b/regression/no_intervening_calls/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/no_intervening_calls/hardhat/contracts/NoInterveningCalls_v1.sol b/regression/no_intervening_calls/hardhat/contracts/NoInterveningCalls_v1.sol
new file mode 100644
index 00000000..c892b180
--- /dev/null
+++ b/regression/no_intervening_calls/hardhat/contracts/NoInterveningCalls_v1.sol
@@ -0,0 +1,14 @@
+pragma solidity ^0.8.25;
+
+contract NoInterveningCalls {
+	bool b = true;
+
+    function f() public{}
+    function g() public {
+        b = false;
+    }
+
+    function getB() public view returns (bool) {
+        return b;
+    }
+}
\ No newline at end of file
diff --git a/regression/no_intervening_calls/hardhat/test/test.js b/regression/no_intervening_calls/hardhat/test/test.js
new file mode 100644
index 00000000..24562684
--- /dev/null
+++ b/regression/no_intervening_calls/hardhat/test/test.js
@@ -0,0 +1,22 @@
+const {
+    loadFixture
+} = require("@nomicfoundation/hardhat-toolbox/network-helpers");
+const { expect } = require("chai");
+
+describe("NoInterveningCalls", function () {
+    async function deployContract() {
+
+        const NoInterveningCalls = await(ethers.deployContract("NoInterveningCalls"));
+
+        return { NoInterveningCalls };
+    }
+
+    it("`g()` is called in between the two calls to `f()`, which results in the value of `b` changing", async function () {
+        const { NoInterveningCalls } = await loadFixture(deployContract);
+
+        await NoInterveningCalls.f();
+        await NoInterveningCalls.g();
+        await NoInterveningCalls.f();
+        expect(await NoInterveningCalls.getB()).to.equal(false);
+    })
+});
\ No newline at end of file
diff --git a/regression/no_intervening_calls/skeleton.json b/regression/no_intervening_calls/skeleton.json
new file mode 100644
index 00000000..48eb0642
--- /dev/null
+++ b/regression/no_intervening_calls/skeleton.json
@@ -0,0 +1,8 @@
+{
+    "name": "No Intervening Calls",
+    "specification": "file:specs.md",
+    "properties": {
+        "no-explicit-g-call": "`b` is `true` after two consecutive calls to `f()`, without any intervening calls to `g()`.",
+        "explicit-g-call": "`b` is `true` after `g()` is explicitly called between the two `f()` calls"
+    }
+}
diff --git a/regression/no_intervening_calls/solcmc/NoInterveningCalls_explicit-g-call_v1.sol b/regression/no_intervening_calls/solcmc/NoInterveningCalls_explicit-g-call_v1.sol
new file mode 100644
index 00000000..2e42deb4
--- /dev/null
+++ b/regression/no_intervening_calls/solcmc/NoInterveningCalls_explicit-g-call_v1.sol
@@ -0,0 +1,22 @@
+pragma solidity ^0.8.25;
+
+contract NoInterveningCalls {
+    bool b = true;
+
+    function f() public{}
+    function g() public {
+        b = false;
+    }
+
+    function getB() public view returns (bool) {
+        return b;
+    }
+
+    function h() public {
+        require(b);
+        f();
+        g();
+        f();
+        assert(b);
+    }
+}
\ No newline at end of file
diff --git a/regression/no_intervening_calls/solcmc/NoInterveningCalls_no-explicit-g-call_v1.sol b/regression/no_intervening_calls/solcmc/NoInterveningCalls_no-explicit-g-call_v1.sol
new file mode 100644
index 00000000..0230c17d
--- /dev/null
+++ b/regression/no_intervening_calls/solcmc/NoInterveningCalls_no-explicit-g-call_v1.sol
@@ -0,0 +1,21 @@
+pragma solidity ^0.8.25;
+
+contract NoInterveningCalls {
+    bool b = true;
+
+    function f() public{}
+    function g() public {
+        b = false;
+    }
+
+    function getB() public view returns (bool) {
+        return b;
+    }
+
+    function h() public {
+        require(b);
+        f();
+        f();
+        assert(b);
+    }
+}
\ No newline at end of file
diff --git a/regression/no_intervening_calls/specs.md b/regression/no_intervening_calls/specs.md
new file mode 100644
index 00000000..09bb8906
--- /dev/null
+++ b/regression/no_intervening_calls/specs.md
@@ -0,0 +1,6 @@
+The `NoInterveningCalls` contract manages a boolean state variable `b` with two functions:
+
+- `f()`: A no-op function that performs no state changes.
+- `g()`: A function that modifies the state by setting `b` to `false`.
+
+When `f()` is called two times in a row and `g()` is not called, the value of `b` should not change.
\ No newline at end of file