cerc-io/solidity
10
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

change SMTChecker default settings

Browse Source
This commit is contained in:
Leo Alt 2023-03-16 13:11:33 +01:00
parent 02a07fdf46
commit e698a22ca3
32 changed files with 66 additions and 583 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
docs/smtchecker.rst
View File

@ -22,8 +22,7 @@ specification given by ``require`` and ``assert`` statements. That is, it consid
``require`` statements as assumptions and tries to prove that the conditions
inside ``assert`` statements are always true. If an assertion failure is
found, a counterexample may be given to the user showing how the assertion can
be violated. If no warning is given by the SMTChecker for a property,
it means that the property is safe.
be violated. Safe properties are also reported accordingly.
The other verification targets that the SMTChecker checks at compile time are:
@ -34,16 +33,27 @@ The other verification targets that the SMTChecker checks at compile time are:
- Out of bounds index access.
- Insufficient funds for a transfer.
All the targets above are automatically checked by default if all engines are
enabled, except underflow and overflow for Solidity >=0.8.7.
By default, for Solidity >=0.8.20 only assertions are checked. For Solidity
>=0.8.7 all the targets above are checked by default except for underflow and
overflow. Underflow and overflow are also in the default set for Solidity
<0.8.7. The above only applies for the default targets which can be
overridden by the users' choices.
The potential warnings that the SMTChecker reports are:
- ``<failing property> happens here.``. This means that the SMTChecker proved that a certain property fails. A counterexample may be given, however in complex situations it may also not show a counterexample. This result may also be a false positive in certain cases, when the SMT encoding adds abstractions for Solidity code that is either hard or impossible to express.
- ``X verification condition(s) could not be proved.``. This is a summary of how many properties the SMTChecker was not able to prove. The list can be expanded where the warning below is shown for each of those properties.
- ``<failing property> might happen here``. This means that the solver could not prove either case within the given timeout. Since the result is unknown, the SMTChecker reports the potential failure for soundness. This may be solved by increasing the query timeout, but the problem might also simply be too hard for the engine to solve.
The potential information messages that the SMTChecker reports are:
- ``X verification condition(s) proved safe!``. This is a summary of how many properties the SMTChecker was able to prove. The list can be expanded where the information below is shown for each proved property.
- ``<property> check is safe!``. This means that the SMTChecker managed to prove that the property is safe.
- ``Contract invariant(s)``. This may be shown if the model checker ``invariants`` option is chosen with ``contract`` and the SMTChecker was able to infer contract invariants.
- ``Reentrancy property(ies)``. This may be shown if the model checker ``invariants`` option is chosen with ``reentrancy`` and the SMTChecker was able to infer reentrancy properties for external calls.
To enable the SMTChecker, you must select :ref:`which engine should run<smtchecker_engines>`,
where the default is no engine. Selecting the engine enables the SMTChecker on all files.
where the compiler default is no engine. Selecting the engine enables the SMTChecker on all files.
.. note::
@ -442,16 +452,15 @@ SMTChecker Options and Tuning
Timeout
=======
The SMTChecker uses a hardcoded resource limit (``rlimit``) chosen per solver,
which is not precisely related to time. We chose the ``rlimit`` option as the default
because it gives more determinism guarantees than time inside the solver.
This options translates roughly to "a few seconds timeout" per query. Of course many properties
are very complex and need a lot of time to be solved, where determinism does not matter.
If the SMTChecker does not manage to solve the contract properties with the default ``rlimit``,
a timeout can be given in milliseconds via the CLI option ``--model-checker-timeout <time>`` or
By default the SMTChecker uses a timeout of 1 second per query.
If the SMTChecker does not manage to solve the contract properties with the default timeout,
the user may modify the timeout duration (given in milliseconds) via the CLI option ``--model-checker-timeout <time>`` or
the JSON option ``settings.modelChecker.timeout=<time>``, where 0 means no timeout.
Note that some SMT/CHC solvers do not consider counterexample generation as
part of the solving timeout, so one may experience longer times for properties
that are false.
.. _smtchecker_targets:
Verification Targets
@ -478,6 +487,7 @@ The keywords that represent the targets are:
A common subset of targets might be, for example:
``--model-checker-targets assert,overflow``.
Only assertions are checked by default for Solidity >=0.8.20.
All targets are checked by default, except underflow and overflow for Solidity >=0.8.7.
There is no precise heuristic on how and when to split verification targets,

