From 9245e61775d7d7b46b04461b3ae7161d09f8b172 Mon Sep 17 00:00:00 2001
From: Mathieu Roger <rogma.boami@free.fr>
Date: Wed, 14 Sep 2016 21:36:39 +0200
Subject: [PATCH] Update socrates.py

---
 examples/python/socrates.py | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/examples/python/socrates.py b/examples/python/socrates.py
index 49067225f..8d44b41ea 100644
--- a/examples/python/socrates.py
+++ b/examples/python/socrates.py
@@ -8,8 +8,6 @@
 
 from z3 import *
 
-set_param(proof=True)
-
 Object = DeclareSort('Object')
 
 Human = Function('Human', Object, BoolSort())
@@ -22,14 +20,15 @@ socrates = Const('socrates', Object)
 x = Const('x', Object)
 
 axioms = [ForAll([x], Implies(Human(x), Mortal(x))), 
-          Human(socrates) == True]
+          Human(socrates)]
 
 
 s = Solver()
 s.add(axioms)
+
+print(s.check()) # prints sat so axioms are coherents
+
 # classical refutation
-s.add(Mortal(socrates) == False)
+s.add(Not(Mortal(socrates)))
 
 print(s.check()) # prints unsat so socrates is Mortal
-
-# print(s.proof()) # prints a low level (not readable) proof object.