Testcase and temporary bugfix for an interface problem reported by Alvin Cheung.

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

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index f4a05d03b1775ec7e8ad1f395b79c67abfa55c64..2a30c27c0127ff9ececc0f02c29cd3e45ffeb942 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -321,61 +321,64 @@ extern "C" {
 
   //Kinds of Expr
   enum exprkind_t{
-    UNDEFINED,
-    SYMBOL,
-    BVCONST,
-    BVNEG,
-    BVCONCAT,
-    BVOR,
-    BVAND,
-    BVXOR,
-    BVNAND,
-    BVNOR,
-    BVXNOR,
-    BVEXTRACT,
-    BVLEFTSHIFT,
-    BVRIGHTSHIFT,
-    BVSRSHIFT,
-    BVVARSHIFT,
-    BVPLUS,
-    BVSUB,
-    BVUMINUS,
-    BVMULTINVERSE,
-    BVMULT,
-    BVDIV,
-    BVMOD,
-    SBVDIV,
-    SBVREM,
-    BVSX,
-    BOOLVEC,
-    ITE,
-    BVGETBIT,
-    BVLT,
-    BVLE,
-    BVGT,
-    BVGE,
-    BVSLT,
-    BVSLE,
-    BVSGT,
-    BVSGE,
-    EQ,
-    NEQ,
-    FALSE,
-    TRUE,
-    NOT,
-    AND,
-    OR,
-    NAND,
-    NOR,
-    XOR,
-    IFF,
-    IMPLIES,
-    READ,
-    WRITE,
-    ARRAY,
-    BITVECTOR,
-    BOOLEAN,
-  };
+      UNDEFINED,
+      SYMBOL,
+      BVCONST,
+      BVNEG,
+      BVCONCAT,
+      BVOR,
+      BVAND,
+      BVXOR,
+      BVNAND,
+      BVNOR,
+      BVXNOR,
+      BVEXTRACT,
+      BVLEFTSHIFT,
+      BVRIGHTSHIFT,
+      BVSRSHIFT,
+      BVVARSHIFT,
+      BVPLUS,
+      BVSUB,
+      BVUMINUS,
+      BVMULTINVERSE,
+      BVMULT,
+      BVDIV,
+      BVMOD,
+      SBVDIV,
+      SBVREM,
+      SBVMOD,
+      BVSX,
+      BVZX,
+      BOOLVEC,
+      ITE,
+      BVGETBIT,
+      BVLT,
+      BVLE,
+      BVGT,
+      BVGE,
+      BVSLT,
+      BVSLE,
+      BVSGT,
+      BVSGE,
+      EQ,
+      FALSE,
+      TRUE,
+      NOT,
+      AND,
+      OR,
+      NAND,
+      NOR,
+      XOR,
+      IFF,
+      IMPLIES,
+      FOR,
+      PARAMBOOL,
+      READ,
+      WRITE,
+      ARRAY,
+      BITVECTOR,
+      BOOLEAN,
+  } ;
 
   // type of expression
   enum type_t {

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 23c3da0e14312265486b751c98bbeeb248d4bf5b..56d6ba0583e52f9847772593017d601839d15c90 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -82,5 +82,9 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20
        g++  -g $(CXXFLAGS)  leak.c  -o a20.out $(LIBS)
        $(VALGRIND) ./a20.out
 
+21:    
+       g++ $(CXXFLAGS) interface-check.c -o a21.out $(LIBS)
+       ./a21.out
+
 clean:
        rm -rf *~ *.out

diff --git a/tests/c-api-tests/interface-check.c b/tests/c-api-tests/interface-check.c
new file mode 100644 (file)
index 0000000..07c52dd
--- /dev/null
+++ b/tests/c-api-tests/interface-check.c
@@ -0,0 +1,24 @@
+// Bug reported by Alvin Cheung. Thanks.
+
+#include "c_interface.h"
+#include <iostream>
+#include <cassert>
+#include <stdexcept>
+
+int main(int argc, char * argv [])
+{
+  ::VC vc = vc_createValidityChecker();
+  ::Expr b1 = ::vc_trueExpr(vc);
+  ::Expr b2 = ::vc_falseExpr(vc);
+  ::Expr andExpr = ::vc_andExpr(vc, b1, b2);
+
+  if(::getExprKind(andExpr) !=  ::AND )
+       throw new std::runtime_error("sadfas");
+
+  ::Expr simplifiedExpr = ::vc_simplify(vc, andExpr);
+
+       if (getExprKind(simplifiedExpr) !=  ::FALSE )
+       throw new std::runtime_error("sa22dfas");
+  return 0;
+}
+