11
libsolidity/formal/ModelCheckerSettings.cpp
View File

@ -85,16 +85,11 @@ map<TargetType, string> const ModelCheckerTargets::targetTypeToString{
std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets)
{
set<TargetType> chosenTargets;
if (_targets == "default" || _targets == "all")
{
bool all = _targets == "all";
if (_targets == "all")
for (auto&& v: targetStrings | ranges::views::values)
{
if (!all && (v == TargetType::Underflow || v == TargetType::Overflow))
continue;
chosenTargets.insert(v);
}
}
else if (_targets == "default")
chosenTargets.insert(TargetType::Assert);
else
for (auto&& t: _targets | ranges::views::split(',') | ranges::to<vector<string>>())
{

9
libsolidity/formal/ModelCheckerSettings.h
View File

@ -117,7 +117,7 @@ enum class VerificationTargetType { ConstantCondition, Underflow, Overflow, Unde
struct ModelCheckerTargets
{
/// Adds the default targets, that is, all except underflow and overflow.
/// By default adds only assertions as targets.
static ModelCheckerTargets Default() { return *fromString("default"); }
/// Adds all targets, including underflow and overflow.
static ModelCheckerTargets All() { return *fromString("all"); }
@ -164,7 +164,7 @@ struct ModelCheckerSettings
/// This is the default because Spacer prefers that over precise / and mod.
/// This option allows disabling this mechanism since other solvers
/// might prefer the precise encoding.
bool divModNoSlacks = false;
std::optional<bool> divModNoSlacks = {};
ModelCheckerEngine engine = ModelCheckerEngine::None();
ModelCheckerExtCalls externalCalls = {};
ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
@ -173,7 +173,10 @@ struct ModelCheckerSettings
bool showUnsupported = false;
smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::Z3();
ModelCheckerTargets targets = ModelCheckerTargets::Default();
std::optional<unsigned> timeout;
// Default timeout per query in milliseconds.
// We keep it as optional because tests may overwrite this to use
// resource limit for reproducibility.
std::optional<unsigned> timeout = 1000;
bool operator!=(ModelCheckerSettings const& _other) const noexcept { return !(*this == _other); }
bool operator==(ModelCheckerSettings const& _other) const noexcept

2
libsolidity/formal/SMTEncoder.cpp
View File

@ -2041,7 +2041,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
IntegerType const& _type
)
{
if (m_settings.divModNoSlacks)
if (m_settings.divModNoSlacks.has_value() && *m_settings.divModNoSlacks)
return {_left / _right, _left % _right};
IntegerType const* intType = &_type;

9
libsolidity/interface/CompilerStack.cpp
View File

@ -600,6 +600,15 @@ bool CompilerStack::analyze()
if (m_modelCheckerSettings.engine.any())
m_modelCheckerSettings.solvers = ModelChecker::checkRequestedSolvers(m_modelCheckerSettings.solvers, m_errorReporter);
// Tiny automatic optimization for Eldarica if the user
// has not forcefully chosen `divModNoSlacks = false` which
// is the default for Spacer but worse for Eldarica.
if (
m_modelCheckerSettings.solvers.eld &&
!m_modelCheckerSettings.divModNoSlacks.has_value()
)
m_modelCheckerSettings.divModNoSlacks = true;
ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile);
modelChecker.checkRequestedSourcesAndContracts(allSources);
for (Source const* source: m_sourceOrder)

2
test/cmdlineTests/model_checker_divModSlacks_default_all/args
View File

@ -1 +1 @@
--model-checker-engine all
--model-checker-engine all --model-checker-targets divByZero

2
test/cmdlineTests/model_checker_divModSlacks_default_bmc/args
View File

@ -1 +1 @@
--model-checker-engine bmc
--model-checker-engine bmc --model-checker-targets divByZero

2
test/cmdlineTests/model_checker_divModSlacks_default_chc/args
View File

@ -1 +1 @@
--model-checker-engine chc
--model-checker-engine chc --model-checker-targets divByZero

2
test/cmdlineTests/model_checker_divModSlacks_false_all/args
View File

@ -1 +1 @@
--model-checker-engine all --model-checker-div-mod-no-slacks
--model-checker-engine all --model-checker-div-mod-no-slacks --model-checker-targets divByZero

2
test/cmdlineTests/model_checker_divModSlacks_false_bmc/args
View File

@ -1 +1 @@
--model-checker-engine bmc --model-checker-div-mod-no-slacks
--model-checker-engine bmc --model-checker-div-mod-no-slacks --model-checker-targets divByZero

2
test/cmdlineTests/model_checker_divModSlacks_false_chc/args
View File

@ -1 +1 @@
--model-checker-engine chc --model-checker-div-mod-no-slacks
--model-checker-engine chc --model-checker-div-mod-no-slacks --model-checker-targets divByZero

64
test/cmdlineTests/model_checker_targets_default_all_engines/err
View File

@ -1,18 +1,3 @@
Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> model_checker_targets_default_all_engines/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Warning: CHC: Assertion violation happens here.
Counterexample:
arr = []
@ -27,52 +12,3 @@ test.f(0x0, 1)
|
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Warning: CHC: Empty array "pop" happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> model_checker_targets_default_all_engines/input.sol:12:3:
|
12 | arr.pop();
| ^^^^^^^^^
Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> model_checker_targets_default_all_engines/input.sol:13:3:
|
13 | arr[x];
| ^^^^^^
Warning: BMC: Condition is always true.
--> model_checker_targets_default_all_engines/input.sol:6:11:
|
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_default_all_engines/input.sol:10:3:
|
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0
x = 0
Note: Callstack:
Note:

32
test/cmdlineTests/model_checker_targets_default_bmc/err
View File

@ -1,35 +1,3 @@
Warning: BMC: Condition is always true.
--> model_checker_targets_default_bmc/input.sol:6:11:
|
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:
Warning: BMC: Division by zero happens here.
--> model_checker_targets_default_bmc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Note: Counterexample:
<result> = 0
a = 0
x = 0
Note: Callstack:
Note:
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_default_bmc/input.sol:10:3:
|
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0
x = 0
Note: Callstack:
Note:
Warning: BMC: Assertion violation happens here.
--> model_checker_targets_default_bmc/input.sol:11:3:
|

45
test/cmdlineTests/model_checker_targets_default_chc/err
View File

@ -1,18 +1,3 @@
Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> model_checker_targets_default_chc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Warning: CHC: Assertion violation happens here.
Counterexample:
arr = []
@ -27,33 +12,3 @@ test.f(0x0, 1)
|
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Warning: CHC: Empty array "pop" happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> model_checker_targets_default_chc/input.sol:12:3:
|
12 | arr.pop();
| ^^^^^^^^^
Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> model_checker_targets_default_chc/input.sol:13:3:
|
13 | arr[x];
| ^^^^^^

2
test/cmdlineTests/model_checker_timeout_all/args
View File

@ -1 +1 @@
--model-checker-engine all --model-checker-timeout 1000
--model-checker-engine all --model-checker-timeout 1000 --model-checker-targets all

2
test/cmdlineTests/model_checker_timeout_bmc/args
View File

@ -1 +1 @@
--model-checker-engine bmc --model-checker-timeout 1000
--model-checker-engine bmc --model-checker-timeout 1000 --model-checker-targets all

2
test/cmdlineTests/model_checker_timeout_chc/args
View File

@ -1 +1 @@
--model-checker-engine chc --model-checker-timeout 1000
--model-checker-engine chc --model-checker-timeout 1000 --model-checker-targets all

1
test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json
View File

@ -16,6 +16,7 @@
{
"modelChecker":
{
"targets": ["divByZero"],
"engine": "all"
}
}

1
test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/input.json
View File

@ -16,6 +16,7 @@
{
"modelChecker":
{
"targets": ["divByZero"],
"engine": "bmc"
}
}

1
test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/input.json
View File

@ -16,6 +16,7 @@
{
"modelChecker":
{
"targets": ["divByZero"],
"engine": "chc"
}
}

1
test/cmdlineTests/standard_model_checker_divModSlacks_false_all/input.json
View File

@ -16,6 +16,7 @@
{
"modelChecker":
{
"targets": ["divByZero"],
"engine": "all",
"divModNoSlacks": true
}

1
test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/input.json
View File

@ -16,6 +16,7 @@
{
"modelChecker":
{
"targets": ["divByZero"],
"engine": "bmc",
"divModNoSlacks": true
}

1
test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/input.json
View File

@ -16,6 +16,7 @@
{
"modelChecker":
{
"targets": ["divByZero"],
"engine": "chc",
"divModNoSlacks": true
}

1
test/cmdlineTests/standard_model_checker_divModSlacks_wrong/input.json
View File

@ -16,6 +16,7 @@
{
"modelChecker":
{
"targets": ["divByZero"],
"engine": "chc",
"divModNoSlacks": 42
}

3
test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json
View File

@ -3,7 +3,8 @@
{
"smtlib2queries":
{
"0x75b95497d56c30e254a59358d72ddd4e78f9e90db621cfe677e85d05b2252411": "(set-option :produce-models true)
"0x1709577b0e186388ed08c2cf085f20c115c4c94745fb102c5be552ff2e4c7028": "(set-option :produce-models true)
(set-option :timeout 1000)
(set-logic ALL)
(declare-fun |x_3_3| () Int)
(declare-fun |error_0| () Int)

182
test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json
View File

@ -1,44 +1,6 @@
{
"errors":
[
{
"component": "general",
"errorCode": "4281",
"formattedMessage": "Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> A:10:7:
|
10 | \t\t\t\t\t\t2 / x;
| \t\t\t\t\t\t^^^^^
",
"message": "CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)",
"severity": "warning",
"sourceLocation":
{
"end": 216,
"file": "A",
"start": 211
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "6328",
@ -76,150 +38,6 @@ test.f(0x0, 1)",
"start": 245
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "2529",
"formattedMessage": "Warning: CHC: Empty array \"pop\" happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> A:13:7:
|
13 | \t\t\t\t\t\tarr.pop();
| \t\t\t\t\t\t^^^^^^^^^
",
"message": "CHC: Empty array \"pop\" happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)",
"severity": "warning",
"sourceLocation":
{
"end": 275,
"file": "A",
"start": 266
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "6368",
"formattedMessage": "Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> A:14:7:
|
14 | \t\t\t\t\t\tarr[x];
| \t\t\t\t\t\t^^^^^^
",
"message": "CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)",
"severity": "warning",
"sourceLocation":
{
"end": 289,
"file": "A",
"start": 283
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "6838",
"formattedMessage": "Warning: BMC: Condition is always true.
--> A:7:15:
|
7 | \t\t\t\t\t\trequire(x >= 0);
| \t\t\t\t\t\t ^^^^^^
Note: Callstack:
",
"message": "BMC: Condition is always true.",
"secondarySourceLocations":
[
{
"message": "Callstack:"
}
],
"severity": "warning",
"sourceLocation":
{
"end": 165,
"file": "A",
"start": 159
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "1236",
"formattedMessage": "Warning: BMC: Insufficient funds happens here.
--> A:11:7:
|
11 | \t\t\t\t\t\ta.transfer(x);
| \t\t\t\t\t\t^^^^^^^^^^^^^
Note: Counterexample:
a = 0
x = 0
Note: Callstack:
Note:
",
"message": "BMC: Insufficient funds happens here.",
"secondarySourceLocations":
[
{
"message": "Counterexample:
a = 0
x = 0
"
},
{
"message": "Callstack:"
},
{
"message": ""
}
],
"severity": "warning",
"sourceLocation":
{
"end": 237,
"file": "A",
"start": 224
},
"type": "Warning"
}
],
"sources":

111
test/cmdlineTests/standard_model_checker_targets_default_bmc/output.json
View File

@ -1,117 +1,6 @@
{
"errors":
[
{
"component": "general",
"errorCode": "6838",
"formattedMessage": "Warning: BMC: Condition is always true.
--> A:7:15:
|
7 | \t\t\t\t\t\trequire(x >= 0);
| \t\t\t\t\t\t ^^^^^^
Note: Callstack:
",
"message": "BMC: Condition is always true.",
"secondarySourceLocations":
[
{
"message": "Callstack:"
}
],
"severity": "warning",
"sourceLocation":
{
"end": 165,
"file": "A",
"start": 159
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "3046",
"formattedMessage": "Warning: BMC: Division by zero happens here.
--> A:10:7:
|
10 | \t\t\t\t\t\t2 / x;
| \t\t\t\t\t\t^^^^^
Note: Counterexample:
<result> = 0
a = 0
x = 0
Note: Callstack:
Note:
",
"message": "BMC: Division by zero happens here.",
"secondarySourceLocations":
[
{
"message": "Counterexample:
<result> = 0
a = 0
x = 0
"
},
{
"message": "Callstack:"
},
{
"message": ""
}
],
"severity": "warning",
"sourceLocation":
{
"end": 216,
"file": "A",
"start": 211
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "1236",
"formattedMessage": "Warning: BMC: Insufficient funds happens here.
--> A:11:7:
|
11 | \t\t\t\t\t\ta.transfer(x);
| \t\t\t\t\t\t^^^^^^^^^^^^^
Note: Counterexample:
a = 0
x = 0
Note: Callstack:
Note:
",
"message": "BMC: Insufficient funds happens here.",
"secondarySourceLocations":
[
{
"message": "Counterexample:
a = 0
x = 0
"
},
{
"message": "Callstack:"
},
{
"message": ""
}
],
"severity": "warning",
"sourceLocation":
{
"end": 237,
"file": "A",
"start": 224
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "4661",

114
test/cmdlineTests/standard_model_checker_targets_default_chc/output.json
View File

@ -1,44 +1,6 @@
{
"errors":
[
{
"component": "general",
"errorCode": "4281",
"formattedMessage": "Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> A:10:7:
|
10 | \t\t\t\t\t\t2 / x;
| \t\t\t\t\t\t^^^^^
",
"message": "CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)",
"severity": "warning",
"sourceLocation":
{
"end": 216,
"file": "A",
"start": 211
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "6328",
@ -76,82 +38,6 @@ test.f(0x0, 1)",
"start": 245
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "2529",
"formattedMessage": "Warning: CHC: Empty array \"pop\" happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> A:13:7:
|
13 | \t\t\t\t\t\tarr.pop();
| \t\t\t\t\t\t^^^^^^^^^
",
"message": "CHC: Empty array \"pop\" happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)",
"severity": "warning",
"sourceLocation":
{
"end": 275,
"file": "A",
"start": 266
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "6368",
"formattedMessage": "Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)
--> A:14:7:
|
14 | \t\t\t\t\t\tarr[x];
| \t\t\t\t\t\t^^^^^^
",
"message": "CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0x0
x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0x0, 1)",
"severity": "warning",
"sourceLocation":
{
"end": 289,
"file": "A",
"start": 283
},
"type": "Warning"
}
],
"sources":

1
test/cmdlineTests/standard_model_checker_timeout_all/input.json
View File

@ -11,6 +11,7 @@
{
"modelChecker":
{
"targets": ["assert", "divByZero"],
"engine": "all",
"timeout": 1000
}

1
test/cmdlineTests/standard_model_checker_timeout_bmc/input.json
View File

@ -11,6 +11,7 @@
{
"modelChecker":
{
"targets": ["assert", "divByZero"],
"engine": "bmc",
"timeout": 1000
}

1
test/cmdlineTests/standard_model_checker_timeout_chc/input.json
View File

@ -11,6 +11,7 @@
{
"modelChecker":
{
"targets": ["assert", "divByZero"],
"engine": "chc",
"timeout": 1000
}

3
test/libsolidity/SMTCheckerTest.cpp
View File

@ -82,6 +82,9 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
if (m_modelCheckerSettings.solvers.none() || m_modelCheckerSettings.engine.none())
m_shouldRun = false;
// Disable the default timeout to force resource limit.
m_modelCheckerSettings.timeout = {};
auto const& ignoreCex = m_reader.stringSetting("SMTIgnoreCex", "yes");
if (ignoreCex == "no")
m_ignoreCex = false;