From 119da41f6ce71ff12b1a6661992901ad5adb760c Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Tue, 29 Sep 2009 16:03:40 +0000 Subject: [PATCH] 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 --- src/c_interface/c_interface.cpp | 6 ++++-- tests/c-api-tests/Makefile | 2 +- tests/c-api-tests/biosat-rna.cpp | 2 +- 3 files changed, 6 insertions(+), 4 deletions(-) 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' -- 2.47.3