cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #10572 from ethereum/smt_abi

Browse Source 
[SMTChecker] Support ABI functions as uninterpreted functions
This commit is contained in:
Đorđe Mijović 2020-12-17 15:53:05 +01:00 committed by GitHub
commit 9328503265
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
98 changed files with 1730 additions and 673 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -1,5 +1,7 @@
### 0.8.1 (unreleased)
Compiler Features:
* SMTChecker: Support ABI functions as uninterpreted functions.
### 0.8.0 (2020-12-16)

4
libsolidity/formal/CHC.cpp
View File

@ -916,7 +916,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state(1)};
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
vector<smtutil::Expression>{state().state(2)} +
@ -1160,7 +1160,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
solAssert(false, "Unreachable!");
};
errorFlag().increaseIndex();
vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().crypto(), state().tx(), state().state()};
vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
auto const* contract = function->annotation().contract;
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;

29
libsolidity/formal/Predicate.cpp
View File

@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) co
auto const* fun = programFunction();
solAssert(fun, "");
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in preInputVars.
auto first = _args.begin() + 5 + static_cast<int>(stateVars->size());
auto first = _args.begin() + 6 + static_cast<int>(stateVars->size());
auto last = first + static_cast<int>(fun->parameters().size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
solAssert(last >= _args.begin() && last <= _args.end(), "");
@ -189,8 +189,8 @@ string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) co
vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expression> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of the summary predicate of a contract without constructor is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of the summary predicate of a contract without constructor is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
/// Here we are interested in postStateVars.
auto stateVars = stateVariables();
solAssert(stateVars.has_value(), "");
@ -199,12 +199,12 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
vector<smtutil::Expression>::const_iterator stateLast;
if (auto const* function = programFunction())
{
stateFirst = _args.begin() + 5 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
stateFirst = _args.begin() + 6 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else if (programContract())
{
stateFirst = _args.begin() + 6 + static_cast<int>(stateVars->size());
stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size());
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else
@ -221,7 +221,7 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expression> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in postInputVars.
auto const* function = programFunction();
solAssert(function, "");
@ -231,7 +231,7 @@ vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expre
auto const& inParams = function->parameters();
auto first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
auto last = first + static_cast<int>(inParams.size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
@ -245,7 +245,7 @@ vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expre
vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expression> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in outputVars.
auto const* function = programFunction();
solAssert(function, "");
@ -255,7 +255,7 @@ vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expr
auto const& inParams = function->parameters();
auto first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
solAssert(first >= _args.begin() && first <= _args.end(), "");
@ -311,6 +311,11 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
{
return {};
}
catch(invalid_argument const&)
{
return {};
}
// Limit this counterexample size to 1k.
// Some OSs give you "unlimited" memory through swap and other virtual memory,
// so purely relying on bad_alloc being thrown is not a good idea.
@ -382,6 +387,10 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
{
return true;
}
catch (invalid_argument const&)
{
return true;
}
optional<string> elemStr = expressionToString(_expr.arguments.at(2), _type.baseType());
if (!elemStr)
return false;

12
libsolidity/formal/PredicateInstance.cpp
View File

@ -30,14 +30,14 @@ namespace solidity::frontend::smt
smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.crypto(0), state.state(0)};
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)};
return _pred(stateExprs + initialStateVariables(_contract, _context));
}
smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.crypto(0), state.state()};
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context));
}
@ -58,7 +58,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex
return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context));
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
}
@ -69,7 +69,7 @@ smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _co
return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context));
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()};
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
state.newState();
stateExprs += vector<smtutil::Expression>{state.state()};
stateExprs += currentStateVariables(contract, _context);
@ -145,7 +145,7 @@ vector<smtutil::Expression> currentFunctionVariablesForDefinition(
)
{
auto& state = _context.state();
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)};
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)};
exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
exprs += vector<smtutil::Expression>{state.state()};
@ -162,7 +162,7 @@ vector<smtutil::Expression> currentFunctionVariablesForCall(
)
{
auto& state = _context.state();
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()};
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });

6
libsolidity/formal/PredicateSort.cpp
View File

@ -31,7 +31,7 @@ namespace solidity::frontend::smt
SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{
return make_shared<FunctionSort>(
vector<SortPointer>{_state.thisAddressSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort
);
}
@ -54,7 +54,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
auto varSorts = stateSorts(_contract);
vector<SortPointer> stateSort{_state.stateSort()};
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
SortProvider::boolSort
);
}
@ -66,7 +66,7 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
varSorts +
inputSorts +
vector<SortPointer>{_state.stateSort()} +

8
libsolidity/formal/PredicateSort.h
View File

@ -33,7 +33,7 @@ namespace solidity::frontend::smt
*
* 1. Interface
* The idle state of a contract. Signature:
* interface(this, cryptoFunctions, blockchainState, stateVariables).
* interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables).
*
* 2. Nondet interface
* The nondeterminism behavior of a contract. Signature:
@ -43,15 +43,15 @@ namespace solidity::frontend::smt
* The summary of a contract's deployment procedure.
* Signature:
* If the contract has a constructor function, this is the same as the summary of that function. Otherwise:
* constructor_summary(error, this, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables').
* constructor_summary(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables').
*
* 4. Function entry/summary
* The entry point of a function definition. Signature:
* function_entry(error, this, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
* function_entry(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
*
* 5. Function body
* Use for any predicate within a function. Signature:
* function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
* function_body(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
*/
/// @returns the interface predicate sort for _contract.

95
libsolidity/formal/SMTEncoder.cpp
View File

@ -71,7 +71,12 @@ bool SMTEncoder::analyze(SourceUnit const& _source)
analysis = false;
}
return analysis;
if (!analysis)
return false;
m_context.state().prepareForSourceUnit(_source);
return true;
}
bool SMTEncoder::visit(ContractDefinition const& _contract)
@ -680,13 +685,15 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
if (isPublicGetter(_funCall.expression()))
visitPublicGetter(_funCall);
break;
case FunctionType::Kind::ABIDecode:
case FunctionType::Kind::ABIEncode:
case FunctionType::Kind::ABIEncodePacked:
case FunctionType::Kind::ABIEncodeWithSelector:
case FunctionType::Kind::ABIEncodeWithSignature:
visitABIFunction(_funCall);
break;
case FunctionType::Kind::Internal:
case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCall:
case FunctionType::Kind::BareCallCode:
case FunctionType::Kind::BareDelegateCall:
case FunctionType::Kind::BareStaticCall:
case FunctionType::Kind::Creation:
break;
case FunctionType::Kind::KECCAK256:
case FunctionType::Kind::ECRecover:
@ -728,6 +735,11 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::ObjectCreation:
visitObjectCreation(_funCall);
return;
case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCall:
case FunctionType::Kind::BareCallCode:
case FunctionType::Kind::BareDelegateCall:
case FunctionType::Kind::Creation:
default:
m_errorReporter.warning(
4588_error,
@ -786,6 +798,50 @@ void SMTEncoder::visitRequire(FunctionCall const& _funCall)
addPathImpliedExpression(expr(*args.front()));
}
void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
{
auto symbFunction = m_context.state().abiFunction(&_funCall);
auto const& [name, inTypes, outTypes] = m_context.state().abiFunctionTypes(&_funCall);
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind();
auto const& args = _funCall.sortedArguments();
auto argsActualLength = kind == FunctionType::Kind::ABIDecode ? 1 : args.size();
vector<smtutil::Expression> symbArgs;
solAssert(inTypes.size() == argsActualLength, "");
for (unsigned i = 0; i < argsActualLength; ++i)
if (args.at(i))
symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i)));
optional<smtutil::Expression> arg;
if (inTypes.size() == 1)
arg = expr(*args.at(0));
else
{
auto inputSort = dynamic_cast<smtutil::ArraySort&>(*symbFunction.sort).domain;
arg = smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""),
symbArgs
);
}
auto out = smtutil::Expression::select(symbFunction, *arg);
if (outTypes.size() == 1)
defineExpr(_funCall, out);
else
{
auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
solAssert(symbTuple, "");
solAssert(symbTuple->components().size() == outTypes.size(), "");
solAssert(out.sort->kind == smtutil::Kind::Tuple, "");
symbTuple->increaseIndex();
for (unsigned i = 0; i < symbTuple->components().size(); ++i)
m_context.addAssertion(symbTuple->component(i) == smtutil::Expression::tuple_get(out, i));
}
}
void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
{
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
@ -2672,6 +2728,33 @@ RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
return nullptr;
}
set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
{
struct ABIFunctions: public ASTConstVisitor
{
ABIFunctions(ASTNode const* _node) { _node->accept(*this); }
void endVisit(FunctionCall const& _funCall)
{
if (*_funCall.annotation().kind == FunctionCallKind::FunctionCall)
switch (dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type).kind())
{
case FunctionType::Kind::ABIEncode:
case FunctionType::Kind::ABIEncodePacked:
case FunctionType::Kind::ABIEncodeWithSelector:
case FunctionType::Kind::ABIEncodeWithSignature:
case FunctionType::Kind::ABIDecode:
abiCalls.insert(&_funCall);
break;
default: {}
}
}
set<FunctionCall const*> abiCalls;
};
return ABIFunctions(_node).abiCalls;
}
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
{
FunctionDefinition const* funDef = functionCallToDefinition(_funCall);

3
libsolidity/formal/SMTEncoder.h
View File

@ -87,6 +87,8 @@ public:
/// RationalNumberType or can be const evaluated, and nullptr otherwise.
static RationalNumberType const* isConstant(Expression const& _expr);
static std::set<FunctionCall const*> collectABICalls(ASTNode const* _node);
protected:
// TODO: Check that we do not have concurrent reads and writes to a variable,
// because the order of expression evaluation is undefined
@ -159,6 +161,7 @@ protected:
void initFunction(FunctionDefinition const& _function);
void visitAssert(FunctionCall const& _funCall);
void visitRequire(FunctionCall const& _funCall);
void visitABIFunction(FunctionCall const& _funCall);
void visitCryptoFunction(FunctionCall const& _funCall);
void visitGasLeft(FunctionCall const& _funCall);
virtual void visitAddMulMod(FunctionCall const& _funCall);

136
libsolidity/formal/SymbolicState.cpp
View File

@ -20,6 +20,7 @@
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SMTEncoder.h>
using namespace std;
using namespace solidity;
@ -77,6 +78,10 @@ void SymbolicState::reset()
m_state.reset();
m_tx.reset();
m_crypto.reset();
/// We don't reset m_abi's pointer nor clear m_abiMembers on purpose,
/// since it only helps to keep the already generated types.
solAssert(m_abi, "");
m_abi->reset();
}
smtutil::Expression SymbolicState::balances() const
@ -149,6 +154,14 @@ smtutil::Expression SymbolicState::txConstraints(FunctionDefinition const& _func
return conj;
}
void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
{
set<FunctionCall const*> abiCalls = SMTEncoder::collectABICalls(&_source);
for (auto const& source: _source.referencedSourceUnits(true))
abiCalls += SMTEncoder::collectABICalls(source);
buildABIFunctions(abiCalls);
}
/// Private helpers.
void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
@ -160,3 +173,126 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression
);
m_state.assignMember("balances", newBalances);
}
void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFunctions)
{
map<string, SortPointer> functions;
for (auto const* funCall: _abiFunctions)
{
auto t = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type);
auto const& args = funCall->sortedArguments();
auto const& paramTypes = t->parameterTypes();
auto const& returnTypes = t->returnParameterTypes();
auto argTypes = [](auto const& _args) {
return applyMap(_args, [](auto arg) { return arg->annotation().type; });
};
/// Since each abi.* function may have a different number of input/output parameters,
/// we generically compute those types.
vector<TypePointer> inTypes;
vector<TypePointer> outTypes;
if (t->kind() == FunctionType::Kind::ABIDecode)
{
/// abi.decode : (bytes, tuple_of_types(return_types)) -> (return_types)
inTypes.emplace_back(TypeProvider::bytesMemory());
auto const* tupleType = dynamic_cast<TupleType const*>(args.at(1)->annotation().type);
solAssert(tupleType, "");
for (auto t: tupleType->components())
{
auto typeType = dynamic_cast<TypeType const*>(t);
solAssert(typeType, "");
outTypes.emplace_back(typeType->actualType());
}
}
else
{
outTypes = returnTypes;
if (
t->kind() == FunctionType::Kind::ABIEncodeWithSelector ||
t->kind() == FunctionType::Kind::ABIEncodeWithSignature
)
{
/// abi.encodeWithSelector : (bytes4, one_or_more_types) -> bytes
/// abi.encodeWithSignature : (string, one_or_more_types) -> bytes
inTypes.emplace_back(paramTypes.front());
inTypes += argTypes(vector<ASTPointer<Expression const>>(args.begin() + 1, args.end()));
}
else
{
/// abi.encode/abi.encodePacked : one_or_more_types -> bytes
solAssert(
t->kind() == FunctionType::Kind::ABIEncode ||
t->kind() == FunctionType::Kind::ABIEncodePacked,
""
);
inTypes = argTypes(args);
}
}
/// Rational numbers and string literals add the concrete values to the type name,
/// so we replace them by uint256 and bytes since those are the same as their SMT types.
/// TODO we could also replace all types by their ABI type.
auto replaceTypes = [](auto& _types) {
for (auto& t: _types)
if (t->category() == frontend::Type::Category::RationalNumber)
t = TypeProvider::uint256();
else if (t->category() == frontend::Type::Category::StringLiteral)
t = TypeProvider::bytesMemory();
};
replaceTypes(inTypes);
replaceTypes(outTypes);
auto name = t->richIdentifier();
for (auto paramType: inTypes + outTypes)
name += "_" + paramType->richIdentifier();
m_abiMembers[funCall] = {name, inTypes, outTypes};
if (functions.count(name))
continue;
/// If there is only one input or output parameter, we use that type directly.
/// Otherwise we create a tuple wrapping the necessary input or output types.
auto typesToSort = [](auto const& _types, string const& _name) -> shared_ptr<Sort> {
if (_types.size() == 1)
return smtSort(*_types.front());
vector<string> inNames;
vector<SortPointer> sorts;
for (unsigned i = 0; i < _types.size(); ++i)
{
inNames.emplace_back(_name + "_input_" + to_string(i));
sorts.emplace_back(smtSort(*_types.at(i)));
}
return make_shared<smtutil::TupleSort>(
_name + "_input",
inNames,
sorts
);
};
auto functionSort = make_shared<smtutil::ArraySort>(
typesToSort(inTypes, name),
typesToSort(outTypes, name)
);
functions[name] = functionSort;
}
m_abi = make_unique<BlockchainVariable>("abi", move(functions), m_context);
}
smtutil::Expression SymbolicState::abiFunction(frontend::FunctionCall const* _funCall)
{
solAssert(m_abi, "");
return m_abi->member(get<0>(m_abiMembers.at(_funCall)));
}
SymbolicState::SymbolicABIFunction const& SymbolicState::abiFunctionTypes(FunctionCall const* _funCall) const
{
return m_abiMembers.at(_funCall);
}

