review

Author: Leo Alt

libsmtutil/CHCSmtLib2Interface.cpp

@@ -23,6 +23,8 @@
 #include <boost/algorithm/string/join.hpp>
 #include <boost/algorithm/string/predicate.hpp>
 
+#include <range/v3/view.hpp>
+
 #include <array>
 #include <fstream>
 #include <iostream>
@@ -91,7 +93,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expre
 	swap(m_accumulatedOutput, accumulated);
 	solAssert(m_smtlib2, "");
 	writeHeader();
-	for (auto const& [type, decl]: m_smtlib2->userSorts())
+	for (auto const& decl: m_smtlib2->userSorts() | ranges::views::values)
 		write(decl);
 	m_accumulatedOutput += accumulated;
 

libsmtutil/SMTLib2Interface.h

@@ -66,7 +66,7 @@ class SMTLib2Interface: public SolverInterface
 
 	std::map<std::string, SortPointer> variables() { return m_variables; }
 
-	std::vector<std::pair<std::string, std::string>>const& userSorts() const { return m_userSorts; }
+	std::vector<std::pair<std::string, std::string>> const& userSorts() const { return m_userSorts; }
 
 private:
 	void declareFunction(std::string const& _name, SortPointer const& _sort);

libsmtutil/SolverInterface.h

@@ -64,8 +64,8 @@ class Expression
 		name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
 	Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {}
 	Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
-	Expression(s256 const& _number): Expression(_number.sign() >= 0 ? _number.str() : "-", _number.sign() >= 0 ? std::vector<Expression>{} : std::vector<Expression>{Expression(size_t(0)), u256(-_number)}, SortProvider::sintSort) {}
-	Expression(bigint const& _number): Expression(_number.sign() >= 0 ? _number.str() : "-", _number.sign() >= 0 ? std::vector<Expression>{} : std::vector<Expression>{Expression(size_t(0)), u256(-_number)}, SortProvider::sintSort) {}
+	Expression(s256 const& _number): Expression(_number >= 0 ? _number.str() : "-", _number >= 0 ? std::vector<Expression>{} : std::vector<Expression>{Expression(size_t(0)), bigint(-_number)}, SortProvider::sintSort) {}
+	Expression(bigint const& _number): Expression(_number >= 0 ? _number.str() : "-", _number >= 0 ? std::vector<Expression>{} : std::vector<Expression>{Expression(size_t(0)), bigint(-_number)}, SortProvider::sintSort) {}
 
 	Expression(Expression const&) = default;
 	Expression(Expression&&) = default;

libsolidity/formal/CHC.cpp

@@ -947,6 +947,7 @@ void CHC::resetSourceAnalysis()
 	{
 		auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
 		solAssert(smtlib2Interface, "");
+		smtlib2Interface->reset();
 		m_context.setSolver(smtlib2Interface->smtlib2Interface());
 	}