From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 25 Mar 2022 13:08:01 +0000 (-0700)
Subject: Fix Python API tests (#8392)
X-Git-Tag: cvc5-1.0.0~177
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c4ad6a462ea1f583950af993468a10d45ca7e0c;p=cvc5.git

Fix Python API tests (#8392)

Note that we are currently not running API tests on the CI due to the
changes in 23dd064.
---

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 6329c1011..6f18d96b4 100644
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -2468,6 +2468,7 @@ def test_issue7000(solver):
 
 
 def test_mk_sygus_var(solver):
+    solver.setOption("sygus", "true")
     boolSort = solver.getBooleanSort()
     intSort = solver.getIntegerSort()
     funSort = solver.mkFunctionSort(intSort, boolSort)
@@ -2515,7 +2516,7 @@ def test_synth_fun(solver):
     with pytest.raises(RuntimeError):
         solver.synthFun("f6", [x], boolean, g2)
     slv = cvc5.Solver()
-    solver.setOption("sygus", "true")
+    slv.setOption("sygus", "true")
     x2 = slv.mkVar(slv.getBooleanSort())
     slv.synthFun("f1", [x2], slv.getBooleanSort())
     with pytest.raises(RuntimeError):