28
libsolidity/formal/SymbolicState.h
View File

@ -138,10 +138,32 @@ public:
smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); }
//@}
/// ABI functions.
//@{
/// Calls the internal methods that build the symbolic ABI functions
/// based on the abi.* calls in _source and referenced sources.
void prepareForSourceUnit(SourceUnit const& _source);
smtutil::Expression abiFunction(FunctionCall const* _funCall);
using SymbolicABIFunction = std::tuple<
std::string,
std::vector<TypePointer>,
std::vector<TypePointer>
>;
SymbolicABIFunction const& abiFunctionTypes(FunctionCall const* _funCall) const;
smtutil::Expression abi() const { solAssert(m_abi, ""); return m_abi->value(); }
smtutil::Expression abi(unsigned _idx) const { solAssert(m_abi, ""); return m_abi->value(_idx); }
smtutil::SortPointer const& abiSort() const { solAssert(m_abi, ""); return m_abi->sort(); }
void newABI() { solAssert(m_abi, ""); m_abi->newVar(); }
//@}
private:
/// Adds _value to _account's balance.
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
/// Builds m_abi based on the abi.* calls _abiFunctions.
void buildABIFunctions(std::set<FunctionCall const*> const& _abiFunctions);
EncodingContext& m_context;
SymbolicIntVariable m_error{
@ -213,6 +235,12 @@ private:
},
m_context
};
/// Tuple containing all used ABI functions.
std::unique_ptr<BlockchainVariable> m_abi;
/// Maps ABI functions calls to their tuple names generated by
/// `buildABIFunctions`.
std::map<FunctionCall const*, SymbolicABIFunction> m_abiMembers;
};
}

4
libsolidity/formal/SymbolicTypes.cpp
View File

@ -556,6 +556,10 @@ smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, fronte
solAssert(intType, "");
return _expr >= minValue(*intType) && _expr <= maxValue(*intType);
}
else if (isArray(*_type) || isMapping(*_type))
/// Length cannot be negative.
return smtutil::Expression::tuple_get(_expr, 1) >= 0;
return smtutil::Expression(true);
}

4
test/cmdlineTests/standard_model_checker_engine_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x238aade411d63d50406236089e28f3770d51f95888222fdb838f930911e0f763":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x88f5b0fdb94a459ff6e3f6ee6fd482520d1d0ddeb45b14acd5060b6ecfe818dd":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -10,6 +10,8 @@
(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-fun |x_4_0| () Int)
(declare-fun |expr_8_0| () Int)
(declare-fun |expr_9_0| () Int)

236
test/cmdlineTests/standard_model_checker_timeout_all/output.json
View File

