From 3599c8c6b92cac837b7fa3f0c0c196a12e749151 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@gmail.com>
Date: Fri, 30 Jun 2023 15:02:06 +0200
Subject: [PATCH] SMTChecker: Fix generation of smtlib scripts

When both CHC and BMC engines are used, the type of state variable
changes when trusted mode for external calls is used. This is because in
CHC engine, trusted mode means we pack more information into the
symbolic state. In BMC this type is always simple.

However, if BMC is run after CHC, in the current code state variables
are reset (and their declaration dumped into SMT-LIB script) before BMC
resets the type of the state variable.

The proposed solution is to simply reset the variable type before the
first variable of this type is created.
---
 libsolidity/formal/BMC.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index d38f27b6a..cead3a528 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -81,13 +81,13 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 
 	SMTEncoder::resetSourceAnalysis();
 
+	state().prepareForSourceUnit(_source, false);
 	m_solvedTargets = std::move(_solvedTargets);
 	m_context.setSolver(m_interface.get());
 	m_context.reset();
 	m_context.setAssertionAccumulation(true);
 	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 	createFreeConstants(sourceDependencies(_source));
-	state().prepareForSourceUnit(_source, false);
 	m_unprovedAmt = 0;
 
 	_source.accept(*this);