diff --git a/test/cmdlineTests/model_checker_invariants_contract_eld/args b/test/cmdlineTests/model_checker_invariants_contract_eld/args
new file mode 100644
index 000000000000..7f2a13bfd8c1
--- /dev/null
+++ b/test/cmdlineTests/model_checker_invariants_contract_eld/args
@@ -0,0 +1 @@
+--model-checker-engine chc --model-checker-invariants contract --model-checker-solvers eld
diff --git a/test/cmdlineTests/model_checker_invariants_contract_eld/err b/test/cmdlineTests/model_checker_invariants_contract_eld/err
new file mode 100644
index 000000000000..29c5a5bc8eae
--- /dev/null
+++ b/test/cmdlineTests/model_checker_invariants_contract_eld/err
@@ -0,0 +1,4 @@
+Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+
+Info: Contract invariant(s) for model_checker_invariants_contract_eld/input.sol:test:
+(x = 0)
diff --git a/test/cmdlineTests/model_checker_invariants_contract_eld/input.sol b/test/cmdlineTests/model_checker_invariants_contract_eld/input.sol
new file mode 100644
index 000000000000..4bee228bd65f
--- /dev/null
+++ b/test/cmdlineTests/model_checker_invariants_contract_eld/input.sol
@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract test {
+	uint x;
+	function f() public view {
+		assert(x < 10);
+	}
+}