]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commitdiff
Fix regresscapi. This file wasn't checked in
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 14 Jun 2010 03:04:47 +0000 (03:04 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 14 Jun 2010 03:04:47 +0000 (03:04 +0000)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@841 e59a4935-1847-0410-ae03-e826735625c1

tests/c-api-tests/parsestring-using-cinterface.c [new file with mode: 0644]

diff --git a/tests/c-api-tests/parsestring-using-cinterface.c b/tests/c-api-tests/parsestring-using-cinterface.c
new file mode 100644 (file)
index 0000000..3d4129e
--- /dev/null
@@ -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);
+}
+