@ -1,57 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x0d6f843ef6990bfad1918be96d1aad42b5d7ca87a171d0ac34009e0d4b6e8e03":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_15_0| () Int)
(declare-fun |r_div_mod_15_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
(check-sat)
","0x3091365cefd5a713eea87735305ab53c75303343ebf74b77d3578ae0b73c64a2":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(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 (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
(check-sat)
","0x6b268fc2d87ebda3f3b3b93c8d0b2b5374fd3bd33387113b9ee138a85c142dae":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x17eb7e6c3c9675e486088d4f0c4091012e0d7d510a5b9c0d2912b9c57e5456d5":"(set-option :produce-models true)
(set-option :timeout 1000)
(set-logic ALL)
(declare-fun |error_0| () Int)
@ -64,6 +11,8 @@
(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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
@ -86,62 +35,9 @@
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
(check-sat)
","0xa81ce8317a79fc74d85d9edfe56caf9b0274a7da4556bfb418652051e0bfa679":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(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 (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
(check-sat)
","0xaec7aba847ba235b585e4c7e6ec8d8eee964e76bd40a02e00af3354acede95d8":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_15_0| () Int)
(declare-fun |r_div_mod_15_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
(check-sat)
","0xe6aad7b5a7ba681908e47e11921c93815f9a4cdd90ef82dd79a60fcac94492c9":"(set-option :produce-models true)
","0x2b53b933e67842c0d550b4a25069debb0949a378a0c560f021c914b93615b1fc":"(set-option :produce-models true)
(set-option :timeout 1000)
(set-logic ALL)
(declare-fun |error_0| () Int)
@ -154,6 +50,8 @@
(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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
@ -203,7 +101,7 @@
(assert (= |EVALEXPR_3| r_34_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| ))
","0xf877f10b1dc480ae2403c9376947f543da579bf3aff7dfaa2f946e300b81d305":"(set-option :produce-models true)
","0x47c361f3e8e669764e26b1b1498b9455e7c589547ab5b90e5efdd82b14dfbd3a":"(set-option :produce-models true)
(set-option :timeout 1000)
(set-logic ALL)
(declare-fun |error_0| () Int)
@ -216,6 +114,90 @@
(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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_15_0| () Int)
(declare-fun |r_div_mod_15_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
(check-sat)
","0xcb2117c40da91e8a86270886eca9e12cf9524141e96a95d18711d0c97f974086":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(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 (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
(check-sat)
","0xcc5b317723ba883782a53eb35e82063ffcd1eee56de51d63c6c2971413b03d3a":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(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 (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
(check-sat)
","0xdee28d62f23c1f8b40466ff649c947e3e5793e66b2049a92d0de96208e441565":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
@ -238,7 +220,39 @@
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
(check-sat)
","0xf4cd8362dc82ca7448e9c27bbf7b391942d5110c7b29a1dba6a4e8037a7f68cf":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_15_0| () Int)
(declare-fun |r_div_mod_15_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
(check-sat)
"}},"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation might happen here.
--> A:6:85:

834
test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
View File

@ -1,185 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x0e2ec6d70e3de7ac14f07c9bbb08f9436e3b832ae8456d340e4d4a8b8712c7f5":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_37_0| () Int)
(declare-fun |expr_38_0| () Int)
(declare-fun |d_div_mod_2_0| () Int)
(declare-fun |r_div_mod_2_0| () Int)
(declare-fun |expr_39_1| () Int)
(declare-fun |r_34_1| () Int)
(declare-fun |expr_42_0| () Int)
(declare-fun |expr_43_0| () Int)
(declare-fun |d_div_mod_3_0| () Int)
(declare-fun |r_div_mod_3_0| () Int)
(declare-fun |expr_44_1| () Int)
(declare-fun |expr_45_0| () Int)
(declare-fun |expr_46_1| () Bool)
(assert (and (and (and true true) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))) (= expr_27_0 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| y_6_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| k_8_0))
(declare-const |EVALEXPR_3| Int)
(assert (= |EVALEXPR_3| r_34_0))
(declare-const |EVALEXPR_4| Int)
(assert (= |EVALEXPR_4| expr_27_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
","0x3091365cefd5a713eea87735305ab53c75303343ebf74b77d3578ae0b73c64a2":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(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 (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
(check-sat)
","0x46c0f34a4da6b31138e9238be92256a3c472a5a24c88371ef680f78e0c520cb6":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_37_0| () Int)
(declare-fun |expr_38_0| () Int)
(declare-fun |d_div_mod_2_0| () Int)
(declare-fun |r_div_mod_2_0| () Int)
(declare-fun |expr_39_1| () Int)
(declare-fun |r_34_1| () Int)
(declare-fun |expr_42_0| () Int)
(declare-fun |expr_43_0| () Int)
(declare-fun |d_div_mod_3_0| () Int)
(declare-fun |r_div_mod_3_0| () Int)
(declare-fun |expr_44_1| () Int)
(declare-fun |expr_45_0| () Int)
(declare-fun |expr_46_1| () Bool)
(assert (and (and (and true true) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))) (= expr_38_0 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| y_6_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| k_8_0))
(declare-const |EVALEXPR_3| Int)
(assert (= |EVALEXPR_3| r_34_0))
(declare-const |EVALEXPR_4| Int)
(assert (= |EVALEXPR_4| expr_38_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
","0x6378f27de46d517b5bafe774eab66c12cb656dbd031cb5e710f07b1bfd6c5f79":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
(check-sat)
","0x7db419e89d4bb9fbaa4bda7fd522223a515177ff577a6d381e7f2b7f4612582b":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x0017aa24ac5e0f5ac607f58201176163a5609823b2487aec1cdb16e925cfb577":"(set-option :produce-models true)
(set-option :timeout 1000)
(set-logic ALL)
(declare-fun |error_0| () Int)
@ -192,6 +11,8 @@
(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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
@ -209,230 +30,7 @@
(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1))
(check-sat)
","0x7de8eaf2518b47eec1afadbebacdfa7d93a1878e0f1b6eef91b8a80f1246937e":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
(check-sat)
","0x8c4f3faef8ad4a2fe9935f16ec93e2df20f5a3831be51c13afe060774658141c":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
(check-sat)
","0xa4666c5d197afd69bd82af703fb694c1d3cdd8926ab480fc42e69231134d9265":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_37_0| () Int)
(declare-fun |expr_38_0| () Int)
(declare-fun |d_div_mod_2_0| () Int)
(declare-fun |r_div_mod_2_0| () Int)
(declare-fun |expr_39_1| () Int)
(declare-fun |r_34_1| () Int)
(declare-fun |expr_42_0| () Int)
(declare-fun |expr_43_0| () Int)
(declare-fun |d_div_mod_3_0| () Int)
(declare-fun |r_div_mod_3_0| () Int)
(declare-fun |expr_44_1| () Int)
(declare-fun |expr_45_0| () Int)
(declare-fun |expr_46_1| () Bool)
(assert (and (and (and true true) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))) (= expr_19_0 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| y_6_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| k_8_0))
(declare-const |EVALEXPR_3| Int)
(assert (= |EVALEXPR_3| r_34_0))
(declare-const |EVALEXPR_4| Int)
(assert (= |EVALEXPR_4| expr_19_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
","0xa81ce8317a79fc74d85d9edfe56caf9b0274a7da4556bfb418652051e0bfa679":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(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 (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
(check-sat)
","0xa96a68b7853fcc0a10dd525c3ff838e3bfac425b104c44b240623f7a35aee6f1":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_37_0| () Int)
(declare-fun |expr_38_0| () Int)
(declare-fun |d_div_mod_2_0| () Int)
(declare-fun |r_div_mod_2_0| () Int)
(declare-fun |expr_39_1| () Int)
(declare-fun |r_34_1| () Int)
(declare-fun |expr_42_0| () Int)
(declare-fun |expr_43_0| () Int)
(declare-fun |d_div_mod_3_0| () Int)
(declare-fun |r_div_mod_3_0| () Int)
(declare-fun |expr_44_1| () Int)
(declare-fun |expr_45_0| () Int)
(declare-fun |expr_46_1| () Bool)
(assert (and (and (and true true) (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_3_0)) (and (and (<= 0 r_div_mod_3_0) (or (= expr_43_0 0) (< r_div_mod_3_0 expr_43_0))) (and (= (+ (* d_div_mod_3_0 expr_43_0) r_div_mod_3_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| y_6_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| k_8_0))
(declare-const |EVALEXPR_3| Int)
(assert (= |EVALEXPR_3| r_34_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| ))
","0xcc1de975d2f5e9b3e4ff9b4f46c8248513ac3b755b60f8a630a46d12b4b11f9a":"(set-option :produce-models true)
","0x01adbdf930a8c2d705ee70e5e78e29c29dac476aa100fcb798f868f51b26204f":"(set-option :produce-models true)
(set-option :timeout 1000)
(set-logic ALL)
(declare-fun |error_0| () Int)
@ -445,6 +43,8 @@
(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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
@ -496,6 +96,428 @@
(assert (= |EVALEXPR_4| expr_43_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
","0x0240b78036d9401081928b0678ac1093bc5f539b272727c2f666f50cbc42f152":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_37_0| () Int)
(declare-fun |expr_38_0| () Int)
(declare-fun |d_div_mod_2_0| () Int)
(declare-fun |r_div_mod_2_0| () Int)
(declare-fun |expr_39_1| () Int)
(declare-fun |r_34_1| () Int)
(declare-fun |expr_42_0| () Int)
(declare-fun |expr_43_0| () Int)
(declare-fun |d_div_mod_3_0| () Int)
(declare-fun |r_div_mod_3_0| () Int)
(declare-fun |expr_44_1| () Int)
(declare-fun |expr_45_0| () Int)
(declare-fun |expr_46_1| () Bool)
(assert (and (and (and true true) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))) (= expr_19_0 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| y_6_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| k_8_0))
(declare-const |EVALEXPR_3| Int)
(assert (= |EVALEXPR_3| r_34_0))
(declare-const |EVALEXPR_4| Int)
(assert (= |EVALEXPR_4| expr_19_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
","0x330edc0eeae79b3a01e99e82b2ee2b82fb55bb3a293e5bdf000b21347c367bf5":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1)))
(check-sat)
","0x65adca9cfdac21d489384711fb7cecea5c811b2d9ea3115e661640f5c4f6b653":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_37_0| () Int)
(declare-fun |expr_38_0| () Int)
(declare-fun |d_div_mod_2_0| () Int)
(declare-fun |r_div_mod_2_0| () Int)
(declare-fun |expr_39_1| () Int)
(declare-fun |r_34_1| () Int)
(declare-fun |expr_42_0| () Int)
(declare-fun |expr_43_0| () Int)
(declare-fun |d_div_mod_3_0| () Int)
(declare-fun |r_div_mod_3_0| () Int)
(declare-fun |expr_44_1| () Int)
(declare-fun |expr_45_0| () Int)
(declare-fun |expr_46_1| () Bool)
(assert (and (and (and true true) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))) (= expr_27_0 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| y_6_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| k_8_0))
(declare-const |EVALEXPR_3| Int)
(assert (= |EVALEXPR_3| r_34_0))
(declare-const |EVALEXPR_4| Int)
(assert (= |EVALEXPR_4| expr_27_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
","0x6615bd1d9fcf33421097f19e3ad0fb38bcd1d1191aa6ae4f0689699322e0c0d9":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1))
(check-sat)
","0x7f31c70550c1d2f3c45a8c0e8468fe1477b68f37f97127d10746210f1fe97f96":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_37_0| () Int)
(declare-fun |expr_38_0| () Int)
(declare-fun |d_div_mod_2_0| () Int)
(declare-fun |r_div_mod_2_0| () Int)
(declare-fun |expr_39_1| () Int)
(declare-fun |r_34_1| () Int)
(declare-fun |expr_42_0| () Int)
(declare-fun |expr_43_0| () Int)
(declare-fun |d_div_mod_3_0| () Int)
(declare-fun |r_div_mod_3_0| () Int)
(declare-fun |expr_44_1| () Int)
(declare-fun |expr_45_0| () Int)
(declare-fun |expr_46_1| () Bool)
(assert (and (and (and true true) (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_3_0)) (and (and (<= 0 r_div_mod_3_0) (or (= expr_43_0 0) (< r_div_mod_3_0 expr_43_0))) (and (= (+ (* d_div_mod_3_0 expr_43_0) r_div_mod_3_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| y_6_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| k_8_0))
(declare-const |EVALEXPR_3| Int)
(assert (= |EVALEXPR_3| r_34_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| ))
","0x9bd658c40e2e05920cb7023c6bae797f58090029e71d5c679c9b55d2f016307e":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(declare-fun |expr_26_0| () Int)
(declare-fun |expr_27_0| () Int)
(declare-fun |d_div_mod_1_0| () Int)
(declare-fun |r_div_mod_1_0| () Int)
(declare-fun |expr_28_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_1| () Bool)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int)
(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_37_0| () Int)
(declare-fun |expr_38_0| () Int)
(declare-fun |d_div_mod_2_0| () Int)
(declare-fun |r_div_mod_2_0| () Int)
(declare-fun |expr_39_1| () Int)
(declare-fun |r_34_1| () Int)
(declare-fun |expr_42_0| () Int)
(declare-fun |expr_43_0| () Int)
(declare-fun |d_div_mod_3_0| () Int)
(declare-fun |r_div_mod_3_0| () Int)
(declare-fun |expr_44_1| () Int)
(declare-fun |expr_45_0| () Int)
(declare-fun |expr_46_1| () Bool)
(assert (and (and (and true true) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))) (= expr_38_0 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| y_6_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| k_8_0))
(declare-const |EVALEXPR_3| Int)
(assert (= |EVALEXPR_3| r_34_0))
(declare-const |EVALEXPR_4| Int)
(assert (= |EVALEXPR_4| expr_38_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
","0xc47149a0c48b40420cedfb8f77dc50e53fdad2f202344393df79022cd0b2105c":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_20_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_22_1| () Bool)
(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1)))
(check-sat)
","0xcb2117c40da91e8a86270886eca9e12cf9524141e96a95d18711d0c97f974086":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(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 (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1)))
(check-sat)
","0xcc5b317723ba883782a53eb35e82063ffcd1eee56de51d63c6c2971413b03d3a":"(set-option :produce-models true)
(set-option :timeout 1000)
(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.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-fun |x_4_0| () Int)
(declare-fun |y_6_0| () Int)
(declare-fun |k_8_0| () Int)
(declare-fun |r_34_0| () Int)
(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 (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1))
(check-sat)
"}},"errors":[{"component":"general","errorCode":"7812","formattedMessage":"Warning: BMC: Assertion violation might happen here.
--> A:6:85:
|

67
test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol Normal file
View File

@ -0,0 +1,67 @@
pragma experimental SMTChecker;
pragma abicoder v2;
contract C {
function abiDecodeArray(bytes memory b1, bytes memory b2) public pure {
(uint[] memory a, uint[] memory b) = abi.decode(b1, (uint[], uint[]));
assert(a.length == b.length); // should fail
(uint[] memory c, uint[] memory d) = abi.decode(b1, (uint[], uint[]));
assert(a.length == c.length);
assert(a.length == d.length); // should fail
assert(b.length == d.length);
assert(b.length == c.length); // should fail
(uint[] memory e, uint[] memory f, uint[] memory g) = abi.decode(b1, (uint[], uint[], uint[]));
assert(e.length == a.length); // should fail
assert(f.length == b.length); // should fail
assert(e.length == g.length); // should fail
(uint[][] memory h, uint[][][] memory i, uint j) = abi.decode(b1, (uint[][], uint[][][], uint));
assert(h[j].length == i[j][j].length); // should fail
(uint[] memory k, uint[] memory l) = abi.decode(b2, (uint[], uint[]));
assert(k.length == a.length); // should fail
assert(k.length == l.length); // should fail
assert(l.length == b.length); // should fail
}
}
// ----
// Warning 8364: (194-200): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (202-208): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (315-321): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (323-329): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (564-570): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (572-578): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (580-586): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (801-807): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (801-809): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-817): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (811-819): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-821): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (943-949): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (951-957): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 6328: (214-242): CHC: Assertion violation happens here.
// Warning 6328: (367-395): CHC: Assertion violation happens here.
// Warning 6328: (446-474): CHC: Assertion violation happens here.
// Warning 6328: (592-620): CHC: Assertion violation happens here.
// Warning 6328: (639-667): CHC: Assertion violation happens here.
// Warning 6328: (686-714): CHC: Assertion violation happens here.
// Warning 6328: (833-870): CHC: Assertion violation happens here.
// Warning 6328: (963-991): CHC: Assertion violation happens here.
// Warning 6328: (1010-1038): CHC: Assertion violation happens here.
// Warning 6328: (1057-1085): CHC: Assertion violation happens here.
// Warning 8364: (194-200): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (202-208): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (315-321): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (323-329): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (564-570): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (572-578): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (580-586): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (801-807): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (801-809): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-817): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (811-819): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-821): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (943-949): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (951-957): Assertion checker does not yet implement type type(uint256[] memory)

30
test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol Normal file
View File

@ -0,0 +1,30 @@
pragma experimental SMTChecker;
contract C {
function abiDecodeSimple(bytes memory b1, bytes memory b2) public pure {
(uint x, uint y) = abi.decode(b1, (uint, uint));
(uint z, uint w) = abi.decode(b1, (uint, uint));
assert(x == z);
assert(x == y); // should fail
assert(y == w);
assert(z == w); // should fail
(uint a, uint b, bool c) = abi.decode(b1, (uint, uint, bool));
assert(a == x); // should fail
assert(b == y); // should fail
assert(c); // should fail
(uint k, uint l) = abi.decode(b2, (uint, uint));
assert(k == x); // should fail
assert(l == y); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (241-255): CHC: Assertion violation happens here.
// Warning 6328: (292-306): CHC: Assertion violation happens here.
// Warning 6328: (391-405): CHC: Assertion violation happens here.
// Warning 6328: (424-438): CHC: Assertion violation happens here.
// Warning 6328: (457-466): CHC: Assertion violation happens here.
// Warning 6328: (537-551): CHC: Assertion violation happens here.
// Warning 6328: (570-584): CHC: Assertion violation happens here.

31
test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice.sol Normal file
View File

@ -0,0 +1,31 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(bytes calldata data) external pure {
bytes memory b1 = abi.encode(data);
bytes memory b2 = abi.encode(data[0:]);
// should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately
assert(b1.length == b2.length); // fails for now
// Disabled because of Spacer nondeterminism
//bytes memory b3 = abi.encode(data[:data.length]);
// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
//assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encode(data[5:10]);
assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encode(data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
}
}
// ----
// Warning 6328: (311-341): CHC: Assertion violation happens here.
// Warning 1218: (694-724): CHC: Error trying to invoke SMT solver.
// Warning 6328: (694-724): CHC: Assertion violation might happen here.
// Warning 1218: (945-975): CHC: Error trying to invoke SMT solver.
// Warning 6328: (945-975): CHC: Assertion violation might happen here.
// Warning 4661: (694-724): BMC: Assertion violation happens here.
// Warning 4661: (945-975): BMC: Assertion violation happens here.

31
test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol Normal file
View File

@ -0,0 +1,31 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(uint[] calldata data) external pure {
bytes memory b1 = abi.encode(data);
bytes memory b2 = abi.encode(data[0:]);
// should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately
assert(b1.length == b2.length); // fails for now
bytes memory b3 = abi.encode(data[:data.length]);
// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encode(data[5:10]);
assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encode(data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
}
}
// ----
// Warning 6328: (312-342): CHC: Assertion violation happens here.
// Warning 6328: (548-578): CHC: Assertion violation happens here.
// Warning 1218: (644-674): CHC: Error trying to invoke SMT solver.
// Warning 6328: (644-674): CHC: Assertion violation might happen here.
// Warning 1218: (895-925): CHC: Error trying to invoke SMT solver.
// Warning 6328: (895-925): CHC: Assertion violation might happen here.
// Warning 4661: (644-674): BMC: Assertion violation happens here.
// Warning 4661: (895-925): BMC: Assertion violation happens here.

9
test/libsolidity/smtCheckerTests/abi/abi_encode_hash.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeHash(uint a, uint b) public pure {
require(a == b);
bytes memory b1 = abi.encode(a, a, a, a);
bytes memory b2 = abi.encode(b, a, b, a);
assert(keccak256(b1) == keccak256(b2));
}
}

36
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice.sol Normal file
View File

@ -0,0 +1,36 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedSlice(bytes calldata data) external pure {
bytes memory b1 = abi.encodePacked(data);
bytes memory b2 = abi.encodePacked(data[0:]);
// should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately
// Disabled because of Spacer nondeterminism
//assert(b1.length == b2.length); // fails for now
// Disabled because of Spacer nondeterminism
//bytes memory b3 = abi.encodePacked(data[:data.length]);
// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
//assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encodePacked(data[5:10]);
// Disabled because of Spacer nondeterminism
//assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encodePacked(data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
bytes memory b6 = abi.encode(data[5:10]);
// Disabled because of Spacer nondeterminism
//assert(b4.length == b6.length); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 2072: (159-174): Unused local variable.
// Warning 2072: (723-738): Unused local variable.
// Warning 2072: (1131-1146): Unused local variable.
// Warning 6328: (1079-1109): CHC: Assertion violation happens here.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol Normal file
View File

@ -0,0 +1,37 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedSlice(uint[] calldata data) external pure {
bytes memory b1 = abi.encodePacked(data);
bytes memory b2 = abi.encodePacked(data[0:]);
// should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately
assert(b1.length == b2.length); // fails for now
// Disabled because of Spacer nondeterminism
//bytes memory b3 = abi.encodePacked(data[:data.length]);
// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
//assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encodePacked(data[5:10]);
assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encodePacked(data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
bytes memory b6 = abi.encode(data[5:10]);
assert(b4.length == b6.length); // should fail
}
}
// ----
// Warning 6328: (330-360): CHC: Assertion violation happens here.
// Warning 1218: (725-755): CHC: Error trying to invoke SMT solver.
// Warning 6328: (725-755): CHC: Assertion violation might happen here.
// Warning 1218: (982-1012): CHC: Error trying to invoke SMT solver.
// Warning 6328: (982-1012): CHC: Assertion violation might happen here.
// Warning 1218: (1078-1108): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1078-1108): CHC: Assertion violation might happen here.
// Warning 4661: (725-755): BMC: Assertion violation happens here.
// Warning 4661: (982-1012): BMC: Assertion violation happens here.
// Warning 4661: (1078-1108): BMC: Assertion violation happens here.

16
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedHash(uint a, uint b) public pure {
require(a == b);
bytes memory b1 = abi.encodePacked(a, a, a, a);
bytes memory b2 = abi.encodePacked(b, a, b, a);
assert(keccak256(b1) == keccak256(b2));
bytes memory b3 = abi.encode(a, a, a, a);
assert(keccak256(b1) == keccak256(b3)); // should fail
}
}
// ----
// Warning 1218: (313-351): CHC: Error trying to invoke SMT solver.
// Warning 6328: (313-351): CHC: Assertion violation might happen here.
// Warning 4661: (313-351): BMC: Assertion violation happens here.

34
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol Normal file
View File

@ -0,0 +1,34 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedSimple(bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure {
require(x == y);
bytes memory b1 = abi.encodePacked(x, z, a);
bytes memory b2 = abi.encodePacked(y, z, a);
assert(b1.length == b2.length);
bytes memory b3 = abi.encodePacked(y, z, b);
assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encodePacked(t, z, a);
assert(b1.length == b4.length); // should fail
bytes memory b5 = abi.encodePacked(y, y, y, y, a, a, a);
assert(b1.length != b5.length); // should fail
assert(b1.length == b5.length); // should fail
bytes memory b6 = abi.encode(x, z, a);
assert(b1.length == b6.length); // should fail
}
}
// ----
// Warning 6328: (354-384): CHC: Assertion violation happens here.
// Warning 1218: (451-481): CHC: Error trying to invoke SMT solver.
// Warning 6328: (451-481): CHC: Assertion violation might happen here.
// Warning 1218: (560-590): CHC: Error trying to invoke SMT solver.
// Warning 6328: (560-590): CHC: Assertion violation might happen here.
// Warning 1218: (609-639): CHC: Error trying to invoke SMT solver.
// Warning 6328: (609-639): CHC: Assertion violation might happen here.
// Warning 6328: (700-730): CHC: Assertion violation happens here.
// Warning 4661: (451-481): BMC: Assertion violation happens here.
// Warning 4661: (560-590): BMC: Assertion violation happens here.
// Warning 4661: (609-639): BMC: Assertion violation happens here.

38
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol Normal file
View File

@ -0,0 +1,38 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedStringLiteral() public pure {
bytes memory b1 = abi.encodePacked("");
bytes memory b2 = abi.encodePacked("");
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b2.length);
bytes memory b3 = abi.encodePacked(bytes(""));
assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encodePacked(bytes24(""));
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b4.length);
bytes memory b5 = abi.encodePacked(string(""));
assert(b1.length == b5.length); // should fail
bytes memory b6 = abi.encode("");
assert(b1.length == b6.length); // should fail
}
}
// ----
// Warning 1218: (258-288): CHC: Error trying to invoke SMT solver.
// Warning 6328: (258-288): CHC: Assertion violation might happen here.
// Warning 1218: (342-372): CHC: Error trying to invoke SMT solver.
// Warning 6328: (342-372): CHC: Assertion violation might happen here.
// Warning 1218: (515-545): CHC: Error trying to invoke SMT solver.
// Warning 6328: (515-545): CHC: Assertion violation might happen here.
// Warning 1218: (600-630): CHC: Error trying to invoke SMT solver.
// Warning 6328: (600-630): CHC: Assertion violation might happen here.
// Warning 1218: (686-716): CHC: Error trying to invoke SMT solver.
// Warning 6328: (686-716): CHC: Assertion violation might happen here.
// Warning 4661: (258-288): BMC: Assertion violation happens here.
// Warning 4661: (342-372): BMC: Assertion violation happens here.
// Warning 4661: (515-545): BMC: Assertion violation happens here.
// Warning 4661: (600-630): BMC: Assertion violation happens here.
// Warning 4661: (686-716): BMC: Assertion violation happens here.

30
test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol Normal file
View File

@ -0,0 +1,30 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSimple(bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure {
require(x == y);
bytes memory b1 = abi.encode(x, z, a);
bytes memory b2 = abi.encode(y, z, a);
assert(b1.length == b2.length);
bytes memory b3 = abi.encode(y, z, b);
assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encode(t, z, a);
assert(b1.length == b4.length); // should fail
bytes memory b5 = abi.encode(y, y, y, y, a, a, a);
assert(b1.length != b5.length); // should fail
assert(b1.length == b5.length); // should fail
}
}
// ----
// Warning 1218: (330-360): CHC: Error trying to invoke SMT solver.
// Warning 6328: (330-360): CHC: Assertion violation might happen here.
// Warning 1218: (421-451): CHC: Error trying to invoke SMT solver.
// Warning 6328: (421-451): CHC: Assertion violation might happen here.
// Warning 1218: (524-554): CHC: Error trying to invoke SMT solver.
// Warning 6328: (524-554): CHC: Assertion violation might happen here.
// Warning 6328: (573-603): CHC: Assertion violation happens here.
// Warning 4661: (330-360): BMC: Assertion violation happens here.
// Warning 4661: (421-451): BMC: Assertion violation happens here.
// Warning 4661: (524-554): BMC: Assertion violation happens here.

32
test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol Normal file
View File

@ -0,0 +1,32 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeStringLiteral() public pure {
bytes memory b1 = abi.encode("");
bytes memory b2 = abi.encode("");
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b2.length);
bytes memory b3 = abi.encode(bytes(""));
assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encode(bytes24(""));
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b4.length);
bytes memory b5 = abi.encode(string(""));
assert(b1.length == b5.length); // should fail
}
}
// ----
// Warning 1218: (240-270): CHC: Error trying to invoke SMT solver.
// Warning 6328: (240-270): CHC: Assertion violation might happen here.
// Warning 1218: (318-348): CHC: Error trying to invoke SMT solver.
// Warning 6328: (318-348): CHC: Assertion violation might happen here.
// Warning 1218: (485-515): CHC: Error trying to invoke SMT solver.
// Warning 6328: (485-515): CHC: Assertion violation might happen here.
// Warning 1218: (564-594): CHC: Error trying to invoke SMT solver.
// Warning 6328: (564-594): CHC: Assertion violation might happen here.
// Warning 4661: (240-270): BMC: Assertion violation happens here.
// Warning 4661: (318-348): BMC: Assertion violation happens here.
// Warning 4661: (485-515): BMC: Assertion violation happens here.
// Warning 4661: (564-594): BMC: Assertion violation happens here.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol Normal file
View File

@ -0,0 +1,37 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(bytes4 sel, bytes calldata data) external pure {
bytes memory b1 = abi.encodeWithSelector(sel, data);
bytes memory b2 = abi.encodeWithSelector(sel, data[0:]);
// should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately
assert(b1.length == b2.length); // fails for now
bytes memory b3 = abi.encodeWithSelector(sel, data[:data.length]);
// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encodeWithSelector(sel, data[5:10]);
assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encodeWithSelector(sel, data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
bytes memory b6 = abi.encodeWithSelector(0xcafecafe, data[5:10]);
assert(b4.length == b6.length); // should fail
}
}
// ----
// Warning 6328: (357-387): CHC: Assertion violation happens here.
// Warning 6328: (610-640): CHC: Assertion violation happens here.
// Warning 1218: (723-753): CHC: Error trying to invoke SMT solver.
// Warning 6328: (723-753): CHC: Assertion violation might happen here.
// Warning 1218: (991-1021): CHC: Error trying to invoke SMT solver.
// Warning 6328: (991-1021): CHC: Assertion violation might happen here.
// Warning 1218: (1111-1141): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1111-1141): CHC: Assertion violation might happen here.
// Warning 4661: (723-753): BMC: Assertion violation happens here.
// Warning 4661: (991-1021): BMC: Assertion violation happens here.
// Warning 4661: (1111-1141): BMC: Assertion violation happens here.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol Normal file
View File

@ -0,0 +1,37 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(bytes4 sel, uint[] calldata data) external pure {
bytes memory b1 = abi.encodeWithSelector(sel, data);
bytes memory b2 = abi.encodeWithSelector(sel, data[0:]);
// should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately
assert(b1.length == b2.length); // fails for now
bytes memory b3 = abi.encodeWithSelector(sel, data[:data.length]);
// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encodeWithSelector(sel, data[5:10]);
assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encodeWithSelector(sel, data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
bytes memory b6 = abi.encodeWithSelector(0xcafecafe, data[5:10]);
assert(b4.length == b6.length); // should fail
}
}
// ----
// Warning 6328: (358-388): CHC: Assertion violation happens here.
// Warning 6328: (611-641): CHC: Assertion violation happens here.
// Warning 1218: (724-754): CHC: Error trying to invoke SMT solver.
// Warning 6328: (724-754): CHC: Assertion violation might happen here.
// Warning 1218: (992-1022): CHC: Error trying to invoke SMT solver.
// Warning 6328: (992-1022): CHC: Assertion violation might happen here.
// Warning 1218: (1112-1142): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1112-1142): CHC: Assertion violation might happen here.
// Warning 4661: (724-754): BMC: Assertion violation happens here.
// Warning 4661: (992-1022): BMC: Assertion violation happens here.
// Warning 4661: (1112-1142): BMC: Assertion violation happens here.

20
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeHash(bytes4 sel, uint a, uint b) public pure {
require(a == b);
bytes memory b1 = abi.encodeWithSelector(sel, a, a, a, a);
bytes memory b2 = abi.encodeWithSelector(sel, b, a, b, a);
assert(keccak256(b1) == keccak256(b2));
bytes memory b3 = abi.encodeWithSelector(0xcafecafe, a, a, a, a);
assert(keccak256(b1) == keccak256(b3)); // should fail
assert(keccak256(b1) != keccak256(b3)); // should fail
}
}
// ----
// Warning 1218: (365-403): CHC: Error trying to invoke SMT solver.
// Warning 6328: (365-403): CHC: Assertion violation might happen here.
// Warning 1218: (422-460): CHC: Error trying to invoke SMT solver.
// Warning 6328: (422-460): CHC: Assertion violation might happen here.
// Warning 4661: (365-403): BMC: Assertion violation happens here.
// Warning 4661: (422-460): BMC: Assertion violation happens here.

32
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol Normal file
View File

@ -0,0 +1,32 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSimple(bytes4 sel, bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure {
require(x == y);
// Disabled because of Spacer nondeterminism
bytes memory b1 = abi.encodeWithSelector(sel, x, z, a);
//bytes memory b2 = abi.encodeWithSelector(sel, y, z, a);
//assert(b1.length == b2.length);
// Disabled because of Spacer nondeterminism
//bytes memory b3 = abi.encodeWithSelector(sel, y, z, b);
//assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encodeWithSelector(sel, t, z, a);
assert(b1.length == b4.length); // should fail
bytes memory b5 = abi.encodeWithSelector(sel, y, y, y, y, a, a, a);
assert(b1.length != b5.length); // should fail
assert(b1.length == b5.length); // should fail
bytes memory b6 = abi.encodeWithSelector(0xcafecafe, x, z, a);
assert(b1.length == b6.length); // should fail
}
}
// ----
// Warning 5667: (132-147): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (603-633): CHC: Assertion violation happens here.
// Warning 6328: (723-753): CHC: Assertion violation happens here.
// Warning 6328: (772-802): CHC: Assertion violation happens here.
// Warning 1218: (887-917): CHC: Error trying to invoke SMT solver.
// Warning 6328: (887-917): CHC: Assertion violation might happen here.
// Warning 4661: (887-917): BMC: Assertion violation happens here.

36
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol Normal file
View File

@ -0,0 +1,36 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeStringLiteral(bytes4 sel) public pure {
bytes memory b1 = abi.encodeWithSelector(sel, "");
bytes memory b2 = abi.encodeWithSelector(sel, "");
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b2.length);
bytes memory b3 = abi.encodeWithSelector(sel, bytes(""));
assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encodeWithSelector(sel, bytes24(""));
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b4.length);
bytes memory b5 = abi.encodeWithSelector(sel, string(""));
assert(b1.length == b5.length); // should fail
bytes memory b6 = abi.encodeWithSelector(0xcafecafe, bytes24(""));
assert(b4.length == b6.length); // should fail
}
}
// ----
// Warning 6328: (284-314): CHC: Assertion violation happens here.
// Warning 1218: (379-409): CHC: Error trying to invoke SMT solver.
// Warning 6328: (379-409): CHC: Assertion violation might happen here.
// Warning 1218: (563-593): CHC: Error trying to invoke SMT solver.
// Warning 6328: (563-593): CHC: Assertion violation might happen here.
// Warning 1218: (659-689): CHC: Error trying to invoke SMT solver.
// Warning 6328: (659-689): CHC: Assertion violation might happen here.
// Warning 1218: (778-808): CHC: Error trying to invoke SMT solver.
// Warning 6328: (778-808): CHC: Assertion violation might happen here.
// Warning 4661: (379-409): BMC: Assertion violation happens here.
// Warning 4661: (563-593): BMC: Assertion violation happens here.
// Warning 4661: (659-689): BMC: Assertion violation happens here.
// Warning 4661: (778-808): BMC: Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol Normal file
View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C {
function f(string memory sig, uint x, uint[] memory a) public pure {
bytes memory b1 = abi.encodeWithSignature(sig, x, a);
bytes memory b2 = abi.encodeWithSelector(bytes4(keccak256(bytes(sig))), x, a);
// should hold but we do not evaluate keccak256 in an interpreted way
assert(b1.length == b2.length);
}
}
// ----
// Warning 6328: (326-356): CHC: Assertion violation might happen here.
// Warning 7812: (326-356): BMC: Assertion violation might happen here.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol Normal file
View File

@ -0,0 +1,37 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(string memory sig, bytes calldata data) external pure {
bytes memory b1 = abi.encodeWithSignature(sig, data);
bytes memory b2 = abi.encodeWithSignature(sig, data[0:]);
// should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately
assert(b1.length == b2.length); // fails for now
bytes memory b3 = abi.encodeWithSignature(sig, data[:data.length]);
// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encodeWithSignature(sig, data[5:10]);
assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encodeWithSignature(sig, data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
bytes memory b6 = abi.encodeWithSelector("f()", data[5:10]);
assert(b4.length == b6.length); // should fail
}
}
// ----
// Warning 6328: (366-396): CHC: Assertion violation happens here.
// Warning 6328: (620-650): CHC: Assertion violation happens here.
// Warning 1218: (734-764): CHC: Error trying to invoke SMT solver.
// Warning 6328: (734-764): CHC: Assertion violation might happen here.
// Warning 1218: (1003-1033): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1003-1033): CHC: Assertion violation might happen here.
// Warning 1218: (1118-1148): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1118-1148): CHC: Assertion violation might happen here.
// Warning 4661: (734-764): BMC: Assertion violation happens here.
// Warning 4661: (1003-1033): BMC: Assertion violation happens here.
// Warning 4661: (1118-1148): BMC: Assertion violation happens here.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol Normal file
View File

@ -0,0 +1,37 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(string memory sig, uint[] calldata data) external pure {
bytes memory b1 = abi.encodeWithSignature(sig, data);
bytes memory b2 = abi.encodeWithSignature(sig, data[0:]);
// should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately
assert(b1.length == b2.length); // fails for now
bytes memory b3 = abi.encodeWithSignature(sig, data[:data.length]);
// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encodeWithSignature(sig, data[5:10]);
assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encodeWithSignature(sig, data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
bytes memory b6 = abi.encodeWithSelector("f()", data[5:10]);
assert(b4.length == b6.length); // should fail
}
}
// ----
// Warning 6328: (367-397): CHC: Assertion violation happens here.
// Warning 6328: (621-651): CHC: Assertion violation happens here.
// Warning 1218: (735-765): CHC: Error trying to invoke SMT solver.
// Warning 6328: (735-765): CHC: Assertion violation might happen here.
// Warning 1218: (1004-1034): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1004-1034): CHC: Assertion violation might happen here.
// Warning 1218: (1119-1149): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1119-1149): CHC: Assertion violation might happen here.
// Warning 4661: (735-765): BMC: Assertion violation happens here.
// Warning 4661: (1004-1034): BMC: Assertion violation happens here.
// Warning 4661: (1119-1149): BMC: Assertion violation happens here.

20
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol Normal file
View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeHash(string memory sig, uint a, uint b) public pure {
require(a == b);
bytes memory b1 = abi.encodeWithSignature(sig, a, a, a, a);
bytes memory b2 = abi.encodeWithSignature(sig, b, a, b, a);
assert(keccak256(b1) == keccak256(b2));
bytes memory b3 = abi.encodeWithSelector("f()", a, a, a, a);
assert(keccak256(b1) == keccak256(b3)); // should fail
assert(keccak256(b1) != keccak256(b3)); // should fail
}
}
// ----
// Warning 1218: (369-407): CHC: Error trying to invoke SMT solver.
// Warning 6328: (369-407): CHC: Assertion violation might happen here.
// Warning 1218: (426-464): CHC: Error trying to invoke SMT solver.
// Warning 6328: (426-464): CHC: Assertion violation might happen here.
// Warning 4661: (369-407): BMC: Assertion violation happens here.
// Warning 4661: (426-464): BMC: Assertion violation happens here.

34
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol Normal file
View File

@ -0,0 +1,34 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSimple(string memory sig, bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure {
require(x == y);
bytes memory b1 = abi.encodeWithSignature(sig, x, z, a);
bytes memory b2 = abi.encodeWithSignature(sig, y, z, a);
assert(b1.length == b2.length);
bytes memory b3 = abi.encodeWithSignature(sig, y, z, b);
assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encodeWithSignature(sig, t, z, a);
assert(b1.length == b4.length); // should fail
bytes memory b5 = abi.encodeWithSignature(sig, y, y, y, y, a, a, a);
assert(b1.length != b5.length); // should fail
assert(b1.length == b5.length); // should fail
bytes memory b6 = abi.encodeWithSignature("f()", x, z, a);
assert(b1.length == b6.length); // should fail
}
}
// ----
// Warning 6328: (403-433): CHC: Assertion violation happens here.
// Warning 6328: (512-542): CHC: Assertion violation happens here.
// Warning 1218: (633-663): CHC: Error trying to invoke SMT solver.
// Warning 6328: (633-663): CHC: Assertion violation might happen here.
// Warning 1218: (682-712): CHC: Error trying to invoke SMT solver.
// Warning 6328: (682-712): CHC: Assertion violation might happen here.
// Warning 1218: (793-823): CHC: Error trying to invoke SMT solver.
// Warning 6328: (793-823): CHC: Assertion violation might happen here.
// Warning 4661: (633-663): BMC: Assertion violation happens here.
// Warning 4661: (682-712): BMC: Assertion violation happens here.
// Warning 4661: (793-823): BMC: Assertion violation happens here.

36
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol Normal file
View File

@ -0,0 +1,36 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeStringLiteral(string memory sig) public pure {
bytes memory b1 = abi.encodeWithSignature(sig, "");
bytes memory b2 = abi.encodeWithSignature(sig, "");
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b2.length);
bytes memory b3 = abi.encodeWithSignature(sig, bytes(""));
assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encodeWithSignature(sig, bytes24(""));
// should hold, but currently fails due to string literal abstraction
assert(b1.length == b4.length);
bytes memory b5 = abi.encodeWithSignature(sig, string(""));
assert(b1.length == b5.length); // should fail
bytes memory b6 = abi.encodeWithSelector("f()", bytes24(""));
assert(b4.length == b6.length); // should fail
}
}
// ----
// Warning 6328: (293-323): CHC: Assertion violation happens here.
// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver.
// Warning 6328: (389-419): CHC: Assertion violation might happen here.
// Warning 1218: (574-604): CHC: Error trying to invoke SMT solver.
// Warning 6328: (574-604): CHC: Assertion violation might happen here.
// Warning 1218: (671-701): CHC: Error trying to invoke SMT solver.
// Warning 6328: (671-701): CHC: Assertion violation might happen here.
// Warning 1218: (785-815): CHC: Error trying to invoke SMT solver.
// Warning 6328: (785-815): CHC: Assertion violation might happen here.
// Warning 4661: (389-419): BMC: Assertion violation happens here.
// Warning 4661: (574-604): BMC: Assertion violation happens here.
// Warning 4661: (671-701): BMC: Assertion violation happens here.
// Warning 4661: (785-815): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
View File

@ -12,4 +12,4 @@ contract C {
}
}
// ----
// Warning 6328: (167-188): CHC: Assertion violation happens here.\nCounterexample:\na = [[17, 12, 12, 12, 12], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15]]\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()
// Warning 6328: (167-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf()

4
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol
View File

File diff suppressed because one or more lines are too long

2
test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
View File

@ -10,4 +10,4 @@ contract C {
}
}
// ----
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2437\n\n\nTransaction trace:\nconstructor()\nf(2437)
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\n\nTransaction trace:\nconstructor()\nf(21238)

4
test/libsolidity/smtCheckerTests/complex/MerkleProof.sol
View File

@ -34,7 +34,3 @@ library MerkleProof {
}
// ----
// Warning 4588: (988-1032): Assertion checker does not yet implement this type of function call.
// Warning 4588: (1175-1219): Assertion checker does not yet implement this type of function call.
// Warning 4588: (988-1032): Assertion checker does not yet implement this type of function call.
// Warning 4588: (1175-1219): Assertion checker does not yet implement this type of function call.

8
test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
View File

@ -83,6 +83,10 @@ contract InternalCall {
// Warning 2018: (1144-1206): Function state mutability can be restricted to pure
// Warning 2018: (1212-1274): Function state mutability can be restricted to pure
// Warning 2018: (1280-1342): Function state mutability can be restricted to pure
// Warning 4588: (771-814): Assertion checker does not yet implement this type of function call.
// Warning 4588: (771-814): Assertion checker does not yet implement this type of function call.
// Warning 4588: (714-749): Assertion checker does not yet implement this type of function call.
// Warning 4588: (760-815): Assertion checker does not yet implement this type of function call.
// Warning 4588: (887-919): Assertion checker does not yet implement this type of function call.
// Warning 4588: (714-749): Assertion checker does not yet implement this type of function call.
// Warning 4588: (760-815): Assertion checker does not yet implement this type of function call.
// Warning 4588: (887-919): Assertion checker does not yet implement this type of function call.
// Warning 5729: (1403-1408): BMC does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol
View File

@ -25,4 +25,4 @@ contract D is C {
}
}
// ----
// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\na = 0\n\n\nTransaction trace:\nconstructor(0)
// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 1\n\n\nTransaction trace:\nconstructor(1)

2
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol
View File

@ -26,6 +26,6 @@ contract C is B {
}
// ----
// Warning 5740: (152-157): Unreachable code.
// Warning 6328: (310-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 1\n\n\nTransaction trace:\nconstructor(1)
// Warning 6328: (310-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 0\n\n\nTransaction trace:\nconstructor(0)
// Warning 6328: (343-357): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 1\n\n\nTransaction trace:\nconstructor(1)
// Warning 6328: (376-390): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 0\n\n\nTransaction trace:\nconstructor(0)

8
test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol
View File

@ -10,7 +10,9 @@ contract C {
assert(r == k);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (183-197): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [7, 7]\n\n\nTransaction trace:\nconstructor()\nf([7, 7])
// Warning 6328: (201-215): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [9, 9]\n\n\nTransaction trace:\nconstructor()\nf([9, 9])
// Warning 6328: (219-233): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [7, 7]\n\n\nTransaction trace:\nconstructor()\nf([7, 7])
// Warning 6328: (183-197): CHC: Assertion violation happens here.
// Warning 6328: (201-215): CHC: Assertion violation happens here.
// Warning 6328: (219-233): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol
View File

@ -11,4 +11,4 @@ contract C {
}
}
// ----
// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]\n\n\nTransaction trace:\nconstructor()\nf([7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7])
// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf(data)

4
test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
View File

@ -17,7 +17,9 @@ contract C {
assert(x < 10);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (146-149): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\ninc()\nState: x = 2, d = 0\nf()
// Warning 6328: (189-203): CHC: Assertion violation happens here.
// Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

4
test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol
View File

@ -5,7 +5,3 @@ contract C {
}
}
// ----
// Warning 4588: (162-176): Assertion checker does not yet implement this type of function call.
// Warning 4588: (178-203): Assertion checker does not yet implement this type of function call.
// Warning 4588: (162-176): Assertion checker does not yet implement this type of function call.
// Warning 4588: (178-203): Assertion checker does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
View File

@ -18,6 +18,6 @@ contract A is B {
}
}
// ----
// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (207-212): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)

6
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol
View File

@ -24,7 +24,9 @@ contract A is B2, B1 {
assert(a == x + 1);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639934)
// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (314-319): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (302-320): CHC: Assertion violation happens here.\nCounterexample:\na = 0\nx = 0\n\n\nTransaction trace:\nconstructor(0)
// Warning 6328: (302-320): CHC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
View File

@ -26,8 +26,10 @@ contract A is B2, B1 {
assert(b1 != b2);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nb1 = 0, a = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nx = 1\n\n\nTransaction trace:\nconstructor(1)
// Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nb2 = 0, a = 1\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nb2 = 0, a = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639934)
// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (334-350): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
View File

@ -13,4 +13,4 @@ contract C {
}
}
// ----
// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11)
// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(9)

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol
View File

@ -15,4 +15,4 @@ contract C is B {
}
}
// ----
// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(9)
// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11)

4
test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
View File

@ -13,5 +13,5 @@ contract C {
}
}
// ----
// Warning 6328: (162-176): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\ny = 0\n\n\nTransaction trace:\nconstructor(1, 0)\nState: x = 1\nf(0)
// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 5\na = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 6328: (162-176): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 1\n\n\nTransaction trace:\nconstructor(0, 0)\nState: x = 0\nf(1)
// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 5\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nb = 1\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1)

2
test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
View File

@ -17,4 +17,4 @@ contract C {
}
}
// ----
// Warning 6328: (293-307): CHC: Assertion violation happens here.
// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()

4
test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol
View File

@ -20,5 +20,7 @@ contract C {
assert(y == 1); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (387-401): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol
View File

@ -32,5 +32,5 @@ contract C is Z(5) {
}
}
// ----
// Warning 4984: (325-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 1\nz = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (325-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (400-413): CHC: Assertion violation happens here.\nCounterexample:\nx = 6\n\n\n\nTransaction trace:\nconstructor()

6
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol
View File

@ -32,7 +32,9 @@ contract C is Z(5) {
assert(x > 90); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (143-149): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 9\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639927\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639927)
// Warning 4984: (143-149): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (333-340): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (409-423): CHC: Assertion violation happens here.\nCounterexample:\nx = 15\n\n\n\nTransaction trace:\nconstructor()
// Warning 6328: (409-423): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol
View File

@ -34,6 +34,8 @@ contract C is Z, B {
assert(x == k); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (456-470): CHC: Assertion violation happens here.

9
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
View File

@ -11,14 +11,15 @@ contract LoopFor2 {
}
// Removed because current Spacer seg faults in cex generation.
//assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
// Removed because current Spacer seg faults in cex generation.
//assert(a[0] == 900);
// Removed because current Spacer seg faults in cex generation.
//assert(b[0] == 900);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 2072: (156-171): Unused local variable.
// Warning 4984: (252-257): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (232-238): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (373-392): CHC: Assertion violation happens here.
// Warning 6328: (396-415): CHC: Assertion violation happens here.

10
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
View File

@ -4,6 +4,9 @@ contract LoopFor2 {
uint[] b;
uint[] c;
// Disabled because of Spancer nondeterminism in the overflow queries
// which can't be disabled separately.
/*
function testUnboundedForLoop(uint n) public {
b[0] = 900;
uint[] storage a = b;
@ -17,9 +20,8 @@ contract LoopFor2 {
assert(a[0] == 900);
assert(b[0] == 900);
}
*/
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (237-242): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (217-223): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (341-360): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1)
// Warning 6328: (364-383): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1)

9
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
View File

@ -13,15 +13,16 @@ contract LoopFor2 {
}
// Removed because current Spacer seg faults in cex generation.
//assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
// Removed because current Spacer seg faults in cex generation.
//assert(a[0] == 900);
// Removed because current Spacer seg faults in cex generation.
//assert(b[0] == 900);
}
}
// ====
// SMTIgnoreCex: yes
// SMTSolvers: z3
// ----
// Warning 2072: (156-171): Unused local variable.
// Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (270-273): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (373-392): CHC: Assertion violation happens here.
// Warning 6328: (396-415): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol
View File

@ -30,4 +30,4 @@ contract C
}
// ----
// Warning 6328: (329-344): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 10\nb = false\nc = true\n\n\nTransaction trace:\nconstructor()\nf(0, 9, false, true)
// Warning 6328: (380-395): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 20\nb = false\nc = false\n\n\nTransaction trace:\nconstructor()\nf(0, 0, false, false)
// Warning 6328: (380-395): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\n\nTransaction trace:\nconstructor()\nf(9, 0, true, false)

