Improvement. Add the ability to set SAT solvers via the command line. Thanks to Steph...

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 62ff8779e12693f841a979f3131f37ad579bf7a8..849f131bdacff45f9ee748a93c07742f7bb5c22a 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -141,16 +141,23 @@ void vc_setFlags(VC vc, char c, int param_value) {
 }
 
 void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value) {
-  switch (f) {
+    bmstar b = (bmstar)(((stpstar)vc)->bm);
+    switch (f) {
   case EXPRDELETE:
     cinterface_exprdelete_on_flag = param_value != 0;
     break;
+  case MS:
+      b->UserFlags.solver_to_use = BEEV::UserDefinedFlags::MINISAT_SOLVER;
+      break;
+  case SMS:
+      b->UserFlags.solver_to_use = BEEV::UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER;
+      break;
   case CMS2:
-      {
-      bmstar b = (bmstar)(((stpstar)vc)->bm);
       b->UserFlags.solver_to_use = BEEV::UserDefinedFlags::CRYPTOMINISAT_SOLVER;
       break;
-      }
+  case MSP:
+      b->UserFlags.solver_to_use = BEEV::UserDefinedFlags::MINISAT_PROPAGATORS;
+      break;
   default:
     BEEV::FatalError("C_interface: vc_setInterfaceFlags: Unrecognized flag\n");
     break;

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index 19b4a2d14daf728f72b489cff870440524ade6ea..a8fd9471fc9307e3d6547b4c44044e7b81189eaa 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -58,7 +58,11 @@ extern "C" {
     the time that vc_Destroy is called, vc_Destroy will automatically
     delete them. */
     EXPRDELETE,
-    CMS2
+    MS,
+    SMS,
+    CMS2,
+    MSP
+
   };
   void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value);
 

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index d42f8973f49589fc08be330ad78713f6aa51e063..e18e2b54324681aeb1bd1ec0f1ecb18e5a2b8d87 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -14,7 +14,7 @@ else
 endif
 
 
-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 24 25
+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 24 25 26
        rm -rf *.out
 
 0:     
@@ -105,8 +105,13 @@ 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 24 25
        ./a24.out
 
 25:
-       g++ $(CXXFLAGS) -o a26.out \
+       g++ $(CXXFLAGS) -o a25.out \
          ../../lib/libstp.a stp-bool.c ../../lib/libstp.a
+       ./a25.out
+
+26:
+       g++ $(CXXFLAGS) -o a26.out \
+         ../../lib/libstp.a stp-test3.c ../../lib/libstp.a
        ./a26.out
 
 clean:

diff --git a/tests/c-api-tests/f.cvc b/tests/c-api-tests/f.cvc
new file mode 100644 (file)
index 0000000..85c743a
--- /dev/null
+++ b/tests/c-api-tests/f.cvc
@@ -0,0 +1,45 @@
+%% Regression level = 0
+%% Result = InValid
+%% Runtime = 1
+%% Language = presentation
+
+x0 : BITVECTOR(64);
+x1 : BITVECTOR(64);
+x2 : BITVECTOR(64);
+x3 : BITVECTOR(64);
+x4 : BITVECTOR(64);
+x5 : BITVECTOR(64);
+x6 : BITVECTOR(64);
+x7 : BITVECTOR(64);
+x8 : BITVECTOR(64);
+x9 : BITVECTOR(64);
+x10 : BITVECTOR(64);
+x11 : BITVECTOR(64);
+x12 : BITVECTOR(64);
+x13 : BITVECTOR(64);
+x14 : BITVECTOR(64);
+x15 : BITVECTOR(64);
+x16 : BITVECTOR(64);
+x17 : BITVECTOR(64);
+x18 : BITVECTOR(64);
+x19 : BITVECTOR(64);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000c6a), BVMULT(64,x1, 0hex0000000000000685), BVMULT(64,x2, 0hex000000000000078c), BVMULT(64,x3, 0hex00000000000005d5), BVMULT(64,x4, 0hex0000000000000809), BVMULT(64,x5, 0hex000000000000042f), BVMULT(64,x6, 0hex0000000000000d11), BVMULT(64,x7, 0hex0000000000000e32), BVMULT(64,x8, 0hex00000000000004e3), BVMULT(64,x9, 0hex0000000000000848), BVMULT(64,x10, 0hex000000000000020f), BVMULT(64,x11, 0hex00000000000005b1), BVMULT(64,x12, 0hex0000000000000f41), BVMULT(64,x13, 0hex0000000000000a8a), BVMULT(64,x14, 0hex0000000000000967), BVMULT(64,x15, 0hex0000000000000f34), BVMULT(64,x16, 0hex0000000000000eb4), BVMULT(64,x17, 0hex00000000000008a6), BVMULT(64,x18, 0hex0000000000000614), BVMULT(64,x19, 0hex00000000000005da),0hex0000000000000000) = 0hex0000000000000e43);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000264), BVMULT(64,x1, 0hex0000000000000480), BVMULT(64,x2, 0hex0000000000000ebd), BVMULT(64,x3, 0hex0000000000000118), BVMULT(64,x4, 0hex0000000000000f75), BVMULT(64,x5, 0hex00000000000002e0), BVMULT(64,x6, 0hex0000000000000ec4), BVMULT(64,x7, 0hex0000000000000691), BVMULT(64,x8, 0hex0000000000000725), BVMULT(64,x9, 0hex0000000000000836), BVMULT(64,x10, 0hex00000000000005d7), BVMULT(64,x11, 0hex0000000000000ad0), BVMULT(64,x12, 0hex0000000000000489), BVMULT(64,x13, 0hex000000000000036b), BVMULT(64,x14, 0hex000000000000029f), BVMULT(64,x15, 0hex0000000000000864), BVMULT(64,x16, 0hex0000000000000ada), BVMULT(64,x17, 0hex000000000000032a), BVMULT(64,x18, 0hex000000000000020a), BVMULT(64,x19, 0hex0000000000000ebb),0hex0000000000000000) = 0hex00000000000006e4);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000004a8), BVMULT(64,x1, 0hex00000000000001ee), BVMULT(64,x2, 0hex0000000000000cf6), BVMULT(64,x3, 0hex00000000000009b4), BVMULT(64,x4, 0hex0000000000000136), BVMULT(64,x5, 0hex0000000000000cb9), BVMULT(64,x6, 0hex0000000000000648), BVMULT(64,x7, 0hex0000000000000149), BVMULT(64,x8, 0hex000000000000014f), BVMULT(64,x9, 0hex00000000000004d0), BVMULT(64,x10, 0hex0000000000000dde), BVMULT(64,x11, 0hex0000000000000e7f), BVMULT(64,x12, 0hex00000000000005c9), BVMULT(64,x13, 0hex00000000000004f9), BVMULT(64,x14, 0hex0000000000000c4f), BVMULT(64,x15, 0hex00000000000001c0), BVMULT(64,x16, 0hex0000000000000116), BVMULT(64,x17, 0hex0000000000000a6f), BVMULT(64,x18, 0hex0000000000000e8f), BVMULT(64,x19, 0hex0000000000000222),0hex0000000000000000) = 0hex0000000000000aaf);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000d88), BVMULT(64,x1, 0hex0000000000000bc1), BVMULT(64,x2, 0hex0000000000000446), BVMULT(64,x3, 0hex0000000000000c96), BVMULT(64,x4, 0hex0000000000000655), BVMULT(64,x5, 0hex0000000000000800), BVMULT(64,x6, 0hex0000000000000d7d), BVMULT(64,x7, 0hex0000000000000b6a), BVMULT(64,x8, 0hex0000000000000650), BVMULT(64,x9, 0hex0000000000000990), BVMULT(64,x10, 0hex0000000000000028), BVMULT(64,x11, 0hex0000000000000a23), BVMULT(64,x12, 0hex0000000000000c62), BVMULT(64,x13, 0hex0000000000000ddc), BVMULT(64,x14, 0hex0000000000000bef), BVMULT(64,x15, 0hex000000000000050c), BVMULT(64,x16, 0hex0000000000000061), BVMULT(64,x17, 0hex0000000000000577), BVMULT(64,x18, 0hex0000000000000357), BVMULT(64,x19, 0hex0000000000000790),0hex0000000000000000) = 0hex0000000000000dfb);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex000000000000000b), BVMULT(64,x1, 0hex0000000000000427), BVMULT(64,x2, 0hex0000000000000d0a), BVMULT(64,x3, 0hex0000000000000c8a), BVMULT(64,x4, 0hex0000000000000446), BVMULT(64,x5, 0hex0000000000000464), BVMULT(64,x6, 0hex00000000000004d9), BVMULT(64,x7, 0hex0000000000000038), BVMULT(64,x8, 0hex0000000000000f7c), BVMULT(64,x9, 0hex0000000000000e3c), BVMULT(64,x10, 0hex00000000000007db), BVMULT(64,x11, 0hex0000000000000631), BVMULT(64,x12, 0hex000000000000011b), BVMULT(64,x13, 0hex00000000000006c7), BVMULT(64,x14, 0hex0000000000000976), BVMULT(64,x15, 0hex000000000000099f), BVMULT(64,x16, 0hex0000000000000c24), BVMULT(64,x17, 0hex00000000000001e9), BVMULT(64,x18, 0hex0000000000000872), BVMULT(64,x19, 0hex0000000000000f72),0hex0000000000000000) = 0hex00000000000009e4);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000d8d), BVMULT(64,x1, 0hex0000000000000c8d), BVMULT(64,x2, 0hex0000000000000aa3), BVMULT(64,x3, 0hex00000000000000ec), BVMULT(64,x4, 0hex00000000000005bf), BVMULT(64,x5, 0hex00000000000004a6), BVMULT(64,x6, 0hex0000000000000b3d), BVMULT(64,x7, 0hex0000000000000bdf), BVMULT(64,x8, 0hex00000000000006cd), BVMULT(64,x9, 0hex000000000000058b), BVMULT(64,x10, 0hex000000000000047b), BVMULT(64,x11, 0hex0000000000000bd3), BVMULT(64,x12, 0hex000000000000055f), BVMULT(64,x13, 0hex00000000000006f9), BVMULT(64,x14, 0hex0000000000000853), BVMULT(64,x15, 0hex000000000000092b), BVMULT(64,x16, 0hex0000000000000cc9), BVMULT(64,x17, 0hex00000000000002a0), BVMULT(64,x18, 0hex0000000000000b3c), BVMULT(64,x19, 0hex0000000000000e83),0hex0000000000000000) = 0hex0000000000000b94);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000acc), BVMULT(64,x1, 0hex000000000000011c), BVMULT(64,x2, 0hex0000000000000b65), BVMULT(64,x3, 0hex0000000000000857), BVMULT(64,x4, 0hex000000000000074a), BVMULT(64,x5, 0hex0000000000000061), BVMULT(64,x6, 0hex0000000000000625), BVMULT(64,x7, 0hex000000000000026b), BVMULT(64,x8, 0hex00000000000008ff), BVMULT(64,x9, 0hex0000000000000269), BVMULT(64,x10, 0hex0000000000000d9b), BVMULT(64,x11, 0hex00000000000001bb), BVMULT(64,x12, 0hex00000000000004c3), BVMULT(64,x13, 0hex0000000000000e33), BVMULT(64,x14, 0hex0000000000000bd5), BVMULT(64,x15, 0hex000000000000096b), BVMULT(64,x16, 0hex00000000000004ea), BVMULT(64,x17, 0hex0000000000000d61), BVMULT(64,x18, 0hex00000000000007dd), BVMULT(64,x19, 0hex00000000000004d0),0hex0000000000000000) = 0hex0000000000000146);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000c17), BVMULT(64,x1, 0hex0000000000000aa1), BVMULT(64,x2, 0hex0000000000000a81), BVMULT(64,x3, 0hex0000000000000c53), BVMULT(64,x4, 0hex00000000000004eb), BVMULT(64,x5, 0hex00000000000006ed), BVMULT(64,x6, 0hex00000000000004d8), BVMULT(64,x7, 0hex000000000000003f), BVMULT(64,x8, 0hex0000000000000632), BVMULT(64,x9, 0hex000000000000056c), BVMULT(64,x10, 0hex00000000000003c3), BVMULT(64,x11, 0hex000000000000020e), BVMULT(64,x12, 0hex0000000000000a26), BVMULT(64,x13, 0hex0000000000000690), BVMULT(64,x14, 0hex00000000000001ae), BVMULT(64,x15, 0hex000000000000023e), BVMULT(64,x16, 0hex00000000000008b0), BVMULT(64,x17, 0hex000000000000094c), BVMULT(64,x18, 0hex00000000000003e0), BVMULT(64,x19, 0hex00000000000006d0),0hex0000000000000000) = 0hex00000000000000ce);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000009d7), BVMULT(64,x1, 0hex000000000000095b), BVMULT(64,x2, 0hex0000000000000cb0), BVMULT(64,x3, 0hex0000000000000c43), BVMULT(64,x4, 0hex00000000000003e1), BVMULT(64,x5, 0hex00000000000001e1), BVMULT(64,x6, 0hex0000000000000a6e), BVMULT(64,x7, 0hex00000000000002d7), BVMULT(64,x8, 0hex0000000000000808), BVMULT(64,x9, 0hex000000000000028a), BVMULT(64,x10, 0hex0000000000000806), BVMULT(64,x11, 0hex0000000000000c80), BVMULT(64,x12, 0hex00000000000006a0), BVMULT(64,x13, 0hex0000000000000e8a), BVMULT(64,x14, 0hex0000000000000b6e), BVMULT(64,x15, 0hex0000000000000ee4), BVMULT(64,x16, 0hex00000000000002d3), BVMULT(64,x17, 0hex000000000000092b), BVMULT(64,x18, 0hex00000000000002d7), BVMULT(64,x19, 0hex00000000000006ee),0hex0000000000000000) = 0hex0000000000000abd);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000047), BVMULT(64,x1, 0hex0000000000000371), BVMULT(64,x2, 0hex00000000000002dd), BVMULT(64,x3, 0hex000000000000032e), BVMULT(64,x4, 0hex0000000000000bf7), BVMULT(64,x5, 0hex0000000000000e77), BVMULT(64,x6, 0hex000000000000029c), BVMULT(64,x7, 0hex0000000000000880), BVMULT(64,x8, 0hex0000000000000bab), BVMULT(64,x9, 0hex0000000000000678), BVMULT(64,x10, 0hex000000000000090d), BVMULT(64,x11, 0hex0000000000000bc0), BVMULT(64,x12, 0hex000000000000075e), BVMULT(64,x13, 0hex000000000000095b), BVMULT(64,x14, 0hex00000000000005dd), BVMULT(64,x15, 0hex00000000000001d0), BVMULT(64,x16, 0hex0000000000000c91), BVMULT(64,x17, 0hex00000000000007db), BVMULT(64,x18, 0hex0000000000000778), BVMULT(64,x19, 0hex000000000000040c),0hex0000000000000000) = 0hex00000000000009da);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000009c2), BVMULT(64,x1, 0hex00000000000002c4), BVMULT(64,x2, 0hex000000000000021e), BVMULT(64,x3, 0hex0000000000000139), BVMULT(64,x4, 0hex0000000000000142), BVMULT(64,x5, 0hex0000000000000cf3), BVMULT(64,x6, 0hex0000000000000072), BVMULT(64,x7, 0hex00000000000000a0), BVMULT(64,x8, 0hex000000000000009a), BVMULT(64,x9, 0hex00000000000004b5), BVMULT(64,x10, 0hex00000000000000bb), BVMULT(64,x11, 0hex0000000000000eb3), BVMULT(64,x12, 0hex00000000000005ae), BVMULT(64,x13, 0hex0000000000000d0c), BVMULT(64,x14, 0hex0000000000000976), BVMULT(64,x15, 0hex0000000000000cbc), BVMULT(64,x16, 0hex00000000000008e9), BVMULT(64,x17, 0hex00000000000004e6), BVMULT(64,x18, 0hex0000000000000466), BVMULT(64,x19, 0hex0000000000000c8c),0hex0000000000000000) = 0hex0000000000000417);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000c4c), BVMULT(64,x1, 0hex0000000000000c29), BVMULT(64,x2, 0hex0000000000000f49), BVMULT(64,x3, 0hex000000000000036b), BVMULT(64,x4, 0hex0000000000000570), BVMULT(64,x5, 0hex000000000000017f), BVMULT(64,x6, 0hex0000000000000d91), BVMULT(64,x7, 0hex0000000000000e37), BVMULT(64,x8, 0hex0000000000000197), BVMULT(64,x9, 0hex0000000000000665), BVMULT(64,x10, 0hex0000000000000f1b), BVMULT(64,x11, 0hex00000000000009f3), BVMULT(64,x12, 0hex0000000000000efd), BVMULT(64,x13, 0hex00000000000000d3), BVMULT(64,x14, 0hex0000000000000a9f), BVMULT(64,x15, 0hex00000000000007c2), BVMULT(64,x16, 0hex0000000000000a84), BVMULT(64,x17, 0hex000000000000097a), BVMULT(64,x18, 0hex000000000000014b), BVMULT(64,x19, 0hex00000000000004f8),0hex0000000000000000) = 0hex00000000000009b3);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000004bf), BVMULT(64,x1, 0hex0000000000000e2f), BVMULT(64,x2, 0hex0000000000000add), BVMULT(64,x3, 0hex0000000000000119), BVMULT(64,x4, 0hex0000000000000eb1), BVMULT(64,x5, 0hex00000000000000b2), BVMULT(64,x6, 0hex0000000000000622), BVMULT(64,x7, 0hex0000000000000c0f), BVMULT(64,x8, 0hex0000000000000ed5), BVMULT(64,x9, 0hex0000000000000559), BVMULT(64,x10, 0hex0000000000000722), BVMULT(64,x11, 0hex000000000000011d), BVMULT(64,x12, 0hex000000000000098f), BVMULT(64,x13, 0hex0000000000000a54), BVMULT(64,x14, 0hex000000000000077d), BVMULT(64,x15, 0hex0000000000000132), BVMULT(64,x16, 0hex000000000000017b), BVMULT(64,x17, 0hex00000000000001af), BVMULT(64,x18, 0hex0000000000000505), BVMULT(64,x19, 0hex0000000000000aa1),0hex0000000000000000) = 0hex0000000000000548);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000445), BVMULT(64,x1, 0hex0000000000000f69), BVMULT(64,x2, 0hex0000000000000e0b), BVMULT(64,x3, 0hex000000000000058b), BVMULT(64,x4, 0hex00000000000008fc), BVMULT(64,x5, 0hex0000000000000b15), BVMULT(64,x6, 0hex0000000000000a23), BVMULT(64,x7, 0hex0000000000000aed), BVMULT(64,x8, 0hex0000000000000ec9), BVMULT(64,x9, 0hex0000000000000b28), BVMULT(64,x10, 0hex00000000000005e3), BVMULT(64,x11, 0hex0000000000000104), BVMULT(64,x12, 0hex00000000000007ed), BVMULT(64,x13, 0hex000000000000014c), BVMULT(64,x14, 0hex0000000000000ed0), BVMULT(64,x15, 0hex0000000000000d85), BVMULT(64,x16, 0hex0000000000000c63), BVMULT(64,x17, 0hex0000000000000ae6), BVMULT(64,x18, 0hex0000000000000a43), BVMULT(64,x19, 0hex00000000000004aa),0hex0000000000000000) = 0hex00000000000008fc);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000008de), BVMULT(64,x1, 0hex0000000000000ee5), BVMULT(64,x2, 0hex0000000000000e00), BVMULT(64,x3, 0hex0000000000000aee), BVMULT(64,x4, 0hex0000000000000a5b), BVMULT(64,x5, 0hex0000000000000eee), BVMULT(64,x6, 0hex0000000000000770), BVMULT(64,x7, 0hex00000000000006e5), BVMULT(64,x8, 0hex000000000000014e), BVMULT(64,x9, 0hex0000000000000286), BVMULT(64,x10, 0hex00000000000009a1), BVMULT(64,x11, 0hex0000000000000624), BVMULT(64,x12, 0hex000000000000081d), BVMULT(64,x13, 0hex00000000000000bf), BVMULT(64,x14, 0hex0000000000000428), BVMULT(64,x15, 0hex0000000000000a8a), BVMULT(64,x16, 0hex0000000000000e38), BVMULT(64,x17, 0hex0000000000000a47), BVMULT(64,x18, 0hex00000000000003b4), BVMULT(64,x19, 0hex0000000000000af0),0hex0000000000000000) = 0hex00000000000009ee);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000000e7), BVMULT(64,x1, 0hex0000000000000e3d), BVMULT(64,x2, 0hex000000000000033d), BVMULT(64,x3, 0hex000000000000053a), BVMULT(64,x4, 0hex0000000000000cff), BVMULT(64,x5, 0hex0000000000000322), BVMULT(64,x6, 0hex0000000000000534), BVMULT(64,x7, 0hex00000000000006b3), BVMULT(64,x8, 0hex0000000000000ab4), BVMULT(64,x9, 0hex000000000000058a), BVMULT(64,x10, 0hex0000000000000154), BVMULT(64,x11, 0hex0000000000000b9d), BVMULT(64,x12, 0hex0000000000000d5b), BVMULT(64,x13, 0hex0000000000000a5b), BVMULT(64,x14, 0hex000000000000091b), BVMULT(64,x15, 0hex0000000000000f18), BVMULT(64,x16, 0hex00000000000000a5), BVMULT(64,x17, 0hex0000000000000976), BVMULT(64,x18, 0hex0000000000000b9c), BVMULT(64,x19, 0hex0000000000000585),0hex0000000000000000) = 0hex0000000000000f2a);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000ce6), BVMULT(64,x1, 0hex0000000000000c5f), BVMULT(64,x2, 0hex0000000000000b69), BVMULT(64,x3, 0hex0000000000000a54), BVMULT(64,x4, 0hex0000000000000610), BVMULT(64,x5, 0hex00000000000001a4), BVMULT(64,x6, 0hex00000000000006fd), BVMULT(64,x7, 0hex0000000000000e03), BVMULT(64,x8, 0hex0000000000000891), BVMULT(64,x9, 0hex0000000000000766), BVMULT(64,x10, 0hex0000000000000a0c), BVMULT(64,x11, 0hex0000000000000a03), BVMULT(64,x12, 0hex0000000000000e94), BVMULT(64,x13, 0hex0000000000000c12), BVMULT(64,x14, 0hex0000000000000b61), BVMULT(64,x15, 0hex0000000000000302), BVMULT(64,x16, 0hex0000000000000f4d), BVMULT(64,x17, 0hex00000000000005d8), BVMULT(64,x18, 0hex000000000000009f), BVMULT(64,x19, 0hex0000000000000b40),0hex0000000000000000) = 0hex0000000000000623);
+ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000005b8), BVMULT(64,x1, 0hex00000000000004b5), BVMULT(64,x2, 0hex000000000000036b), BVMULT(64,x3, 0hex00000000000002f7), BVMULT(64,x4, 0hex0000000000000f3c), BVMULT(64,x5, 0hex0000000000000388), BVMULT(64,x6, 0hex0000000000000ca4), BVMULT(64,x7, 0hex00000000000009c7), BVMULT(64,x8, 0hex0000000000000d63), BVMULT(64,x9, 0hex000000000000034c), BVMULT(64,x10, 0hex0000000000000b33), BVMULT(64,x11, 0hex0000000000000ddc), BVMULT(64,x12, 0hex000000000000029f), BVMULT(64,x13, 0hex0000000000000513), BVMULT(64,x14, 0hex0000000000000650), BVMULT(64,x15, 0hex00000000000004ef), BVMULT(64,x16, 0hex000000000000084b), BVMULT(64,x17, 0hex0000000000000b65), BVMULT(64,x18, 0hex0000000000000a8b), BVMULT(64,x19, 0hex0000000000000df0),0hex0000000000000000) = 0hex0000000000000ef5);
+
+QUERY FALSE;

diff --git a/tests/c-api-tests/stp-test3.c b/tests/c-api-tests/stp-test3.c
new file mode 100644 (file)
index 0000000..6b1bc32
--- /dev/null
+++ b/tests/c-api-tests/stp-test3.c
@@ -0,0 +1,32 @@
+#include <stdio.h>
+#include "c_interface.h"
+
+
+void go (enum ifaceflag_t f)
+{
+       VC vc;
+       
+
+       vc = vc_createValidityChecker ();
+       vc_setInterfaceFlags(vc, f, 0);
+       //vc_setFlags(vc,'s',0);
+
+       vc_parseExpr(vc, "f.cvc");
+
+       Expr a = vc_varExpr(vc, "a", vc_bvType(vc, 8));
+       Expr ct_0 = vc_bvConstExprFromInt(vc, 8, 0);
+
+       Expr a_eq_0 = vc_eqExpr(vc, a, ct_0);
+
+       int query = vc_query(vc, a_eq_0);
+       vc_Destroy (vc);
+}
+
+
+int main ()
+{
+       go(SMS);
+       go(MS);
+       go(CMS2);
+       go(MSP);
+}