diff options
Diffstat (limited to 'examples/api/python/linear_arith.py')
-rwxr-xr-x | examples/api/python/linear_arith.py | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index 6ae6427b1..bab9680b3 100755 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -4,7 +4,7 @@ #! \file linear_arith.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. @@ -54,9 +54,9 @@ if __name__ == "__main__": slv.push() diff_leq_two_thirds = slv.mkTerm(kinds.Leq, diff, two_thirds) print("Prove that", diff_leq_two_thirds, "with CVC4") - print("CVC4 should report VALID") + print("CVC4 should report ENTAILED") print("Result from CVC4 is:", - slv.checkValidAssuming(diff_leq_two_thirds)) + slv.checkEntailed(diff_leq_two_thirds)) slv.pop() print() |