From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 14 Jun 2010 03:04:47 +0000 (+0000)
Subject: Fix regresscapi. This file wasn't checked in
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b4f3ba7f3415e715d27ef57407bad5337a8353bc;p=francis%2Fstp.git

Fix regresscapi. This file wasn't checked in

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@841 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/tests/c-api-tests/parsestring-using-cinterface.c b/tests/c-api-tests/parsestring-using-cinterface.c
new file mode 100644
index 0000000..3d4129e
--- /dev/null
+++ b/tests/c-api-tests/parsestring-using-cinterface.c
@@ -0,0 +1,29 @@
+#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,'m');
+
+  Expr q;
+  Expr asserts;
+
+  
+  const char* s =       "(benchmark fg.smt\n"
+			":logic QF_AUFBV\n"
+			":extrafuns ((x_32 BitVec[32]))\n"
+			":extrafuns ((y32 BitVec[32]))\n"
+			":assumption true\n)\n";
+
+  vc_parseMemExpr(vc,s,&q,&asserts); 
+  
+  vc_printExpr(vc, q);
+  vc_printExpr(vc, asserts);
+  printf("\n");
+
+  vc_Destroy(vc);
+}
+