Fix ICE in constants

libsolidity/formal/BMC.cpp

@@ -80,7 +80,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 	{
 		m_solvedTargets = move(_solvedTargets);
 		m_context.setSolver(m_interface.get());
-		m_context.clear();
+		m_context.reset();
 		m_context.setAssertionAccumulation(true);
 		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 		createFreeConstants(sourceDependencies(_source));

libsolidity/formal/CHC.cpp

@@ -967,7 +967,7 @@ void CHC::resetSourceAnalysis()
 		m_context.setSolver(smtlib2Interface->smtlib2Interface());
 	}
 
-	m_context.clear();
+	m_context.reset();
 	m_context.resetUniqueId();
 	m_context.setAssertionAccumulation(false);
 }

libsolidity/formal/EncodingContext.cpp

@@ -49,12 +49,6 @@ unsigned EncodingContext::newUniqueId()
 	return m_nextUniqueId++;
 }
 
-void EncodingContext::clear()
-{
-	m_variables.clear();
-	reset();
-}
-
 /// Variables.
 
 shared_ptr<SymbolicVariable> EncodingContext::variable(frontend::VariableDeclaration const& _varDecl)

libsolidity/formal/SMTEncoder.cpp

@@ -3034,6 +3034,15 @@ void SMTEncoder::createFreeConstants(set<SourceUnit const*, ASTNode::CompareByID
 		for (auto node: source->nodes())
 			if (auto var = dynamic_cast<VariableDeclaration const*>(node.get()))
 				createVariable(*var);
+			else if (
+				auto contract = dynamic_cast<ContractDefinition const*>(node.get());
+				contract && contract->isLibrary()
+			)
+				for (auto var: contract->stateVariables())
+				{
+					solAssert(var->isConstant(), "");
+					createVariable(*var);
+				}
 }
 
 smt::SymbolicState& SMTEncoder::state()