From 0bfea99cffc058424ca07f462b3067da50520a70 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 1 Dec 2017 14:43:52 -0800
Subject: [PATCH] fix issues found in parsing examples

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c++/example.cpp   | 2 +-
 examples/dotnet/Program.cs | 4 ++--
 src/api/api_parsers.cpp    | 8 ++++++--
 src/cmd_context/pdecl.cpp  | 1 +
 4 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index a6846eb4d..df977268a 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1139,7 +1139,7 @@ static void parse_example() {
     expr a = c.parse_string("(assert a)", sorts, decls);
     std::cout << a << "\n";
 
-    expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))");
+    // expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))");
 }
 
 
diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index e5c863b0a..af3c59099 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -1383,7 +1383,7 @@ namespace test_mapi
         {
             Console.WriteLine("ParserExample1");
 
-            var fml = ctx.ParseSMTLIB2String("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))");
+            var fml = ctx.ParseSMTLIB2String("(declare-const x Int) (declare-const y Int) (assert (> x y)) (assert (> x 0))");
             Console.WriteLine("formula {0}", fml);
 
             Model m = Check(ctx, fml, Status.SATISFIABLE);
@@ -1417,7 +1417,7 @@ namespace test_mapi
 
             BoolExpr ca = CommAxiom(ctx, g);
 
-            BoolExpr thm = ctx.ParseSMTLIB2String("(assert (forall ((x Int) (y Int)) (implies (= x y) (= (gg x 0) (gg 0 y)))))",
+            BoolExpr thm = ctx.ParseSMTLIB2String("(assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))",
              null, null,
              new Symbol[] { ctx.MkSymbol("gg") },
              new FuncDecl[] { g });
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index a7235ef65..d5a98672b 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -52,8 +52,12 @@ extern "C" {
             ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
         }
         for (unsigned i = 0; i < num_sorts; ++i) {
-            psort* ps = ctx->pm().mk_psort_cnst(to_sort(sorts[i]));
-            ctx->insert(ctx->pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps));
+            sort* srt = to_sort(sorts[i]);
+            symbol name(to_symbol(sort_names[i]));
+            if (!ctx->find_psort_decl(name)) {
+                psort* ps = ctx->pm().mk_psort_cnst(srt);
+                ctx->insert(ctx->pm().mk_psort_user_decl(0, name, ps));
+            }
         }
         std::stringstream errstrm;
         ctx->set_regular_stream(errstrm);
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 8a7359e3a..d1185544a 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -853,6 +853,7 @@ pdecl_manager::~pdecl_manager() {
     dec_ref(m_list);
     reset_sort_info();
     SASSERT(m_sort2psort.empty());    
+    SASSERT(m_table.empty());
 }
 
 psort * pdecl_manager::mk_psort_cnst(sort * s) {