fixed bug in c_interface bvconstExprFromInt

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 0f911797e5a2d84691a46c196f83d5909f250835..b4a342688cc37b8e18c72e4a508856b1a594ba5b 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -857,9 +857,11 @@ Expr vc_bvConstExprFromInt(VC vc,
   bmstar b = (bmstar)vc;
 
   unsigned long long int v = (unsigned long long int)value;
-  if(v > (unsigned long long)(1 << n_bits)-1) {
+  unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits;
+  //printf("%ull", max_n_bits);
+  if(v > max_n_bits) {
     printf("CInterface: vc_bvConstExprFromInt: "\
-          "You are trying to construct an constant %llu >= 2 ^ %d,\n", v, n_bits);
+          "You are trying to construct a constant %llu >= %d,\n", v, max_n_bits);
     BEEV::FatalError("FatalError");
   }
   node n = b->CreateBVConst(n_bits, v);

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 1d7a2d5a5601e056b5f6022366c6790c4dbc29c6..01e651ebdb28b58ad40cfa18897f43a79df3aa4b 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -65,7 +65,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19
 
 19:
        g++  -g $(CXXFLAGS)  biosat-rna.cpp  -lstp -o biosat.out
-       time ./biosat.out AUUGGUAUGUAAGCUACUUCUUCCAGUAGCUGCGUCAUAACAUCAAGGUUAUGCAUACUGAGCCGAAGCUCAGCUUCGGUCCUCCAAGGAAGACCA 800
+       ./biosat.out AUUGGUAUGUAAGCUACUUCUUCCAAGACCA 800
 
 
 clean:

diff --git a/tests/c-api-tests/biosat-rna.cpp b/tests/c-api-tests/biosat-rna.cpp
index cda9e5e3f702982d35a30aa7e92dc2c4cc6ca4b4..dd995caa75383010b84d6ceb7a61e4b1c9abaaf4 100644 (file)
--- a/tests/c-api-tests/biosat-rna.cpp
+++ b/tests/c-api-tests/biosat-rna.cpp
@@ -125,7 +125,7 @@ int main(int argc, char** argv) {
   //inputs: the RNA sequence
   char * seq  = argv[1];
   int seq_len = strlen(seq);
-  printf("The sequence length is : %d \n", seq_len);
+  //printf("The sequence length is : %d \n", seq_len);
 
   //inputs: STP needs to find a sequence whose energy is greater than
   //'energy_bound'