4
test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol
View File

@ -11,5 +11,7 @@ contract C
assert(array[p] < 90);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (191-212): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 90\np = 0\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(90, 0)
// Warning 6328: (191-212): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol
View File

@ -11,5 +11,7 @@ contract C
assert(map[p] < 90);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (197-216): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 99\np = 0\n\n\nTransaction trace:\nconstructor()\nf(99, 0)
// Warning 6328: (197-216): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/operators/slice.sol
View File

@ -4,7 +4,8 @@ contract C {
function f(bytes calldata b) external pure {
require(b[10] == 0xff);
assert(bytes(b[10:20]).length == 10);
assert(bytes(b[10:20])[0] == 0xff);
// Disabled because of Spacer nondeterminism
//assert(bytes(b[10:20])[0] == 0xff);
// Disabled because of Spacer nondeterminism
//assert(bytes(b[10:20])[5] == 0xff);
}

2
test/libsolidity/smtCheckerTests/operators/unary_add_array.sol
View File

@ -15,4 +15,4 @@ contract C
}
}
// ----
// Warning 6328: (240-253): CHC: Assertion violation happens here.
// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 0\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(0)

4
test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol
View File

@ -14,5 +14,7 @@ contract C
assert(b > 4);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (244-257): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 6328: (244-257): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol
View File

