mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #11289 from ethereum/smt_fix_chcsmtlib2interface
[SMTChecker] Fix CHCSmtLib2Interface
This commit is contained in:
Leonardo
GitHub
commit
a87998494a
@ -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>
|
||||
@ -53,8 +55,7 @@ void CHCSmtLib2Interface::reset()
|
||||
m_accumulatedOutput.clear();
|
||||
m_variables.clear();
|
||||
m_unhandledQueries.clear();
|
||||
if (m_queryTimeout)
|
||||
write("(set-option :timeout " + to_string(*m_queryTimeout) + ")");
|
||||
m_sortNames.clear();
|
||||
}
|
||||
|
||||
void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
|
||||
@ -64,27 +65,25 @@ void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
|
||||
if (!m_variables.count(_expr.name))
|
||||
{
|
||||
auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);
|
||||
string domain = m_smtlib2->toSmtLibSort(fSort->domain);
|
||||
string domain = toSmtLibSort(fSort->domain);
|
||||
// Relations are predicates which have implicit codomain Bool.
|
||||
m_variables.insert(_expr.name);
|
||||
write(
|
||||
"(declare-rel |" +
|
||||
"(declare-fun |" +
|
||||
_expr.name +
|
||||
"| " +
|
||||
domain +
|
||||
")"
|
||||
" Bool)"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& _name)
|
||||
void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*_name*/)
|
||||
{
|
||||
write(
|
||||
"(rule (! " +
|
||||
"(assert\n(forall " + forall() + "\n" +
|
||||
m_smtlib2->toSExpr(_expr) +
|
||||
" :named " +
|
||||
_name +
|
||||
"))"
|
||||
"))\n\n"
|
||||
);
|
||||
}
|
||||
|
||||
@ -92,22 +91,29 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expre
|
||||
{
|
||||
string accumulated{};
|
||||
swap(m_accumulatedOutput, accumulated);
|
||||
for (auto const& var: m_smtlib2->variables())
|
||||
declareVariable(var.first, var.second);
|
||||
solAssert(m_smtlib2, "");
|
||||
writeHeader();
|
||||
for (auto const& decl: m_smtlib2->userSorts() | ranges::views::values)
|
||||
write(decl);
|
||||
m_accumulatedOutput += accumulated;
|
||||
|
||||
string queryRule = "(assert\n(forall " + forall() + "\n" +
|
||||
"(=> " + _block.name + " false)"
|
||||
"))";
|
||||
string response = querySolver(
|
||||
m_accumulatedOutput +
|
||||
"\n(query " + _block.name + " :print-certificate true)"
|
||||
queryRule +
|
||||
"\n(check-sat)"
|
||||
);
|
||||
swap(m_accumulatedOutput, accumulated);
|
||||
|
||||
CheckResult result;
|
||||
// TODO proper parsing
|
||||
if (boost::starts_with(response, "sat\n"))
|
||||
result = CheckResult::SATISFIABLE;
|
||||
else if (boost::starts_with(response, "unsat\n"))
|
||||
if (boost::starts_with(response, "sat"))
|
||||
result = CheckResult::UNSATISFIABLE;
|
||||
else if (boost::starts_with(response, "unknown\n"))
|
||||
else if (boost::starts_with(response, "unsat"))
|
||||
result = CheckResult::SATISFIABLE;
|
||||
else if (boost::starts_with(response, "unknown"))
|
||||
result = CheckResult::UNKNOWN;
|
||||
else
|
||||
result = CheckResult::ERROR;
|
||||
@ -124,10 +130,46 @@ void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const
|
||||
else if (!m_variables.count(_name))
|
||||
{
|
||||
m_variables.insert(_name);
|
||||
write("(declare-var |" + _name + "| " + m_smtlib2->toSmtLibSort(*_sort) + ')');
|
||||
write("(declare-var |" + _name + "| " + toSmtLibSort(*_sort) + ')');
|
||||
}
|
||||
}
|
||||
|
||||
string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort)
|
||||
{
|
||||
if (!m_sortNames.count(&_sort))
|
||||
m_sortNames[&_sort] = m_smtlib2->toSmtLibSort(_sort);
|
||||
return m_sortNames.at(&_sort);
|
||||
}
|
||||
|
||||
string CHCSmtLib2Interface::toSmtLibSort(vector<SortPointer> const& _sorts)
|
||||
{
|
||||
string ssort("(");
|
||||
for (auto const& sort: _sorts)
|
||||
ssort += toSmtLibSort(*sort) + " ";
|
||||
ssort += ")";
|
||||
return ssort;
|
||||
}
|
||||
|
||||
void CHCSmtLib2Interface::writeHeader()
|
||||
{
|
||||
if (m_queryTimeout)
|
||||
write("(set-option :timeout " + to_string(*m_queryTimeout) + ")");
|
||||
write("(set-logic HORN)\n");
|
||||
}
|
||||
|
||||
string CHCSmtLib2Interface::forall()
|
||||
{
|
||||
string vars("(");
|
||||
for (auto const& [name, sort]: m_smtlib2->variables())
|
||||
{
|
||||
solAssert(sort, "");
|
||||
if (sort->kind != Kind::Function)
|
||||
vars += " (" + name + " " + toSmtLibSort(*sort) + ")";
|
||||
}
|
||||
vars += ")";
|
||||
return vars;
|
||||
}
|
||||
|
||||
void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
|
||||
{
|
||||
smtAssert(_sort, "");
|
||||
@ -137,8 +179,8 @@ void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const
|
||||
{
|
||||
auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);
|
||||
smtAssert(fSort->codomain, "");
|
||||
string domain = m_smtlib2->toSmtLibSort(fSort->domain);
|
||||
string codomain = m_smtlib2->toSmtLibSort(*fSort->codomain);
|
||||
string domain = toSmtLibSort(fSort->domain);
|
||||
string codomain = toSmtLibSort(*fSort->codomain);
|
||||
m_variables.insert(_name);
|
||||
write(
|
||||
"(declare-fun |" +
|
||||
|
||||
@ -53,6 +53,12 @@ public:
|
||||
SMTLib2Interface* smtlib2Interface() const { return m_smtlib2.get(); }
|
||||
|
||||
private:
|
||||
std::string toSmtLibSort(Sort const& _sort);
|
||||
std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
|
||||
|
||||
void writeHeader();
|
||||
std::string forall();
|
||||
|
||||
void declareFunction(std::string const& _name, SortPointer const& _sort);
|
||||
|
||||
void write(std::string _data);
|
||||
@ -70,6 +76,8 @@ private:
|
||||
std::vector<std::string> m_unhandledQueries;
|
||||
|
||||
frontend::ReadCallback::Callback m_smtCallback;
|
||||
|
||||
std::map<Sort const*, std::string> m_sortNames;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
@ -170,7 +170,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
|
||||
return arguments[0].andExpr(arguments[1]);
|
||||
else if (n == "or")
|
||||
return arguments[0].orExpr(arguments[1]);
|
||||
else if (n == "implies")
|
||||
else if (n == "=>")
|
||||
return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]);
|
||||
else if (n == "=")
|
||||
return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]);
|
||||
@ -188,7 +188,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
|
||||
return m_context.mkExpr(CVC4::kind::MINUS, arguments[0], arguments[1]);
|
||||
else if (n == "*")
|
||||
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
|
||||
else if (n == "/")
|
||||
else if (n == "div")
|
||||
return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
|
||||
else if (n == "mod")
|
||||
return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]);
|
||||
|
||||
@ -23,6 +23,8 @@
|
||||
#include <boost/algorithm/string/join.hpp>
|
||||
#include <boost/algorithm/string/predicate.hpp>
|
||||
|
||||
#include <range/v3/algorithm/find_if.hpp>
|
||||
|
||||
#include <array>
|
||||
#include <fstream>
|
||||
#include <iostream>
|
||||
@ -173,7 +175,7 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
|
||||
sexpr += string("ite ") +
|
||||
"(= ((_ extract " + pos + " " + pos + ")" + arg + ") #b0) " +
|
||||
nat + " " +
|
||||
"(- (bvneg " + arg + "))";
|
||||
"(- (bv2nat (bvneg " + arg + ")))";
|
||||
}
|
||||
else if (_expr.name == "const_array")
|
||||
{
|
||||
@ -231,14 +233,15 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
|
||||
{
|
||||
auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
|
||||
string tupleName = "|" + tupleSort.name + "|";
|
||||
if (!m_userSorts.count(tupleName))
|
||||
auto isName = [&](auto entry) { return entry.first == tupleName; };
|
||||
if (ranges::find_if(m_userSorts, isName) == m_userSorts.end())
|
||||
{
|
||||
m_userSorts.insert(tupleName);
|
||||
string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName);
|
||||
smtAssert(tupleSort.members.size() == tupleSort.components.size(), "");
|
||||
for (unsigned i = 0; i < tupleSort.members.size(); ++i)
|
||||
decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")";
|
||||
decl += "))))";
|
||||
m_userSorts.emplace_back(tupleName, decl);
|
||||
write(decl);
|
||||
}
|
||||
|
||||
|
||||
@ -66,6 +66,8 @@ public:
|
||||
|
||||
std::map<std::string, SortPointer> variables() { return m_variables; }
|
||||
|
||||
std::vector<std::pair<std::string, std::string>> const& userSorts() const { return m_userSorts; }
|
||||
|
||||
private:
|
||||
void declareFunction(std::string const& _name, SortPointer const& _sort);
|
||||
|
||||
@ -79,7 +81,12 @@ private:
|
||||
|
||||
std::vector<std::string> m_accumulatedOutput;
|
||||
std::map<std::string, SortPointer> m_variables;
|
||||
std::set<std::string> m_userSorts;
|
||||
|
||||
/// Each pair in this vector represents an SMTChecker created
|
||||
/// sort (a user sort), and the smtlib2 declaration of that sort.
|
||||
/// It needs to be a vector so that the declaration order is kept,
|
||||
/// otherwise solvers cannot parse the queries.
|
||||
std::vector<std::pair<std::string, std::string>> m_userSorts;
|
||||
|
||||
std::map<util::h256, std::string> m_queryResponses;
|
||||
std::vector<std::string> m_unhandledQueries;
|
||||
|
||||
@ -64,8 +64,20 @@ public:
|
||||
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.str(), {}, SortProvider::sintSort) {}
|
||||
Expression(bigint const& _number): Expression(_number.str(), {}, 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;
|
||||
@ -86,7 +98,7 @@ public:
|
||||
{"not", 1},
|
||||
{"and", 2},
|
||||
{"or", 2},
|
||||
{"implies", 2},
|
||||
{"=>", 2},
|
||||
{"=", 2},
|
||||
{"<", 2},
|
||||
{"<=", 2},
|
||||
@ -95,7 +107,7 @@ public:
|
||||
{"+", 2},
|
||||
{"-", 2},
|
||||
{"*", 2},
|
||||
{"/", 2},
|
||||
{"div", 2},
|
||||
{"mod", 2},
|
||||
{"bvnot", 1},
|
||||
{"bvand", 2},
|
||||
@ -126,7 +138,7 @@ public:
|
||||
static Expression implies(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression(
|
||||
"implies",
|
||||
"=>",
|
||||
std::move(_a),
|
||||
std::move(_b),
|
||||
Kind::Bool
|
||||
@ -300,7 +312,7 @@ public:
|
||||
friend Expression operator/(Expression _a, Expression _b)
|
||||
{
|
||||
auto intSort = _a.sort;
|
||||
return Expression("/", {std::move(_a), std::move(_b)}, intSort);
|
||||
return Expression("div", {std::move(_a), std::move(_b)}, intSort);
|
||||
}
|
||||
friend Expression operator%(Expression _a, Expression _b)
|
||||
{
|
||||
|
||||
@ -189,7 +189,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
|
||||
return arguments[0] && arguments[1];
|
||||
else if (n == "or")
|
||||
return arguments[0] || arguments[1];
|
||||
else if (n == "implies")
|
||||
else if (n == "=>")
|
||||
return z3::implies(arguments[0], arguments[1]);
|
||||
else if (n == "=")
|
||||
return arguments[0] == arguments[1];
|
||||
@ -207,7 +207,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
|
||||
return arguments[0] - arguments[1];
|
||||
else if (n == "*")
|
||||
return arguments[0] * arguments[1];
|
||||
else if (n == "/")
|
||||
else if (n == "div")
|
||||
return arguments[0] / arguments[1];
|
||||
else if (n == "mod")
|
||||
return z3::mod(arguments[0], arguments[1]);
|
||||
|
||||
@ -946,8 +946,8 @@ void CHC::resetSourceAnalysis()
|
||||
if (!usesZ3)
|
||||
{
|
||||
auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
|
||||
smtlib2Interface->reset();
|
||||
solAssert(smtlib2Interface, "");
|
||||
smtlib2Interface->reset();
|
||||
m_context.setSolver(smtlib2Interface->smtlib2Interface());
|
||||
}
|
||||
|
||||
|
||||
@ -797,7 +797,7 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
|
||||
|
||||
void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
|
||||
{
|
||||
string gasLeft = "gasleft()";
|
||||
string gasLeft = "gasleft";
|
||||
// We increase the variable index since gasleft changes
|
||||
// inside a tx.
|
||||
defineGlobalVariable(gasLeft, _funCall, true);
|
||||
|
||||
@ -118,7 +118,7 @@ SortPointer smtSort(frontend::Type const& _type)
|
||||
else
|
||||
tupleName = arrayType->baseType()->toString(true);
|
||||
|
||||
tupleName += "[]";
|
||||
tupleName += "_array";
|
||||
}
|
||||
else
|
||||
tupleName = _type.toString(true);
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x944140895bd672003614580050e8349baeea7cced0d8b9447aefb6c4833b02a8":"(set-option :produce-models true)
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x4ee925df3426fec84707cea517cc52ed216229bfde71458a69e7edeece2c071e":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -17,7 +17,7 @@
|
||||
(declare-fun |expr_8_0| () Int)
|
||||
(declare-fun |expr_9_1| () Bool)
|
||||
|
||||
(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (implies (and true true) true) (and (= expr_8_0 0) (and (implies (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
|
||||
(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| x_3_0))
|
||||
(check-sat)
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x9190f95880d71b6c4636672b262f07430b161f369cc56816ad265e4fa1ee1f3a":"(set-option :produce-models true)
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x8a1785699211e91e2593e2568d4240af6ec3b4ba113087fcb6f42bc764040d83":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -12,18 +12,18 @@
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
|
||||
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
|
||||
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
|
||||
(check-sat)
|
||||
","0xd32caa9b049de053b56e6d79b6b17e718634bff64ba913b2f28e5369947d4e3b":"(set-option :produce-models true)
|
||||
","0xd5b9836c53d2b59d5215cfe646b8a2d6702aed014aae55a9512896c876117d01":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -37,11 +37,36 @@
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
|
||||
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
|
||||
(check-sat)
|
||||
","0xf74fc530d5dd4498f4ad9eeb32a713af6cc6966efcd3e58083b97f864fdc7cbb":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
|
||||
(declare-fun |state_0| () |state_type|)
|
||||
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
|
||||
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
|
||||
(declare-fun |tx_0| () |tx_type|)
|
||||
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
|
||||
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
@ -64,45 +89,20 @@
|
||||
(declare-fun |expr_39_0| () Int)
|
||||
(declare-fun |expr_40_0| () Int)
|
||||
(declare-fun |expr_41_1| () Bool)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_50_0| () Int)
|
||||
(declare-fun |expr_51_1| () Int)
|
||||
|
||||
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (implies (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (implies (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_14_0)) (and (and (<= 0 r_div_mod_14_0) (or (= expr_29_0 0) (< r_div_mod_14_0 expr_29_0))) (and (= (+ (* d_div_mod_14_0 expr_29_0) r_div_mod_14_0) expr_28_0) (and (implies (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (implies (and true true) true) (and (= expr_28_0 2) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
|
||||
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (=> (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (=> (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_14_0)) (and (and (<= 0 r_div_mod_14_0) (or (= expr_29_0 0) (< r_div_mod_14_0 expr_29_0))) (and (= (+ (* d_div_mod_14_0 expr_29_0) r_div_mod_14_0) expr_28_0) (and (=> (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (=> (and true true) true) (and (= expr_28_0 2) (and (=> (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| a_6_0))
|
||||
(declare-const |EVALEXPR_1| Int)
|
||||
(assert (= |EVALEXPR_1| x_8_1))
|
||||
(check-sat)
|
||||
(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
|
||||
","0xdb117433a9ec32d2f491750fb369a0d49c0afb6cad5f9ea3e1739ef8b87cdf4f":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
|
||||
(declare-fun |state_0| () |state_type|)
|
||||
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
|
||||
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
|
||||
(declare-fun |tx_0| () |tx_type|)
|
||||
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
|
||||
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
|
||||
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
|
||||
(check-sat)
|
||||
"}},"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here.
|
||||
Counterexample:
|
||||
arr = []
|
||||
|
||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
@ -1,4 +1,4 @@
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x3b3d90fa6754444a847a9b6f723e98fc3c8b428cb56d50a010bc2c435aa1bc10":"(set-option :produce-models true)
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x5862836cd5cba5060769154afd0642e5da1a79918f7272f38a25e27138aa8060":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -12,11 +12,11 @@
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
@ -39,14 +39,14 @@
|
||||
(declare-fun |expr_39_0| () Int)
|
||||
(declare-fun |expr_40_0| () Int)
|
||||
(declare-fun |expr_41_1| () Bool)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_50_0| () Int)
|
||||
(declare-fun |expr_51_1| () Int)
|
||||
|
||||
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (implies (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (implies (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_29_0 0) (< r_div_mod_0_0 expr_29_0))) (and (= (+ (* d_div_mod_0_0 expr_29_0) r_div_mod_0_0) expr_28_0) (and (implies (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (implies (and true true) true) (and (= expr_28_0 2) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
|
||||
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (=> (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (=> (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_29_0 0) (< r_div_mod_0_0 expr_29_0))) (and (= (+ (* d_div_mod_0_0 expr_29_0) r_div_mod_0_0) expr_28_0) (and (=> (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (=> (and true true) true) (and (= expr_28_0 2) (and (=> (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| a_6_0))
|
||||
(declare-const |EVALEXPR_1| Int)
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x9190f95880d71b6c4636672b262f07430b161f369cc56816ad265e4fa1ee1f3a":"(set-option :produce-models true)
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x8a1785699211e91e2593e2568d4240af6ec3b4ba113087fcb6f42bc764040d83":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -12,18 +12,18 @@
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
|
||||
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
|
||||
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
|
||||
(check-sat)
|
||||
","0xdb117433a9ec32d2f491750fb369a0d49c0afb6cad5f9ea3e1739ef8b87cdf4f":"(set-option :produce-models true)
|
||||
","0xd5b9836c53d2b59d5215cfe646b8a2d6702aed014aae55a9512896c876117d01":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -37,16 +37,16 @@
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
|
||||
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
|
||||
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
|
||||
(check-sat)
|
||||
"}},"errors":[{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
|
||||
--> A:7:15:
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x3d72a9e21e83263eacaad9b3eaa387b10f1219c1727796d9e946ddce1e99f5a3":"(set-option :produce-models true)
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x8287518649c1faba68e8ce20d7a8d43f63e983df65020101186d67acbfc4db9a":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -12,11 +12,11 @@
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
@ -39,14 +39,14 @@
|
||||
(declare-fun |expr_39_0| () Int)
|
||||
(declare-fun |expr_40_0| () Int)
|
||||
(declare-fun |expr_41_1| () Bool)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_50_0| () Int)
|
||||
(declare-fun |expr_51_1| () Int)
|
||||
|
||||
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (implies (and true true) true) (and (= expr_28_0 2) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))) (= expr_29_0 0)))
|
||||
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (=> (and true true) true) (and (= expr_28_0 2) (and (=> (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))) (= expr_29_0 0)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| a_6_0))
|
||||
(declare-const |EVALEXPR_1| Int)
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x7b2c4d6761f5d49a4a2e0ba56b832d235e93abf16fe2a1383a526aa4fb4fe028":"(set-option :produce-models true)
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0xc4955111313d5bc83a8e7aece746156804afbd102ec8a78c06b2a284470deebc":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -12,11 +12,11 @@
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
@ -39,14 +39,14 @@
|
||||
(declare-fun |expr_39_0| () Int)
|
||||
(declare-fun |expr_40_0| () Int)
|
||||
(declare-fun |expr_41_1| () Bool)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_50_0| () Int)
|
||||
(declare-fun |expr_51_1| () Int)
|
||||
|
||||
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_20_0 expr_25_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
|
||||
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_20_0 expr_25_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| a_6_0))
|
||||
(declare-const |EVALEXPR_1| Int)
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x0bf4bf54fa2ecac3482de1b433e5216d0b2f9c2347e556e43c252499885165e5":"(set-option :produce-models true)
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0xf8a9e6ce3d09ef3b2a597297e00abd8e9cdfee9d2491deb6cb8349f0ee53fc61":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -12,11 +12,11 @@
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
@ -39,14 +39,14 @@
|
||||
(declare-fun |expr_39_0| () Int)
|
||||
(declare-fun |expr_40_0| () Int)
|
||||
(declare-fun |expr_41_1| () Bool)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_50_0| () Int)
|
||||
(declare-fun |expr_51_1| () Int)
|
||||
|
||||
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))))) (< (- expr_17_0 1) 0)))
|
||||
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))))) (< (- expr_17_0 1) 0)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| a_6_0))
|
||||
(declare-const |EVALEXPR_1| Int)
|
||||
|
||||
File diff suppressed because one or more lines are too long
@ -1,4 +1,4 @@
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0x0bf4bf54fa2ecac3482de1b433e5216d0b2f9c2347e556e43c252499885165e5":"(set-option :produce-models true)
|
||||
{"auxiliaryInputRequested":{"smtlib2queries":{"0xc4955111313d5bc83a8e7aece746156804afbd102ec8a78c06b2a284470deebc":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
@ -12,11 +12,11 @@
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
@ -39,71 +39,14 @@
|
||||
(declare-fun |expr_39_0| () Int)
|
||||
(declare-fun |expr_40_0| () Int)
|
||||
(declare-fun |expr_41_1| () Bool)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_50_0| () Int)
|
||||
(declare-fun |expr_51_1| () Int)
|
||||
|
||||
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))))) (< (- expr_17_0 1) 0)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| a_6_0))
|
||||
(declare-const |EVALEXPR_1| Int)
|
||||
(assert (= |EVALEXPR_1| x_8_0))
|
||||
(declare-const |EVALEXPR_2| Int)
|
||||
(assert (= |EVALEXPR_2| (- expr_17_0 1)))
|
||||
(check-sat)
|
||||
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
|
||||
","0x7b2c4d6761f5d49a4a2e0ba56b832d235e93abf16fe2a1383a526aa4fb4fe028":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
|
||||
(declare-fun |state_0| () |state_type|)
|
||||
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
|
||||
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
|
||||
(declare-fun |tx_0| () |tx_type|)
|
||||
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
|
||||
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
(declare-fun |expr_17_0| () Int)
|
||||
(declare-fun |expr_18_1| () Int)
|
||||
(declare-fun |x_8_1| () Int)
|
||||
(declare-fun |expr_20_0| () Int)
|
||||
(declare-fun |expr_25_1| () Int)
|
||||
(declare-fun |expr_26_1| () Int)
|
||||
(declare-fun |expr_28_0| () Int)
|
||||
(declare-fun |expr_29_0| () Int)
|
||||
(declare-fun |d_div_mod_0_0| () Int)
|
||||
(declare-fun |r_div_mod_0_0| () Int)
|
||||
(declare-fun |expr_30_1| () Int)
|
||||
(declare-fun |expr_32_0| () Int)
|
||||
(declare-fun |expr_35_0| () Int)
|
||||
(declare-fun |state_1| () |state_type|)
|
||||
(declare-fun |state_2| () |state_type|)
|
||||
(declare-fun |state_3| () |state_type|)
|
||||
(declare-fun |expr_39_0| () Int)
|
||||
(declare-fun |expr_40_0| () Int)
|
||||
(declare-fun |expr_41_1| () Bool)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
|
||||
(declare-fun |expr_50_0| () Int)
|
||||
(declare-fun |expr_51_1| () Int)
|
||||
|
||||
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_20_0 expr_25_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
|
||||
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (=> (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (=> (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_20_0 expr_25_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| a_6_0))
|
||||
(declare-const |EVALEXPR_1| Int)
|
||||
@ -112,6 +55,63 @@
|
||||
(assert (= |EVALEXPR_2| (+ expr_20_0 expr_25_1)))
|
||||
(check-sat)
|
||||
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
|
||||
","0xf8a9e6ce3d09ef3b2a597297e00abd8e9cdfee9d2491deb6cb8349f0ee53fc61":"(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
|
||||
(declare-fun |state_0| () |state_type|)
|
||||
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
|
||||
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
|
||||
(declare-fun |tx_0| () |tx_type|)
|
||||
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
|
||||
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
|
||||
(declare-fun |arr_4_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |a_6_0| () Int)
|
||||
(declare-fun |x_8_0| () Int)
|
||||
(declare-fun |arr_4_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |expr_12_0| () Int)
|
||||
(declare-fun |expr_13_0| () Int)
|
||||
(declare-fun |expr_14_1| () Bool)
|
||||
(declare-fun |expr_17_0| () Int)
|
||||
(declare-fun |expr_18_1| () Int)
|
||||
(declare-fun |x_8_1| () Int)
|
||||
(declare-fun |expr_20_0| () Int)
|
||||
(declare-fun |expr_25_1| () Int)
|
||||
(declare-fun |expr_26_1| () Int)
|
||||
(declare-fun |expr_28_0| () Int)
|
||||
(declare-fun |expr_29_0| () Int)
|
||||
(declare-fun |d_div_mod_0_0| () Int)
|
||||
(declare-fun |r_div_mod_0_0| () Int)
|
||||
(declare-fun |expr_30_1| () Int)
|
||||
(declare-fun |expr_32_0| () Int)
|
||||
(declare-fun |expr_35_0| () Int)
|
||||
(declare-fun |state_1| () |state_type|)
|
||||
(declare-fun |state_2| () |state_type|)
|
||||
(declare-fun |state_3| () |state_type|)
|
||||
(declare-fun |expr_39_0| () Int)
|
||||
(declare-fun |expr_40_0| () Int)
|
||||
(declare-fun |expr_41_1| () Bool)
|
||||
(declare-fun |expr_44_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_44_length_pair_1| () |uint_array_tuple|)
|
||||
(declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
|
||||
(declare-fun |expr_49_length_pair_0| () |uint_array_tuple|)
|
||||
(declare-fun |expr_50_0| () Int)
|
||||
(declare-fun |expr_51_1| () Int)
|
||||
|
||||
(assert (and (and (and true true) (and (=> (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (=> (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))))) (< (- expr_17_0 1) 0)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| a_6_0))
|
||||
(declare-const |EVALEXPR_1| Int)
|
||||
(assert (= |EVALEXPR_1| x_8_0))
|
||||
(declare-const |EVALEXPR_2| Int)
|
||||
(assert (= |EVALEXPR_2| (- expr_17_0 1)))
|
||||
(check-sat)
|
||||
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
|
||||
"}},"errors":[{"component":"general","errorCode":"4144","formattedMessage":"Warning: BMC: Underflow (resulting value less than 0) happens here.
|
||||
--> A:8:7:
|
||||
|
|
||||
|
||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
@ -14,7 +14,7 @@ contract LoopFor2 {
|
||||
uint i;
|
||||
while (i < n) {
|
||||
b[i] = i + 1;
|
||||
c[i] = b[i];
|
||||
//c[i] = b[i]; // Removed because of Spacer's nondeterminism
|
||||
++i;
|
||||
}
|
||||
//assert(b[0] == c[0]); // Removed because of Spacer's nondeterminism
|
||||
@ -26,8 +26,6 @@ contract LoopFor2 {
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 6368: (288-292): CHC: Out of bounds access might happen here.
|
||||
// Warning 6368: (312-316): CHC: Out of bounds access might happen here.
|
||||
// Warning 6368: (305-309): CHC: Out of bounds access might happen here.
|
||||
// Warning 6368: (411-415): CHC: Out of bounds access happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\na = []\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
|
||||
// Warning 6328: (404-423): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
|
||||
// Warning 6328: (427-446): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
|
||||
// Warning 6368: (459-463): CHC: Out of bounds access happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\na = []\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
|
||||
// Warning 6328: (452-471): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
|
||||
// Warning 6328: (475-494): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user