From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 16 May 2012 18:20:09 +0000 (+0000)
Subject: Fixing C compatibility library (it still had a reference to CONST_INTEGER).
X-Git-Tag: cvc5-1.0.0~8162
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5212180d05110bbec3ed76e70e985d317ff450c5;p=cvc5.git

Fixing C compatibility library (it still had a reference to CONST_INTEGER).

This hopefully fixes the Debian build.
---

diff --git a/src/bindings/compat/c/c_interface.cpp b/src/bindings/compat/c/c_interface.cpp
index 6a8a98547..d4f287dd7 100644
--- a/src/bindings/compat/c/c_interface.cpp
+++ b/src/bindings/compat/c/c_interface.cpp
@@ -29,6 +29,7 @@
 //#include "vc_cmd.h"
 //#include "theory_bitvector.h"
 //#include "fdstream.h"
+#include <string.h>
 #include <assert.h>
 
 
@@ -2042,20 +2043,20 @@ extern "C" Expr vc_bvWriteToMemoryArray(VC vc,
   DebugAssert(numOfBytes > 0,
 	      "numOfBytes must be greater than 0");
 
-  int newBitsPerElem = numOfBytes*8;
+  //int newBitsPerElem = numOfBytes*8;
   if(numOfBytes == 1)
     return vc_writeExpr(vc, array, byteIndex, element);
   else {
     int count = 1;
-    int hi = newBitsPerElem - 1;
-    int low = newBitsPerElem - 8;
+    //int hi = newBitsPerElem - 1;
+    //int low = newBitsPerElem - 8;
     int low_elem = 0;
     int hi_elem = low_elem + 7;
     Expr c = vc_bvExtract(vc, element, hi_elem, low_elem);
     Expr newarray = vc_writeExpr(vc, array, byteIndex, c);
     while(--numOfBytes > 0) {
-      hi = low-1;
-      low = low-8;
+      //hi = low-1;
+      //low = low-8;
 
       low_elem = low_elem + 8;
       hi_elem = low_elem + 7;
@@ -2825,11 +2826,7 @@ extern "C" int vc_getKindInt(VC vc,char* kind_name)
 extern "C" int vc_getInt(Expr e){
   try{
     CVC3::Expr ex = fromExpr(e);
-    if(ex.getKind() == CVC4::kind::CONST_INTEGER) {
-      return int(ex.getConst<CVC3::Integer>().getLong());
-    } else {
-      return int(ex.getConst<CVC3::Rational>().getNumerator().getLong());
-    }
+    return int(ex.getConst<CVC3::Rational>().getNumerator().getLong());
   } catch (CVC3::Exception ex){
     signal_error("vc_getInt",error_int,ex);
     return error_int;