From 37215ffcfdb0889bffd1cde4b2bbb472394484d8 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Wed, 6 Oct 2021 11:51:55 +0200
Subject: [PATCH] Add SMTCheckerTest isoltest option to ignore invariants

---
 libsolidity/formal/ModelCheckerSettings.h |  1 +
 test/libsolidity/SMTCheckerTest.cpp       | 10 ++++++++++
 test/libsolidity/SMTCheckerTest.h         |  2 ++
 3 files changed, 13 insertions(+)

diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h
index 3d137044a..e3e93fcf4 100644
--- a/libsolidity/formal/ModelCheckerSettings.h
+++ b/libsolidity/formal/ModelCheckerSettings.h
@@ -95,6 +95,7 @@ struct ModelCheckerInvariants
 	static ModelCheckerInvariants Default() { return *fromString("default"); }
 	/// Adds all targets, including underflow and overflow.
 	static ModelCheckerInvariants All() { return *fromString("all"); }
+	static ModelCheckerInvariants None() { return {{}}; }
 
 	static std::optional<ModelCheckerInvariants> fromString(std::string const& _invs);
 
diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp
index 5606b0bfe..3b6b8e1b8 100644
--- a/test/libsolidity/SMTCheckerTest.cpp
+++ b/test/libsolidity/SMTCheckerTest.cpp
@@ -19,6 +19,8 @@
 #include <test/libsolidity/SMTCheckerTest.h>
 #include <test/Common.h>
 
+#include <range/v3/action/remove_if.hpp>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::langutil;
@@ -67,6 +69,14 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
 	else
 		BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT counterexample choice."));
 
+	auto const& ignoreInv = m_reader.stringSetting("SMTIgnoreInv", "no");
+	if (ignoreInv == "no")
+		m_modelCheckerSettings.invariants = ModelCheckerInvariants::All();
+	else if (ignoreInv == "yes")
+		m_modelCheckerSettings.invariants = ModelCheckerInvariants::None();
+	else
+		BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT invariant choice."));
+
 	auto const& ignoreOSSetting = m_reader.stringSetting("SMTIgnoreOS", "none");
 	for (string const& os: ignoreOSSetting | ranges::views::split(',') | ranges::to<vector<string>>())
 	{
diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h
index 9cc4e5751..54d23c74f 100644
--- a/test/libsolidity/SMTCheckerTest.h
+++ b/test/libsolidity/SMTCheckerTest.h
@@ -49,6 +49,8 @@ protected:
 		Set in m_modelCheckerSettings.
 	SMTIgnoreCex: `yes`, `no`, where the default is `no`.
 		Set in m_ignoreCex.
+	SMTIgnoreInv: `yes`, `no`, where the default is `no`.
+		Set in m_modelCheckerSettings.
 	SMTShowUnproved: `yes`, `no`, where the default is `yes`.
 		Set in m_modelCheckerSettings.
 	SMTSolvers: `all`, `cvc4`, `z3`, `none`, where the default is `all`.