From a7ef33c136c003d0ba0e44ec4553982e2384656b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Sep 2017 11:31:50 -0700
Subject: [PATCH] fix bug in generation of non-recursive constructor, modular
 starting point shifts during recursive calls

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/datatype_decl_plugin.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index b4f30767f..f86668ea8 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -857,9 +857,9 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
     ptr_vector<func_decl> const * constructors = get_datatype_constructors(ty);
     // step 1)
     unsigned sz = constructors->size();
-    ++m_start;
+    unsigned start = ++m_start;
     for (unsigned j = 0; j < sz; ++j) {        
-        func_decl * c = (*constructors)[(j + m_start) % sz];
+        func_decl * c = (*constructors)[(j + start) % sz];
         unsigned num_args = c->get_arity();
         unsigned i = 0;
         for (; i < num_args; i++) {
@@ -872,7 +872,7 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
     }
     // step 2)
     for (unsigned j = 0; j < sz; ++j) {        
-        func_decl * c = (*constructors)[(j + m_start) % sz];
+        func_decl * c = (*constructors)[(j + start) % sz];
         TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";);
         unsigned num_args = c->get_arity();
         unsigned i = 0;