From e7f36a2d3550f265e9a49e25f16cd562062043e4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 14 Sep 2016 10:32:17 -0700
Subject: [PATCH] remove special characters

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/python/socrates.py | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/examples/python/socrates.py b/examples/python/socrates.py
index 79a1b57f1..49067225f 100644
--- a/examples/python/socrates.py
+++ b/examples/python/socrates.py
@@ -1,9 +1,9 @@
 ############################################
 # Copyright (c) Microsoft Corporation. All Rights Reserved.
-# 
-# all humans are mortal
-# Socrates is a human
-# so Socrates mortal 
+#
+# all humans are mortal
+# Socrates is a human
+# so Socrates mortal 
 ############################################
 
 from z3 import *
@@ -15,10 +15,10 @@ Object = DeclareSort('Object')
 Human = Function('Human', Object, BoolSort())
 Mortal = Function('Mortal', Object, BoolSort())
 
-# a well known philosopher 
+# a well known philosopher 
 socrates = Const('socrates', Object)
 
-# free variables used in forall must be declared Const in python
+# free variables used in forall must be declared Const in python
 x = Const('x', Object)
 
 axioms = [ForAll([x], Implies(Human(x), Mortal(x))), 
@@ -27,7 +27,9 @@ axioms = [ForAll([x], Implies(Human(x), Mortal(x))),
 
 s = Solver()
 s.add(axioms)
-# classical refutation
+# classical refutation
 s.add(Mortal(socrates) == False)
 
-print(s.check()) # prints unsat so socrates is Mortal
+print(s.check()) # prints unsat so socrates is Mortal
+
+# print(s.proof()) # prints a low level (not readable) proof object.