From 021bd8a994c63368a45c1819cbf7399ea5332ece Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 21 Dec 2020 17:08:38 -0800
Subject: [PATCH] sym file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/mk_nuget_task.py     | 9 +++++++--
 src/model/model.cpp          | 2 ++
 src/smt/smt_internalizer.cpp | 3 +--
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py
index 220957386..28e090f44 100644
--- a/scripts/mk_nuget_task.py
+++ b/scripts/mk_nuget_task.py
@@ -113,8 +113,10 @@ Linux Dependencies:
     print(contents)
     sym = ""
     if symbols:
-        sym = "s"
-    with open(f"out/Microsoft.Z3.x64.{sym}.nuspec", 'w') as f:
+        sym = "sym."
+    file = f"out/Microsoft.Z3.x64.{sym}nuspec"
+    print(file)
+    with open(file, 'w') as f:
         f.write(contents)
         
 def main():
@@ -125,8 +127,11 @@ def main():
     commit = sys.argv[5]
     source_root = sys.argv[6]
     symbols = False
+    if len(sys.argv) > 7:
+        print(sys.argv[7])
     if len(sys.argv) > 7 and "symbols" == sys.argv[7]:
         symbols = True
+    print(symbols)
     print(packages)
     mk_dir(packages)
     unpack(packages, symbols)
diff --git a/src/model/model.cpp b/src/model/model.cpp
index b14887027..9c22e0e06 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -203,6 +203,7 @@ struct model::top_sort : public ::top_sort<func_decl> {
     {
         params_ref p;
         p.set_bool("elim_ite", false);
+        p.set_bool("ite_extra_rules", true);
         m_rewrite.updt_params(p);
     }
 
@@ -483,6 +484,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
             }
             
             if (t != new_t.get()) trail.push_back(new_t);
+            CTRACE("model", (t != new_t.get()), tout << mk_bounded_pp(t, m) << " " << new_t << "\n";);
             todo.pop_back();
             cache.insert(t, new_t);
             break;
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 28fdaf3b5..24f85ca1b 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -338,9 +338,8 @@ namespace smt {
     }
 
     void context::ensure_internalized(expr* e) {
-        if (!e_internalized(e)) {
+        if (!e_internalized(e)) 
             internalize(e, false);
-        }
     }
 
     /**