summaryrefslogtreecommitdiff
path: root/examples/api/python/combination.py
diff options
context:
space:
mode:
Diffstat (limited to 'examples/api/python/combination.py')
-rwxr-xr-xexamples/api/python/combination.py6
1 files changed, 3 insertions, 3 deletions
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index 1b488d7d5..7a8055bdf 100755
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -4,7 +4,7 @@
#! \file combination.py
## \verbatim
## Top contributors (to current version):
- ## Makai Mann
+ ## Makai Mann, Aina Niemetz
## This file is part of the CVC4 project.
## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
## in the top-level source directory) and their institutional affiliations.
@@ -69,8 +69,8 @@ if __name__ == "__main__":
slv.assertFormula(assertions)
print("Given the following assertions:", assertions, "\n")
- print("Prove x /= y is valid.\nCVC4: ",
- slv.checkValidAssuming(slv.mkTerm(kinds.Distinct, x, y)), "\n")
+ print("Prove x /= y is entailed.\nCVC4: ",
+ slv.checkEntailed(slv.mkTerm(kinds.Distinct, x, y)), "\n")
print("Call checkSat to show that the assertions are satisfiable")
print("CVC4:", slv.checkSat(), "\n")
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback