From 4a6ea0c54e2f2a2ac0f95640731a230352cabdc1 Mon Sep 17 00:00:00 2001
From: khooyp <khooyp@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 11 Jan 2012 16:55:46 +0000
Subject: [PATCH] Add a C API test for the leak fixed in r1141 (when
 pushing/popping assertions), enabling valgrind on this test as well as
 another similar test.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1500 e59a4935-1847-0410-ae03-e826735625c1
---
 tests/c-api-tests/Makefile      |  8 +++++--
 tests/c-api-tests/push-no-pop.c | 41 +++++++++++++++++++++++++++++++++
 2 files changed, 47 insertions(+), 2 deletions(-)
 create mode 100644 tests/c-api-tests/push-no-pop.c

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 98bf6a8..11df111 100644
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -14,7 +14,7 @@ else
 endif
 
 
-all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
+all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
 	rm -rf *.out
 
 0:	
@@ -71,7 +71,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 2
 	./a16.out
 17:
 	g++  $(CXXFLAGS)  push-pop.c -o a17.out $(LIBS)
-	./a17.out
+	$(VALGRIND) ./a17.out
 18:
 	g++  $(CXXFLAGS)  cvc-to-c.cpp  -o a18.out $(LIBS)
 	#./a18.out ./t.cvc
@@ -119,5 +119,9 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 2
          ../../lib/libstp.a stp-array-model.c ../../lib/libstp.a
 	./a27.out
 
+28:
+	g++ $(CXXFLAGS) push-no-pop.c -o a28.out $(LIBS)
+	$(VALGRIND) ./a28.out
+
 clean:
 	rm -rf *~ *.out *.dSYM
diff --git a/tests/c-api-tests/push-no-pop.c b/tests/c-api-tests/push-no-pop.c
new file mode 100644
index 0000000..daca81f
--- /dev/null
+++ b/tests/c-api-tests/push-no-pop.c
@@ -0,0 +1,41 @@
+/* g++ -I$(HOME)/stp/c_interface push-no-pop.c -L$(HOME)/lib -lstp -o cc*/
+
+#include <stdio.h>
+#include "c_interface.h"
+
+int main() {
+  VC vc = vc_createValidityChecker();
+  vc_setFlags(vc,'n');
+  vc_setFlags(vc,'d');
+  vc_setFlags(vc,'p');
+  //vc_setFlags(vc,'v');
+  //vc_setFlags(vc,'s');
+
+  Type bv8 = vc_bvType(vc, 8);
+
+  Expr a = vc_varExpr(vc, "a", bv8);
+  Expr ct_0 = vc_bvConstExprFromInt(vc, 8, 0);
+
+  Expr a_eq_0 = vc_eqExpr(vc, a, ct_0);
+
+  int query = vc_query(vc, a_eq_0);
+  printf("query = %d\n", query);
+
+  Expr a_neq_0 = vc_notExpr(vc,a_eq_0);
+  vc_assertFormula(vc,a_eq_0);
+  vc_push(vc);
+
+  Expr queryexp = vc_eqExpr(vc, a, vc_bvConstExprFromInt(vc, 8, 0));
+
+  query = vc_query(vc, queryexp);
+  vc_printCounterExample(vc);
+  printf("query = %d\n", query);
+
+  vc_DeleteExpr(queryexp);
+  vc_DeleteExpr(a_neq_0);
+  vc_DeleteExpr(a_eq_0);
+  vc_DeleteExpr(a);
+
+  vc_Destroy(vc);
+}
+
-- 
2.47.3