Fix unterminated parentheses typo in SMTLib2

Found by @leonardoalt
This commit is contained in:
Alex Beregszaszi 2018-07-27 17:31:16 +01:00
parent 2794a22d84
commit dea0567e06

View File

@ -143,7 +143,7 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
{ {
auto const& e = _expressionsToEvaluate.at(i); auto const& e = _expressionsToEvaluate.at(i);
solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate."); solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate.");
command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + "\n"; command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + ")\n";
command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
} }
command += "(check-sat)\n"; command += "(check-sat)\n";