mirror of
https://github.com/Z3Prover/z3
synced 2026-05-30 21:57:46 +00:00
Add comprehensive tests for Python API bug fixes
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
parent
629d999fa2
commit
69bf729a22
1 changed files with 5 additions and 4 deletions
|
|
@ -11,10 +11,8 @@ These tests validate:
|
||||||
import sys
|
import sys
|
||||||
import os
|
import os
|
||||||
|
|
||||||
# Add the z3 module to the path
|
# Make sure we can import z3 from the build directory
|
||||||
sys.path.insert(0, os.path.join(os.path.dirname(__file__), 'z3'))
|
from z3 import z3
|
||||||
|
|
||||||
import z3
|
|
||||||
|
|
||||||
|
|
||||||
def test_ratval_division_by_zero():
|
def test_ratval_division_by_zero():
|
||||||
|
|
@ -98,6 +96,9 @@ def test_user_propagate_double_registration():
|
||||||
try:
|
try:
|
||||||
# Create a minimal UserPropagateBase subclass
|
# Create a minimal UserPropagateBase subclass
|
||||||
class TestPropagator(z3.UserPropagateBase):
|
class TestPropagator(z3.UserPropagateBase):
|
||||||
|
def __init__(self, s=None):
|
||||||
|
super().__init__(s, ctx=z3.Context() if s is None else None)
|
||||||
|
|
||||||
def push(self):
|
def push(self):
|
||||||
pass
|
pass
|
||||||
def pop(self, num_scopes):
|
def pop(self, num_scopes):
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue