From 5652d2a157b85afb3a96bd0732fe219b379dbf78 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 25 Jul 2021 11:59:42 -0700
Subject: [PATCH] #5429 #5431

---
 src/ast/rewriter/seq_rewriter.cpp | 15 +--------------
 src/smt/mam.cpp                   |  8 ++++++--
 2 files changed, 7 insertions(+), 16 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index f2286503f..ff4f62533 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3339,8 +3339,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             //while mk_empty() = [], because deriv(epsilon) = [] = nothing
             return mk_empty();
         }
-        else if (str().is_itos(r1, r2))
-        {
+        else if (str().is_itos(r1, r2)) {
             //
             // here r1 = (str.from_int r2) and r2 is non-ground 
             // or else the expression would have been simplified earlier
@@ -3352,18 +3351,6 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             tl = re().mk_to_re(str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1))));            
             return re_and(result, tl);
         }
-#if 0
-        else {
-            hd = str().mk_nth_i(r1, m_autil.mk_int(0));
-            tl = str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1)));
-            result = re().mk_to_re(tl);
-            result = 
-                m().mk_ite(m_br.mk_eq_rw(r1, str().mk_empty(m().get_sort(r1))), 
-                           mk_empty(),
-                           re_and(m_br.mk_eq_rw(ele, hd), result));
-            return result;
-        }
-#endif
     }
     else if (re().is_reverse(r, r1) && re().is_to_re(r1, r2)) {
         // Reverses are rewritten so that the only derivative case is
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index f8d99f398..0d09f07ea 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -121,7 +121,7 @@ namespace {
 
     struct instruction {
         opcode         m_opcode;
-        instruction *  m_next;
+        instruction* m_next = nullptr;
 #ifdef _PROFILE_MAM
         unsigned       m_counter; // how often it was executed
 #endif
@@ -1224,9 +1224,10 @@ namespace {
                     return;
 
             SASSERT(head->m_next == 0);
+
             m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
 
-            for (instruction * curr : m_seq) {
+            for (instruction* curr : m_seq) {
                 head->m_next = curr;
                 head = curr;
             }
@@ -2309,7 +2310,10 @@ namespace {
 
     main_loop:
 
+        if (!m_pc)
+            goto backtrack;
         TRACE("mam_int", display_pc_info(tout););
+        
 #ifdef _PROFILE_MAM
         const_cast<instruction*>(m_pc)->m_counter++;
 #endif