From 035aa7a659025cadaea9181a3f99097565265767 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 11 Feb 2013 12:31:52 +0000
Subject: [PATCH] Fix c-api parsing of CVC strings. Thanks to Ryan Govostes for
 reporting.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1669 e59a4935-1847-0410-ae03-e826735625c1
---
 src/c_interface/c_interface.cpp               |  3 +-
 .../parsestring-using-cinterface.c            | 31 +++++++++++++++++++
 2 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index ab83d3b..3b0e072 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -1838,6 +1838,7 @@ extern void smt_switch_to_buffer (YY_BUFFER_STATE new_buffer  );
 #endif
 
 int smt_scan_string(const char *yy_str);
+int cvc_scan_string(const char *yy_str);
 
 int vc_parseMemExpr(VC vc, const char* s, Expr* oquery, Expr* oasserts ) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
@@ -1867,7 +1868,7 @@ int vc_parseMemExpr(VC vc, const char* s, Expr* oquery, Expr* oasserts ) {
     {
       //YY_BUFFER_STATE bstat = cvc_scan_string(s);
       //cvc_switch_to_buffer(bstat);
-      smt_scan_string(s);
+      cvc_scan_string(s);
       cvcparse((void*)&AssertsQuery);
       //cvc_delete_buffer(bstat);
     }
diff --git a/tests/c-api-tests/parsestring-using-cinterface.c b/tests/c-api-tests/parsestring-using-cinterface.c
index e0aedb1..aa0ccac 100644
--- a/tests/c-api-tests/parsestring-using-cinterface.c
+++ b/tests/c-api-tests/parsestring-using-cinterface.c
@@ -1,7 +1,36 @@
 #include <stdio.h>
 #include "c_interface.h"
 
+int CVC_PARSE() {
+  VC vc = vc_createValidityChecker();
+  vc_setFlags(vc,'n');
+  vc_setFlags(vc,'d');
+  vc_setFlags(vc,'p');
+
+  Expr q;
+  Expr asserts;
+
+  
+  const char* s =       "QUERY BVMOD(2,0bin10,0bin10) = 0bin00;\n";
+
+  vc_parseMemExpr(vc,s,&q,&asserts); 
+  
+  vc_printExpr(vc, q);
+  vc_printExpr(vc, asserts);
+  printf("\n");
+
+  vc_DeleteExpr(q);
+  vc_DeleteExpr(asserts);
+  vc_Destroy(vc);
+  return 0;
+}
+
+
+
+
 int main() {
+  CVC_PARSE();
+
   VC vc = vc_createValidityChecker();
   vc_setFlags(vc,'n');
   vc_setFlags(vc,'d');
@@ -24,6 +53,8 @@ int main() {
   vc_printExpr(vc, asserts);
   printf("\n");
 
+  vc_DeleteExpr(q);
+  vc_DeleteExpr(asserts);
   vc_Destroy(vc);
   return 0;
 }
-- 
2.47.3