From ed9674be8db28e1163e109ac34e66cd71e030265 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 18 Sep 2019 22:33:00 +0200 Subject: [PATCH] [SMTChecker] Add as const function to SMTLib2Interface --- libsolidity/formal/SMTLib2Interface.cpp | 23 +++++++++++++++---- .../smtCheckerTestsJSON/multi.json | 4 ++-- .../smtCheckerTestsJSON/simple.json | 2 +- 3 files changed, 22 insertions(+), 7 deletions(-) diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index cd516109e..c0d37431e 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -46,7 +46,7 @@ void SMTLib2Interface::reset() m_accumulatedOutput.emplace_back(); m_variables.clear(); write("(set-option :produce-models true)"); - write("(set-logic QF_UFLIA)"); + write("(set-logic ALL)"); } void SMTLib2Interface::push() @@ -126,9 +126,24 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr) { if (_expr.arguments.empty()) return _expr.name; - std::string sexpr = "(" + _expr.name; - for (auto const& arg: _expr.arguments) - sexpr += " " + toSExpr(arg); + + std::string sexpr = "("; + if (_expr.name == "const_array") + { + solAssert(_expr.arguments.size() == 2, ""); + auto sortSort = std::dynamic_pointer_cast(_expr.arguments.at(0).sort); + solAssert(sortSort, ""); + auto arraySort = dynamic_pointer_cast(sortSort->inner); + solAssert(arraySort, ""); + sexpr += "(as const " + toSmtLibSort(*arraySort) + ") "; + sexpr += toSExpr(_expr.arguments.at(1)); + } + else + { + sexpr += _expr.name; + for (auto const& arg: _expr.arguments) + sexpr += " " + toSExpr(arg); + } sexpr += ")"; return sexpr; } diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index e66b17ab0..b125712fd 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -3,8 +3,8 @@ { "smtlib2responses": { - "0x047d0c67d7e03c5ac96ca227d1e19ba63257f4ab19cef30029413219ec8963af": "sat\n((|EVALEXPR_0| 0))\n", - "0xada7569fb01a9b3e2823517ed40dcc99b11fb1e433e6e3ec8a8713f6f95753d3": "sat\n((|EVALEXPR_0| 1))\n" + "0x82fb8ee094f0f56b7a63a74177b54a1710d6fc531d426f288c18f36b76cf6a8b": "sat\n((|EVALEXPR_0| 1))\n", + "0xb524e7c577188e2e36f0e67fead51269fa0f8b8fb41bff2d973dcf584d38cd1e": "sat\n((|EVALEXPR_0| 0))\n" } } } diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json index 2f7ebdffb..89eac1b80 100644 --- a/test/libsolidity/smtCheckerTestsJSON/simple.json +++ b/test/libsolidity/smtCheckerTestsJSON/simple.json @@ -3,7 +3,7 @@ { "smtlib2responses": { - "0x2e32517a1410b1a16decd448bb9bac7789d7cf1c6f98703ed6bacfcad6abebfb": "sat\n((|EVALEXPR_0| 0))\n" + "0x45c37a9829e623d7838d82b547d297cd446d6b5faff36c53a56862fcee50fb41": "sat\n((|EVALEXPR_0| 0))\n" } } }