From 886c62ef41106740589eb5806f579fddc55ba67e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2019 10:30:44 -0800 Subject: [PATCH] add example from #2138 Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index ab9c73209..f93045c9d 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1166,6 +1166,14 @@ static void parse_example() { // expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))"); } +static void parse_string() { + std::cout << "parse string\n"; + z3::context c; + z3::solver s(c); + s.from_string("(declare-const x Int)(assert (> x 10))"); + std::cout << s.check() << "\n"; +} + void mk_model_example() { context c; @@ -1252,6 +1260,7 @@ int main() { sudoku_example(); std::cout << "\n"; consequence_example(); std::cout << "\n"; parse_example(); std::cout << "\n"; + parse_string(); std::cout << "\n"; mk_model_example(); std::cout << "\n"; recfun_example(); std::cout << "\n"; std::cout << "done\n";