From c6a5aa0cc4a83a7eab5913919ca46fcdd5c3a239 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Dec 2021 09:21:02 -0800
Subject: [PATCH] try th_lemma, update documentation of api functions for
 creating strings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/z3_api.h                   |  7 ++++++-
 src/smt/smt_theory.cpp             |  7 +++++++
 src/smt/theory_user_propagator.cpp | 14 ++------------
 3 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 19ceef7c5..2fe9a96e7 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3451,6 +3451,10 @@ extern "C" {
     /**
        \brief Create a sort for unicode strings.
 
+       The sort for characters can be changed to ASCII by setting
+       the global parameter \c encoding to \c ascii, or alternative
+       to 16 bit characters by setting \c encoding to \c bmp.
+
        def_API('Z3_mk_string_sort', SORT, (_in(CONTEXT), ))
      */
     Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
@@ -3459,7 +3463,8 @@ extern "C" {
        \brief Create a sort for unicode characters.
 
        The sort for characters can be changed to ASCII by setting
-       the global parameter \c unicode to \c false.
+       the global parameter \c encoding to \c ascii, or alternative
+       to 16 bit characters by setting \c encoding to \c bmp.
 
        def_API('Z3_mk_char_sort', SORT, (_in(CONTEXT), ))
     */
diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index 0c876e8bc..fb8d61e8a 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -150,6 +150,13 @@ namespace smt {
 
     literal theory::mk_literal(expr* _e) {
         expr_ref e(_e, m);
+        if (has_quantifiers(e)) {
+            expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m);
+            expr_ref eq(m.mk_eq(fn, e), m);
+            ctx.assert_expr(eq);
+            ctx.internalize_assertions();
+            return mk_literal(fn);
+        }
         bool is_not = m.is_not(_e, _e);
         if (!ctx.e_internalized(_e)) {
             ctx.internalize(_e, is_quantifier(_e));
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index 9e10b96c5..722e3343d 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -146,20 +146,10 @@ void theory_user_propagator::propagate() {
                 lit.neg();
             for (auto const& [a,b] : m_eqs)
                 m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
-            literal lit;
-            if (has_quantifiers(prop.m_conseq)) {
-                expr_ref fn(m.mk_fresh_const("user-conseq", m.mk_bool_sort()), m);
-                expr_ref eq(m.mk_eq(fn, prop.m_conseq), m);
-                ctx.assert_expr(eq);
-                ctx.internalize_assertions();
-                lit = mk_literal(fn);
-            }
-            else {
-                lit = mk_literal(prop.m_conseq);
-            }
+            literal lit = mk_literal(prop.m_conseq);            
             ctx.mark_as_relevant(lit);
             m_lits.push_back(lit);
-            ctx.mk_th_axiom(get_id(), m_lits);
+            ctx.mk_th_lemma(get_id(), m_lits);
             TRACE("user_propagate", ctx.display(tout););
         }
         ++m_stats.m_num_propagations;