@ -7,4 +7,4 @@ contract C {
}
}
// ----
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\n\nTransaction trace:\nconstructor()\nf(x, 23158417847463239084714197001737581570653996933128112807891516801582625927988)
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = [19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 22, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19]\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\n\nTransaction trace:\nconstructor()\nf([19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 22, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19], 23158417847463239084714197001737581570653996933128112807891516801582625927988)

2
test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
View File

@ -7,4 +7,4 @@ contract C {
}
// ----
// Warning 4281: (110-115): CHC: Division by zero happens here.\nCounterexample:\n\nx = 0\ny = 0\n = 0\n\nTransaction trace:\nconstructor()\nf(0, 0)
// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nconstructor()\nf((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1))

2
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol
View File

@ -11,8 +11,6 @@ contract C {
// Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call.
// Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory)
// Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer)
// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call.

16
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol
View File

@ -2,18 +2,12 @@ pragma experimental SMTChecker;
pragma experimental "ABIEncoderV2";
contract C {
function f() public pure {
(uint x1, bool b1) = abi.decode("abc", (uint, bool));
(uint x2, bool b2) = abi.decode("abc", (uint, bool));
// False positive until abi.* are implemented as uninterpreted functions.
function f(bytes memory data) public pure {
(uint x1, bool b1) = abi.decode(data, (uint, bool));
(uint x2, bool b2) = abi.decode(data, (uint, bool));
assert(x1 == x2);
}
}
// ----
// Warning 2072: (122-129): Unused local variable.
// Warning 2072: (178-185): Unused local variable.
// Warning 4588: (133-164): Assertion checker does not yet implement this type of function call.
// Warning 4588: (189-220): Assertion checker does not yet implement this type of function call.
// Warning 6328: (300-316): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 4588: (133-164): Assertion checker does not yet implement this type of function call.
// Warning 4588: (189-220): Assertion checker does not yet implement this type of function call.
// Warning 2072: (139-146): Unused local variable.
// Warning 2072: (194-201): Unused local variable.

30
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
View File

@ -1,25 +1,19 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
(uint a1, bytes32 b1, C c1) = abi.decode("abc", (uint, bytes32, C));
(uint a2, bytes32 b2, C c2) = abi.decode("abc", (uint, bytes32, C));
// False positive until abi.* are implemented as uninterpreted functions.
function f(bytes memory data) public pure {
(uint a1, bytes32 b1, C c1) = abi.decode(data, (uint, bytes32, C));
(uint a2, bytes32 b2, C c2) = abi.decode(data, (uint, bytes32, C));
assert(a1 == a2);
assert(a1 != a2);
}
}
// ----
// Warning 2072: (85-95): Unused local variable.
// Warning 2072: (97-101): Unused local variable.
// Warning 2072: (156-166): Unused local variable.
// Warning 2072: (168-172): Unused local variable.
// Warning 8364: (139-140): Assertion checker does not yet implement type type(contract C)
// Warning 4588: (105-142): Assertion checker does not yet implement this type of function call.
// Warning 8364: (210-211): Assertion checker does not yet implement type type(contract C)
// Warning 4588: (176-213): Assertion checker does not yet implement this type of function call.
// Warning 6328: (293-309): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (313-329): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 8364: (139-140): Assertion checker does not yet implement type type(contract C)
// Warning 4588: (105-142): Assertion checker does not yet implement this type of function call.
// Warning 8364: (210-211): Assertion checker does not yet implement type type(contract C)
// Warning 4588: (176-213): Assertion checker does not yet implement this type of function call.
// Warning 2072: (102-112): Unused local variable.
// Warning 2072: (114-118): Unused local variable.
// Warning 2072: (172-182): Unused local variable.
// Warning 2072: (184-188): Unused local variable.
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17]\n\n\nTransaction trace:\nconstructor()\nf([17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17])
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)

