From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 29 Sep 2009 16:03:40 +0000 (+0000)
Subject: fixed bug in c_interface bvconstExprFromInt
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=119da41f6ce71ff12b1a6661992901ad5adb760c;p=francis%2Fstp.git

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 0f91179..b4a3426 100644
--- 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 1d7a2d5..01e651e 100644
--- 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 cda9e5e..dd995ca 100644
--- 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'