Updated script, fixed bug in QF_NIA conversion.

diff --git a/contrib/run-script-smtcomp2016 b/contrib/run-script-smtcomp2016
index 8ac8d5c1d79fcbe01b634463adbaed1dff8f8eae..534e290edefb4192af074cb6cea0e47607a73084 100644 (file)
--- a/contrib/run-script-smtcomp2016
+++ b/contrib/run-script-smtcomp2016
@@ -33,6 +33,14 @@ QF_LIA)
   # same as QF_LRA but add --pb-rewrites
   finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
   ;;
+QF_NIA)
+  trywith 20
+  trywith 1800 --solve-int-as-bv=2 --bitblast=eager
+  trywith 1800 --solve-int-as-bv=4 --bitblast=eager
+  trywith 1800 --solve-int-as-bv=8 --bitblast=eager
+  trywith 1800 --solve-int-as-bv=16 --bitblast=eager
+  finishwith --solve-int-as-bv=32 --bitblast=eager
+  ;;
 ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   # the following is designed for a run time of 2400s (40 min).
   # initial runs 1min
@@ -78,14 +86,18 @@ QF_AUFBV)
   trywith 600
   finishwith --decision=justification-stoponly
   ;;
-QF_ABV)
-  finishwith --ite-simp --simp-with-care --repeat-simp
+  trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
+  trywith 500 --arrays-weak-equiv
+  finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
+  ;;
+QF_UFBV)
+  finishwith --bitblast=eager --bv-sat-solver=cryptominisat
   ;;
 QF_BV)
   exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=1024 \
          --threads 2 \
-         --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --no-bv-abstraction' \
-         --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \
+         --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager  --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-native-xor --no-bv-abstraction' \
+         --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \
          --no-wait-to-join \
          "$bench"
   #trywith 10 --bv-eq-slicer=auto --decision=justification
@@ -93,11 +105,18 @@ QF_BV)
   #trywith 600 --decision=internal --bitblast-eager
   #finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1
   ;;
+QF_AUFLIA)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
+  ;;
+QF_AX)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
+  ;;
 QF_AUFNIA)
   finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
   ;;
-QF_AUFLIA|QF_AX)
-  finishwith --no-arrays-eager-index --arrays-eager-lemmas
+QF_ALIA)
+  trywith 70 --decision=justification --arrays-weak-equiv
+  finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 *)
   # just run the default

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 62afbf987397d7217cd68ae1a4c1d2ba508a3d49..e4b9023d5a6453f05124aa611d2ab0c3c9aa0801 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2603,8 +2603,9 @@ Node SmtEnginePrivate::intToBV(TNode n, NodeMap& cache) {
             case kind::CONST_RATIONAL: {
               Rational constant = current.getConst<Rational>();
               AlwaysAssert(constant.isIntegral());
+              AlwaysAssert(constant >= 0);
               BitVector bv(size, constant.getNumerator());
-              if (bv.getValue() != constant.getNumerator()) {
+              if (bv.toSignedInt() != constant.getNumerator()) {
                 throw TypeCheckingException(current.toExpr(), string("Not enough bits for constant in intToBV: ") + current.toString());
               }
               result = nm->mkConst(bv);

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index a04cbb58f44a9265ddf9f841524ca14cdac25ce0..4a74c1c536230f501eba616afecf9902bd131051 100644 (file)
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -338,6 +338,15 @@ public:
     return d_value;
   }
 
+  Integer toSignedInt() const {
+    // returns Integer corresponding to two's complement interpretation of bv
+    unsigned size = d_size;
+    Integer sign_bit = d_value.extractBitRange(1,size-1);
+    Integer val = d_value.extractBitRange(size-1, 0);
+    Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
+    return res;
+  }
+
   /**
    Returns k is the integer is equal to 2^{k-1} and zero
    otherwise
@@ -356,14 +365,6 @@ private:
   unsigned d_size;
   Integer d_value;
 
-  Integer toSignedInt() const {
-    // returns Integer corresponding to two's complement interpretation of bv
-    unsigned size = d_size;
-    Integer sign_bit = d_value.extractBitRange(1,size-1);
-    Integer val = d_value.extractBitRange(size-1, 0);
-    Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
-    return res;
-  }
 };/* class BitVector */