You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
On the following file, SMTChecker generates invalid SMT-LIB2 script if run with the options --model-checker-engine all --model-checker-solvers smtlib2 --model-checker-print-query --model-checker-ext-calls trusted.
contract D {
function zero() public view returns (uint) {
return 0;
}
}
contract C {
uint x;
function f(D d) public view {
uint res = d.zero();
assert(x < 1000);
}
function inc() public {
++x;
}
}
The problem with the script is with the state_type data type. It is declared with three members, but then applied to a single field in the body of the query.
The text was updated successfully, but these errors were encountered:
The problem seems to be with the symbolic variable for the blockchain state, which has different type in CHC engine and in BMC engine, if trusted mode is used to analyze external calls.
On the following file, SMTChecker generates invalid SMT-LIB2 script if run with the options
--model-checker-engine all --model-checker-solvers smtlib2 --model-checker-print-query --model-checker-ext-calls trusted
.This is the generated SMT-LIB script:
The problem with the script is with the
state_type
data type. It is declared with three members, but then applied to a single field in the body of the query.The text was updated successfully, but these errors were encountered: