From b8a69987c31a74ac0a611b99ca97bb3edd28dc86 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 17 Mar 2024 16:33:32 -0700
Subject: [PATCH] fix #7165

---
 src/api/python/z3/z3.py | 4 ++--
 src/tactic/goal.cpp     | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 16db39afd60..9a3dadda23e 100644
--- 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
index 23e3ff969eb..43cecf92d74 100644
--- 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;