summaryrefslogtreecommitdiff
path: root/examples/api/python/sygus-fun.py
diff options
context:
space:
mode:
Diffstat (limited to 'examples/api/python/sygus-fun.py')
-rw-r--r--examples/api/python/sygus-fun.py4
1 files changed, 2 insertions, 2 deletions
diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index d331c9f9e..a85902961 100644
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -41,8 +41,8 @@ if __name__ == "__main__":
start_bool = slv.mkVar(boolean, "StartBool")
# define the rules
- zero = slv.mkReal(0)
- one = slv.mkReal(1)
+ zero = slv.mkInteger(0)
+ one = slv.mkInteger(1)
plus = slv.mkTerm(kinds.Plus, start, start)
minus = slv.mkTerm(kinds.Minus, start, start)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback