From f3d657ebd1d902fd89972054a263011bc8b510b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jul 2016 12:09:23 -0700 Subject: [PATCH] add tptp5 example to cmake, adding output SZS directives for Geoff Signed-off-by: Nikolaj Bjorner --- contrib/cmake/examples/CMakeLists.txt | 1 + examples/tptp/tptp5.cpp | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/contrib/cmake/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt index b8cecbe63..49ea72fdc 100644 --- a/contrib/cmake/examples/CMakeLists.txt +++ b/contrib/cmake/examples/CMakeLists.txt @@ -1,2 +1,3 @@ add_subdirectory(c) add_subdirectory(c++) +add_subdirectory(tptp) diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index 2773b6cc9..5f45f6c1c 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -2408,7 +2408,9 @@ static void prove_tptp() { } if (g_generate_proof) { try { + std::cout << "SZS output start Proof\n"; display_proof(ctx, fmls, solver); + std::cout << "SZS output end Proof\n"; } catch (failure_ex& ex) { std::cerr << "Proof display could not be completed: " << ex.msg << "\n"; @@ -2434,7 +2436,9 @@ static void prove_tptp() { std::cout << "SZS status Satisfiable\n"; } if (g_generate_model) { + std::cout << "SZS output start Model\n"; display_model(ctx, solver.get_model()); + std::cout << "SZS output end Model\n"; } break; case z3::unknown: