diff options
| author | Alex Beregszaszi <alex@rtfs.hu> | 2018-11-22 21:10:35 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-22 21:10:35 +0800 |
| commit | a5411965e6d7abf50f896291d69cab820db6ef87 (patch) | |
| tree | 227e40834ef555f0f351b54c29564ff9a383785d /libsolidity/formal/SMTLib2Interface.cpp | |
| parent | 60fbc32fdfa4657edd3ebb047b7f65626ac3baba (diff) | |
| parent | 20accf1a90e6b3dd077c67e6d31d1c56fedad5f5 (diff) | |
| download | dexon-solidity-a5411965e6d7abf50f896291d69cab820db6ef87.tar.gz dexon-solidity-a5411965e6d7abf50f896291d69cab820db6ef87.tar.zst dexon-solidity-a5411965e6d7abf50f896291d69cab820db6ef87.zip | |
Merge pull request #5478 from ethereum/smt_refactor_sort_patch3
[SMTChecker] Add ArraySort and array operations
Diffstat (limited to 'libsolidity/formal/SMTLib2Interface.cpp')
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index bb85860f..55c72cfc 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -144,6 +144,11 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) return "Int"; case Kind::Bool: return "Bool"; + case Kind::Array: + { + auto const& arraySort = dynamic_cast<ArraySort const&>(_sort); + return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')'; + } default: solAssert(false, "Invalid SMT sort"); } |