z3py:尝试使用集成员身份时出错

Question

在Z3Py中，我想表示一个（整数）变量的值必须在一组有效值中。在这种情况下，E12 series通常用于电子学中的元件值。你知道吗

我可以用一堆Z3或子句（value == 12 || value == 15 || ...）来实现这一点，但这看起来非常丑陋和低效。每个组件都是我的系统得到大约80个约束来表达这一点。这无疑会使读取unsat错误消息变得困难。你知道吗

当我尝试在Z3Py中使用Set类型时，它会因segfault而崩溃。下面的代码复制了这个。你知道吗

这是使用集合的正确方法吗？有没有其他干净的方法来做同样的事情？你知道吗

import z3
import pytest

e12_series = (1.0, 1.2, 1.5, 1.8, 2.2, 2.7, 3.3, 3.9, 4.7, 5.6, 6.8, 8.2, 10.0)

def e_values(start_decade=1, end_decade=6, series=e12_series):
    values = []
    for decade in range(start_decade, end_decade):
        values += [ int(v*10)*10**(decade-1) for v in series ]    

    return values

def value_in(value, valid):
    options = [ value == v for v in valid ]
    return z3.Or(options)

# Values to test with
E12_VALID=[
    120, 18e3,
]
E12_INVALID=[
    119, 19e3,
]

EXAMPLES = []
EXAMPLES += [ (True, v) for v in E12_VALID ]
EXAMPLES += [ (False, v) for v in E12_INVALID ]

@pytest.mark.parametrize('example', EXAMPLES)
def test_bruteforce(example):
    expect_valid, value = example 
    valid_values = e_values()

    s = z3.Solver()
    var = z3.IntVal(value)
    s.add(value_in(var, valid_values))
    satisfied = str(s.check()) == 'sat'
    assert satisfied == expect_valid, s

@pytest.mark.parametrize('example', EXAMPLES)
def test_set(example):
    expect_valid, value = example

    # create a set
    valid_values = e_values()
    e12 = z3.SetSort(z3.IntSort())
    for val in valid_values:
        z3.SetAdd(e12, val)

    s = z3.Solver()
    var = z3.IntVal(value)
    s.add(z3.IsMember(var, e12))
    satisfied = str(s.check()) == 'sat'
    assert satisfied == expect_valid, s

使用pytest -v setmembers.py运行时，输出为：

platform linux -- Python 3.7.3, pytest-4.4.1, py-1.8.0, pluggy-0.9.0 -- /usr/bin/python
plugins: cov-2.6.1, hypothesis-4.17.0
collected 8 items                                                                                                                                                                                                                            

setmembers.py::test_bruteforce[example0] PASSED                                                                                                                                                                                        [ 12%]
setmembers.py::test_bruteforce[example1] PASSED                                                                                                                                                                                        [ 25%]
setmembers.py::test_bruteforce[example2] PASSED                                                                                                                                                                                        [ 37%]
setmembers.py::test_bruteforce[example3] PASSED                                                                                                                                                                                        [ 50%]
setmembers.py::test_set[example0] Segmentation fault (core dumped)

在Arch Linux上使用python-z3 4.8.4-2