mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix #7165
This commit is contained in:
parent
6450a7a0b8
commit
b8a69987c3
|
@ -5445,10 +5445,10 @@ def EnumSort(name, values, ctx=None):
|
|||
num = len(values)
|
||||
_val_names = (Symbol * num)()
|
||||
for i in range(num):
|
||||
_val_names[i] = to_symbol(values[i])
|
||||
_val_names[i] = to_symbol(values[i], ctx)
|
||||
_values = (FuncDecl * num)()
|
||||
_testers = (FuncDecl * num)()
|
||||
name = to_symbol(name)
|
||||
name = to_symbol(name, ctx)
|
||||
S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
|
||||
V = []
|
||||
for i in range(num):
|
||||
|
|
|
@ -696,7 +696,7 @@ bool goal::is_cnf() const {
|
|||
if (!is_literal(lit))
|
||||
return false;
|
||||
}
|
||||
if (!is_literal(f))
|
||||
else if (!is_literal(f))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
|
|
Loading…
Reference in a new issue