From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 12 Jul 2011 06:17:00 +0000 (+0000)
Subject: Bugfix. Thanks to Jingyue Wu for reporting sbvdiv was broken through the c-api.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=393bef5c6c038988871bb615f82a656c11f3f268;p=francis%2Fstp.git

Bugfix. Thanks to Jingyue Wu for reporting sbvdiv was broken through the c-api.

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 8c96109..8f8ebeb 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -176,6 +176,12 @@ VC vc_createValidityChecker(void) {
                   bvsolver, arrayTransformer, 
                   tosat, Ctr_Example);
   
+  // This expects the simplifying node factory to be used to create all the nodes.
+  // i.e. for sbvdiv to be transformed away. The c-interface uses the hashing node
+  // factory. I tried to enable the simplfyingnode factory. But some c-api-tests
+  // failed with assertion errors.
+  bm->UserFlags.set("bitblast-simplification","0");
+
   BEEV::GlobalSTP = stp;
   decls = new BEEV::ASTVec();
   //created_exprs.clear();
diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index e5392f7..0b9fda4 100644
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -43,7 +43,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
 	g++  $(CXXFLAGS) push-pop-1.c  -o a7.out $(LIBS)
 	./a7.out
 8:
-	g++  $(CXXFLAGS)  sbvmod.c  -o a8.out $(LIBS)
+	g++  $(CXXFLAGS)  sbvdiv.c  -o a8.out $(LIBS)
 	./a8.out
 9:
 	g++  $(CXXFLAGS)  simplify.c -o a9.out $(LIBS) 
diff --git a/tests/c-api-tests/sbvdiv.c b/tests/c-api-tests/sbvdiv.c
new file mode 100644
index 0000000..b1f5dad
--- /dev/null
+++ b/tests/c-api-tests/sbvdiv.c
@@ -0,0 +1,19 @@
+#include "c_interface.h"
+#include <stdio.h>
+#include <iostream>
+
+int main() {
+    VC vc = vc_createValidityChecker();
+    vc_setFlags(vc, 'p');
+
+    Type int_type = vc_bv32Type(vc);
+    Expr zero = vc_bv32ConstExprFromInt(vc, 0);
+    Expr int_max = vc_bvConstExprFromInt(vc, 32, 0x7fffffff);
+    Expr a = vc_varExpr(vc, "a", int_type);
+    Expr b = vc_varExpr(vc, "b", int_type);
+    vc_assertFormula(vc, vc_sbvGtExpr(vc, b, zero));
+    vc_assertFormula(vc, vc_sbvLeExpr(vc, a, vc_sbvDivExpr(vc, 32,int_max, b)));
+    std::cout << vc_query(vc, vc_falseExpr(vc)) << std::endl;
+}
+
+
diff --git a/tests/c-api-tests/sbvmod.c b/tests/c-api-tests/sbvmod.c
deleted file mode 100644
index 3ab5e52..0000000
--- a/tests/c-api-tests/sbvmod.c
+++ /dev/null
@@ -1,5 +0,0 @@
-#include <stdio.h>
-main() {
- signed x = -1 % -1;
- printf("output is %i \n",x);
-}