2
test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol
View File

@ -5,5 +5,3 @@ contract C {
}
}
// ----
// Warning 4588: (126-154): Assertion checker does not yet implement this type of function call.
// Warning 4588: (126-154): Assertion checker does not yet implement this type of function call.

6
test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol
View File

@ -16,6 +16,8 @@ contract C {
assert(gleft == gasleft());
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (124-150): CHC: Assertion violation happens here.\nCounterexample:\ngleft = 1\n\n\n\nTransaction trace:\nconstructor()\nState: gleft = 0\nf()
// Warning 6328: (219-245): CHC: Assertion violation happens here.\nCounterexample:\ngleft = 1\n\n\n\nTransaction trace:\nconstructor()\nState: gleft = 0\nf()
// Warning 6328: (124-150): CHC: Assertion violation happens here.
// Warning 6328: (219-245): CHC: Assertion violation happens here.

10
test/libsolidity/smtCheckerTests/types/address_call.sol
View File

@ -19,7 +19,9 @@ contract C
// EVMVersion: >spuriousDragon
// ----
// Warning 2072: (224-240): Unused local variable.
// Warning 6328: (260-275): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [])
// Warning 6328: (279-293): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [])
// Warning 6328: (297-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [])
// Warning 6328: (320-344): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [])
// Warning 4588: (244-256): Assertion checker does not yet implement this type of function call.
// Warning 6328: (260-275): CHC: Assertion violation happens here.
// Warning 6328: (279-293): CHC: Assertion violation happens here.
// Warning 6328: (297-316): CHC: Assertion violation happens here.
// Warning 6328: (320-344): CHC: Assertion violation happens here.
// Warning 4588: (244-256): Assertion checker does not yet implement this type of function call.

10
test/libsolidity/smtCheckerTests/types/address_delegatecall.sol
View File

@ -19,7 +19,9 @@ contract C
// EVMVersion: >spuriousDragon
// ----
// Warning 2072: (224-240): Unused local variable.
// Warning 6328: (268-283): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [])
// Warning 6328: (287-301): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [])
// Warning 6328: (305-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [])
// Warning 6328: (328-352): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [])
// Warning 4588: (244-264): Assertion checker does not yet implement this type of function call.
// Warning 6328: (268-283): CHC: Assertion violation happens here.
// Warning 6328: (287-301): CHC: Assertion violation happens here.
// Warning 6328: (305-324): CHC: Assertion violation happens here.
// Warning 6328: (328-352): CHC: Assertion violation happens here.
// Warning 4588: (244-264): Assertion checker does not yet implement this type of function call.

2
test/libsolidity/smtCheckerTests/types/address_staticcall.sol
View File

@ -19,4 +19,4 @@ contract C
// EVMVersion: >spuriousDragon
// ----
// Warning 2072: (224-240): Unused local variable.
// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [10, 10]\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [10, 10])
// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 18, 5, 21, 5, 5, 5, 5, 5, 5, 5, 5, 5, 31, 5, 5, 5, 5, 5, 5, 5, 5]\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 18, 5, 21, 5, 5, 5, 5, 5, 5, 5, 5, 5, 31, 5, 5, 5, 5, 5, 5, 5, 5])

2
test/libsolidity/smtCheckerTests/types/address_transfer_2.sol
View File

@ -14,6 +14,6 @@ contract C
}
}
// ----
// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7720\nb = 7719\n\n\nTransaction trace:\nconstructor()\nf(100, 7720, 7719)
// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7719\nb = 7720\n\n\nTransaction trace:\nconstructor()\nf(100, 7719, 7720)
// Warning 1236: (217-232): BMC: Insufficient funds happens here.
// Warning 1236: (236-251): BMC: Insufficient funds happens here.

