From 0ce200144923fe5856054bcad11c9f5471f0d791 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Mar 2018 11:39:22 -0800 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 11 ----------- scripts/mk_util.py | 9 +++++++-- 2 files changed, 7 insertions(+), 13 deletions(-) diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index b2736df4c..772440b42 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -1609,7 +1609,6 @@ public: display_inference(out, "rewrite", "thm", p); break; case Z3_OP_PR_PULL_QUANT: - case Z3_OP_PR_PULL_QUANT_STAR: display_inference(out, "pull_quant", "thm", p); break; case Z3_OP_PR_PUSH_QUANT: @@ -1669,12 +1668,6 @@ public: case Z3_OP_PR_NNF_NEG: display_inference(out, "nnf_neg", "sab", p); break; - case Z3_OP_PR_NNF_STAR: - display_inference(out, "nnf", "sab", p); - break; - case Z3_OP_PR_CNF_STAR: - display_inference(out, "cnf", "sab", p); - break; case Z3_OP_PR_SKOLEMIZE: display_inference(out, "skolemize", "sab", p); break; @@ -1706,10 +1699,6 @@ public: return display_hyp_inference(out, "modus_ponens", "thm", conclusion, hyp, hyp2); } case Z3_OP_PR_NNF_POS: - case Z3_OP_PR_NNF_STAR: - return display_hyp_inference(out, "nnf", "sab", conclusion, hyp); - case Z3_OP_PR_CNF_STAR: - return display_hyp_inference(out, "cnf", "sab", conclusion, hyp); case Z3_OP_PR_SKOLEMIZE: return display_hyp_inference(out, "skolemize", "sab", conclusion, hyp); case Z3_OP_PR_TRANSITIVITY: diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 03256125c..fecc207d8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -889,8 +889,13 @@ def is_CXX_gpp(): return is_compiler(CXX, 'g++') def is_clang_in_gpp_form(cc): - version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8') - return version_string.find('clang') != -1 + str = check_output([cc, '--version']) + try: + version_string = str.encode('utf-8') + except: + version_string = str + clang = 'clang'.encode('utf-8') + return version_string.find(clang) != -1 def is_CXX_clangpp(): if is_compiler(CXX, 'g++'):