From 7db1847f51dd18f731aad7b4920d78faa9951208 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 26 Jun 2017 09:36:53 -0700
Subject: [PATCH] fix bitrot in maxsat example reference management #1116

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/maxsat/maxsat.c                | 12 ++++++++++++
 src/util/lp/sparse_matrix_instances.cpp |  2 +-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c
index eaf01482c..45325311e 100644
--- a/examples/maxsat/maxsat.c
+++ b/examples/maxsat/maxsat.c
@@ -358,6 +358,7 @@ void tst_at_most_one()
 {
     Z3_context ctx = mk_context();
     Z3_solver s = Z3_mk_solver(ctx);
+    Z3_solver_inc_ref(ctx, s);
     Z3_ast k1      = mk_bool_var(ctx, "k1");
     Z3_ast k2      = mk_bool_var(ctx, "k2");
     Z3_ast k3      = mk_bool_var(ctx, "k3");
@@ -376,7 +377,9 @@ void tst_at_most_one()
     if (result != Z3_L_TRUE)
         error("BUG");
     m = Z3_solver_get_model(ctx, s);
+    Z3_model_inc_ref(ctx, m);
     printf("model:\n%s\n", Z3_model_to_string(ctx, m));
+    Z3_model_dec_ref(ctx, m);
     Z3_solver_assert(ctx, s, mk_binary_or(ctx, k2, k3));
     Z3_solver_assert(ctx, s, mk_binary_or(ctx, k1, k6));
     printf("it must be sat...\n");
@@ -384,12 +387,15 @@ void tst_at_most_one()
     if (result != Z3_L_TRUE)
         error("BUG");
     m = Z3_solver_get_model(ctx, s);
+    Z3_model_inc_ref(ctx, m);
     printf("model:\n%s\n", Z3_model_to_string(ctx, m));
     Z3_solver_assert(ctx, s, mk_binary_or(ctx, k4, k5));
     printf("it must be unsat...\n");
     result = Z3_solver_check(ctx, s);
     if (result != Z3_L_FALSE)
         error("BUG");
+    Z3_model_dec_ref(ctx, m);
+    Z3_solver_dec_ref(ctx, s);
     Z3_del_context(ctx);
 }
 
@@ -455,7 +461,9 @@ int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast *
             return num_soft_cnstrs - k - 1;
         }
 	m = Z3_solver_get_model(ctx, s);
+        Z3_model_inc_ref(ctx, m);
         num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars);
+        Z3_model_dec_ref(ctx, m);
         if (num_disabled > k) {
             error("BUG");
         }
@@ -506,6 +514,7 @@ int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs,
     }
     else {
         core = Z3_solver_get_unsat_core(ctx, s);
+        Z3_ast_vector_inc_ref(ctx, core);
 	core_size = Z3_ast_vector_size(ctx, core);
         block_vars = (Z3_ast*) malloc(sizeof(Z3_ast) * core_size);
         k = 0;
@@ -531,6 +540,7 @@ int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs,
             }
         }
         assert_at_most_one(ctx, s, k, block_vars);
+        Z3_ast_vector_dec_ref(ctx, core);
         return 0; // not done.
     }
 }
@@ -598,6 +608,7 @@ int smtlib_maxsat(char * file_name, int approach)
     unsigned result = 0;
     ctx = mk_context();
     s = Z3_mk_solver(ctx);
+    Z3_solver_inc_ref(ctx, s);
     Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0);
     hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs);
     soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs);
@@ -615,6 +626,7 @@ int smtlib_maxsat(char * file_name, int approach)
     }
     free_cnstr_array(hard_cnstrs);
     free_cnstr_array(soft_cnstrs);
+    Z3_solver_dec_ref(ctx, s);
     return result;
 }
 
diff --git a/src/util/lp/sparse_matrix_instances.cpp b/src/util/lp/sparse_matrix_instances.cpp
index f80b60365..c06fcbf05 100644
--- a/src/util/lp/sparse_matrix_instances.cpp
+++ b/src/util/lp/sparse_matrix_instances.cpp
@@ -2,8 +2,8 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Lev Nachmanson
 */
-#include "util/vector.h"
 #include <memory>
+#include "util/vector.h"
 #include "util/lp/lp_settings.h"
 #include "util/lp/lu.h"
 #include "util/lp/sparse_matrix.hpp"