fix #7165

Z3Prover · Mar 17, 2024 · b8a6998 · b8a6998
1 parent 6450a7a
commit b8a6998
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
@@ -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):

diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
@@ -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;