2
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol
View File

@ -20,4 +20,4 @@ contract C
}
}
// ----
// Warning 6328: (436-453): CHC: Assertion violation happens here.\nCounterexample:\narray2d = []\nx = 0\ny = 0\nc = [38, 8, 8, 8, 8, 8, 8, 8, 8]\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\ng(0, 0, [38, 8, 8, 8, 8, 8, 8, 8, 8])
// Warning 6328: (436-453): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\ng(0, 0, c)

6
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol
View File

@ -18,6 +18,8 @@ contract C
f(array2d[x], array2d[y]);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (225-242): CHC: Assertion violation happens here.\nCounterexample:\narray = [1, 19, 19, 19, 19], array2d = []\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: array = [], array2d = []\ng(0, 0)
// Warning 6328: (289-307): CHC: Assertion violation happens here.\nCounterexample:\narray = [1, 19, 19, 19, 19], array2d = []\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: array = [], array2d = []\ng(0, 0)
// Warning 6328: (225-242): CHC: Assertion violation happens here.
// Warning 6328: (289-307): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
View File

@ -27,4 +27,4 @@ contract C
}
}
// ----
// Warning 6328: (572-589): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 20, 20, 20, 20], d = [], array2d = []\nx = 0\nc = [0, 9, 9, 9, 9, 9, 9, 9, 9, 9]\n\n\nTransaction trace:\nconstructor()\nState: b = [], d = [], array2d = []\ng(0, [0, 9, 9, 9, 9, 9, 9, 9, 9, 9])
// Warning 6328: (572-589): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
View File

