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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index ab83d3b86e96e7eb7b880320353f64b1ba820c22..3b0e072bb1e834d0eb89c5419acc7c8deef03caa 100644 (file)
--- 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 e0aedb1219c5d14fd581cd61752b0e00d6f80ee4..aa0ccac29737fd94f7c19a4f4e9ba354374235d8 100644 (file)
--- 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;
 }