@ -11,4 +11,4 @@ contract C
}
// ----
// Warning 2018: (47-148): Function state mutability can be restricted to pure
// Warning 6328: (128-144): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 5, 5, 5, 5, 5]\n\n\nTransaction trace:\nconstructor()\nf(false, [38, 5, 5, 5, 5, 5])
// Warning 6328: (128-144): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]\n\n\nTransaction trace:\nconstructor()\nf(false, [7719, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14])

2
test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol
View File

@ -9,4 +9,4 @@ contract C
}
}
// ----
// Warning 6328: (148-170): CHC: Assertion violation happens here.\nCounterexample:\n\narray = [15, 15, 15, 15, 15]\nx = 38\ny = 38\n\n\nTransaction trace:\nconstructor()\nf([15, 15, 15, 15, 15], 38, 38)
// Warning 6328: (148-170): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 38\n\n\nTransaction trace:\nconstructor()\nf(array, 38, 38)

2
test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol
View File

@ -24,4 +24,4 @@ contract C
}
}
// ----
// Warning 6328: (421-452): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\ng(38)
// Warning 6328: (421-452): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8855\n\n\nTransaction trace:\nconstructor()\ng(8855)

4
test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol
View File

@ -12,7 +12,8 @@ contract C
// erase knowledge about memory references.
assert(c[0] == 42);
// Fails because b1 == a is possible.
assert(a[0] == 2);
// Disabled because Spacer seg faults.
//assert(a[0] == 2);
assert(b1[0] == 1);
}
function g(bool x, uint[2] memory c) public {
@ -23,4 +24,3 @@ contract C
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (338-355): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol
View File

@ -24,4 +24,4 @@ contract C
}
}
// ----
// Warning 6328: (425-456): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\ng(38)
// Warning 6328: (425-456): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8855\n\n\nTransaction trace:\nconstructor()\ng(8855)

2
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
View File

@ -27,4 +27,4 @@ contract C
}
}
// ----
// Warning 6328: (830-850): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\n\nTransaction trace:\nconstructor()\ng(0)
// Warning 6328: (830-850): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol
View File

@ -8,4 +8,4 @@ contract C
}
}
// ----
// Warning 6328: (119-141): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [28958, 28957, 28958, 28958, 28958]\nb2 = [28958, 28957, 28958, 28958, 28958]\n\n\nTransaction trace:\nconstructor()\nf([], [28958, 28957, 28958, 28958, 28958])
// Warning 6328: (119-141): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf(b1, b2)

4
test/libsolidity/smtCheckerTests/types/contract.sol
View File

@ -6,5 +6,7 @@ contract C
assert(c == d);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (84-98): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\nd = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 1)
// Warning 6328: (84-98): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/types/contract_2.sol
View File

@ -11,5 +11,7 @@ contract C
assert(c == d);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (109-123): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\nd = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 1)
// Warning 6328: (109-123): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
View File

@ -6,4 +6,4 @@ contract C {
}
}
// ----
// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\nx = [7, 7]\ny = 0\n\n\nTransaction trace:\nconstructor()\nf([7, 7], 0)
// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\nx = [17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17]\ny = 0\n\n\nTransaction trace:\nconstructor()\nf([17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17], 0)

6
test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol
View File

@ -30,6 +30,8 @@ contract C
f(maps[x], maps[y]);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (397-417): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\ng(true, 0, 0)
// Warning 6328: (463-481): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\ng(true, 0, 0)
// Warning 6328: (397-417): CHC: Assertion violation happens here.
// Warning 6328: (463-481): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol
View File

@ -12,4 +12,4 @@ contract c {
}
}
// ----
// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7719\nb = 38\n\n\nTransaction trace:\nconstructor()\ng(7719, 38)
// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21239\n\n\nTransaction trace:\nconstructor()\ng(38, 21239)

2
test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol
View File

@ -10,5 +10,5 @@ contract C {
}
}
// ----
// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0\n\n\nTransaction trace:\nconstructor()\nf(0)
// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293569\n\n\nTransaction trace:\nconstructor()\nf(52647538817385212172903286807934654968315727694643370704309751478220717293569)
// Warning 6328: (170-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538830022687173130149211684818290356179572910782152375644828738034597888\n\n\nTransaction trace:\nconstructor()\nf(52647538830022687173130149211684818290356179572910782152375644828738034597888)

6
test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol
View File

@ -17,6 +17,8 @@ contract C {
s.a.pop();
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 2529: (133-142): CHC: Empty array "pop" happens here.\nCounterexample:\ns = {x: 38, a: []}\n_x = 38\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(38)
// Warning 6328: (189-213): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 115792089237316195423570985008687907853269984665640564039457584007913129639897, a: [115792089237316195423570985008687907853269984665640564039457584007913129639897, 0]}\n_x = 115792089237316195423570985008687907853269984665640564039457584007913129639897\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(115792089237316195423570985008687907853269984665640564039457584007913129639897)
// Warning 2529: (133-142): CHC: Empty array "pop" happens here.
// Warning 6328: (189-213): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/types/tuple_assignment_array_empty.sol
View File

@ -10,5 +10,7 @@ contract C
assert(a[y] == 4);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (136-153): CHC: Assertion violation happens here.\nCounterexample:\na = []\nx = 39\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: a = []\ng(39, 0)
// Warning 6328: (136-153): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol
View File

@ -11,3 +11,5 @@ contract C {
}
}
// ----
// Warning 4588: (142-161): Assertion checker does not yet implement this type of function call.
// Warning 4588: (142-161): Assertion checker does not yet implement this type of function call.