Incremental support for bv_to_int (#4967)

This PR adds support for incremental solving in bv_to_int.
This amounts to:

using context dependent data structures
adding a test
In addition, we check for parametrized operations in a more robust way (using kind::metakind::PARAMETERIZED) and rename some tests for convenience.

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index bb0bde2f975d1418dfb8df71093f5f7bb8b5245b..04131211361527c57029a87ac1aeb24235311c69 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -108,7 +108,7 @@ Node BVToInt::makeBinary(Node n)
       d_binarizeCache[current] = Node();
       toVisit.insert(toVisit.end(), current.begin(), current.end());
     }
-    else if (d_binarizeCache[current].isNull())
+    else if (d_binarizeCache[current].get().isNull())
     {
       /*
        * We already visited the sub-dag rooted at the current node,
@@ -137,14 +137,13 @@ Node BVToInt::makeBinary(Node n)
       {
         // current has children, but we do not binarize it
         NodeBuilder<> builder(k);
-        if (current.getKind() == kind::BITVECTOR_EXTRACT
-            || current.getKind() == kind::APPLY_UF)
+        if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
         {
           builder << current.getOperator();
         }
         for (Node child : current)
         {
-          builder << d_binarizeCache[child];
+          builder << d_binarizeCache[child].get();
         }
         d_binarizeCache[current] = builder.constructNode();
       }
@@ -186,6 +185,7 @@ Node BVToInt::eliminationPass(Node n)
         (d_rebuildCache.find(current) != d_rebuildCache.end());
     if (!inEliminationCache)
     {
+      // current is not the elimination of any previously-visited node
       // current hasn't been eliminated yet.
       // eliminate operators from it
       Node currentEliminated =
@@ -221,7 +221,7 @@ Node BVToInt::eliminationPass(Node n)
     if (inRebuildCache)
     {
       // current was already added to the rebuild cache.
-      if (d_rebuildCache[current].isNull())
+      if (d_rebuildCache[current].get().isNull())
       {
         // current wasn't rebuilt yet.
         uint64_t numChildren = current.getNumChildren();
@@ -235,8 +235,7 @@ Node BVToInt::eliminationPass(Node n)
           // The main operator is replaced, and the children
           // are replaced with their eliminated counterparts.
           NodeBuilder<> builder(current.getKind());
-          if (current.getKind() == kind::BITVECTOR_EXTRACT
-              || current.getKind() == kind::APPLY_UF)
+          if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
           {
             builder << current.getOperator();
           }
@@ -245,8 +244,8 @@ Node BVToInt::eliminationPass(Node n)
             Assert(d_eliminationCache.find(child) != d_eliminationCache.end());
             Node eliminatedChild = d_eliminationCache[child];
             Assert(d_rebuildCache.find(eliminatedChild) != d_eliminationCache.end());
-            Assert(!d_rebuildCache[eliminatedChild].isNull());
-            builder << d_rebuildCache[eliminatedChild];
+            Assert(!d_rebuildCache[eliminatedChild].get().isNull());
+            builder << d_rebuildCache[eliminatedChild].get();
           }
           d_rebuildCache[current] = builder.constructNode();
         }
@@ -256,7 +255,7 @@ Node BVToInt::eliminationPass(Node n)
   Assert(d_eliminationCache.find(n) != d_eliminationCache.end());
   Node eliminated = d_eliminationCache[n];
   Assert(d_rebuildCache.find(eliminated) != d_rebuildCache.end());
-  Assert(!d_rebuildCache[eliminated].isNull());
+  Assert(!d_rebuildCache[eliminated].get().isNull());
   return d_rebuildCache[eliminated];
 }
 
@@ -270,6 +269,7 @@ Node BVToInt::bvToInt(Node n)
   vector<Node> toVisit;
   toVisit.push_back(n);
   uint64_t granularity = options::BVAndIntegerGranularity();
+  Assert(0 <= granularity && granularity <= 8);
 
   while (!toVisit.empty())
   {
@@ -284,7 +284,7 @@ Node BVToInt::bvToInt(Node n)
     else
     {
       // We already visited this node
-      if (!d_bvToIntCache[current].isNull())
+      if (!d_bvToIntCache[current].get().isNull())
       {
         // We are done computing the translation for current
         toVisit.pop_back();
@@ -643,7 +643,7 @@ Node BVToInt::bvToInt(Node n)
               Assert(d_bvToIntCache.find(a) != d_bvToIntCache.end());
               Assert(i >= j);
               Node div = d_nm->mkNode(
-                  kind::INTS_DIVISION_TOTAL, d_bvToIntCache[a], pow2(j));
+                  kind::INTS_DIVISION_TOTAL, d_bvToIntCache[a].get(), pow2(j));
               d_bvToIntCache[current] = modpow2(div, i - j + 1);
               break;
             }
@@ -814,7 +814,7 @@ bool BVToInt::childrenTypesChanged(Node n) {
   bool result = false;
   for (Node child : n) {
     TypeNode originalType = child.getType();
-    TypeNode newType = d_bvToIntCache[child].getType();
+    TypeNode newType = d_bvToIntCache[child].get().getType();
     if (! newType.isSubtypeOf(originalType)) {
       result = true;
       break;
@@ -825,10 +825,11 @@ bool BVToInt::childrenTypesChanged(Node n) {
 
 BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bv-to-int"),
-      d_binarizeCache(),
-      d_eliminationCache(),
-      d_bvToIntCache(),
-      d_rangeAssertions()
+      d_binarizeCache(preprocContext->getUserContext()),
+      d_eliminationCache(preprocContext->getUserContext()),
+      d_rebuildCache(preprocContext->getUserContext()),
+      d_bvToIntCache(preprocContext->getUserContext()),
+      d_rangeAssertions(preprocContext->getUserContext())
 {
   d_nm = NodeManager::currentNM();
   d_zero = d_nm->mkConst<Rational>(0);
@@ -838,7 +839,6 @@ BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult BVToInt::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  AlwaysAssert(!options::incrementalSolving());
   for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i)
   {
     Node bvNode = (*assertionsToPreprocess)[i];
@@ -857,7 +857,11 @@ void BVToInt::addFinalizeRangeAssertions(
     AssertionPipeline* assertionsToPreprocess)
 {
   vector<Node> vec_range;
-  vec_range.assign(d_rangeAssertions.begin(), d_rangeAssertions.end());
+  vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end());
+  if (vec_range.size() == 0)
+  {
+    return;
+  }
   if (vec_range.size() == 1)
   {
     assertionsToPreprocess->push_back(vec_range[0]);

diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index 5015d1e8efb3e85518878eeb83e333375de8093c..d8ee698792f0a4ce91e82be4cdd34bf733436f40 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -62,6 +62,9 @@
 #ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
 #define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
 
+#include "context/cdhashmap.h"
+#include "context/cdo.h"
+#include "context/context.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 
@@ -69,7 +72,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
-using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
 
 class BVToInt : public PreprocessingPass
 {
@@ -245,10 +248,10 @@ class BVToInt : public PreprocessingPass
   /**
    * Caches for the different functions
    */
-  NodeMap d_binarizeCache;
-  NodeMap d_eliminationCache;
-  NodeMap d_rebuildCache;
-  NodeMap d_bvToIntCache;
+  CDNodeMap d_binarizeCache;
+  CDNodeMap d_eliminationCache;
+  CDNodeMap d_rebuildCache;
+  CDNodeMap d_bvToIntCache;
 
   /**
    * Node manager that is used throughout the pass
@@ -259,7 +262,7 @@ class BVToInt : public PreprocessingPass
    * A set of constraints of the form 0 <= x < 2^k
    * These are added for every new integer variable that we introduce.
    */
-  unordered_set<Node, NodeHashFunction> d_rangeAssertions;
+  context::CDHashSet<Node, NodeHashFunction> d_rangeAssertions;
 
   /**
    * Useful constants

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 7d2427015f2fc205df10a75d96b9450effcc7cb1..130f758943b7faea703d463ff6a190fff83af2be 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -151,14 +151,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
-    // not compatible with incremental
-    if (options::incrementalSolving())
-    {
-      throw OptionException(
-          "solving bitvectors as integers is currently not supported "
-          "when solving incrementally.");
-    }
-    else if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+    if (options::boolToBitvector() != options::BoolToBVMode::OFF)
     {
       throw OptionException(
           "solving bitvectors as integers is incompatible with --bool-to-bv.");

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7a1366b3a9f31e54c11af7c6253bb4d7735da9ba..0caeafb36120c38f830bc7d1a5a70eb98618b791 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -213,11 +213,11 @@ set(regress_0_tests
   regress0/bv/bv_to_int_bvmul1.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
   regress0/bv/bv_to_int_bitwise.smt2
+  regress0/bv/bv_to_int_bvuf_to_intuf.smt2
+  regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
+  regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_elim_err.smt2
   regress0/bv/bv_to_int_zext.smt2
-  regress0/bv/bvuf_to_intuf.smt2
-  regress0/bv/bvuf_to_intuf_smtlib.smt2
-  regress0/bv/bvuf_to_intuf_sorts.smt2
   regress0/bv/bv2nat-ground-c.smt2
   regress0/bv/bv2nat-simp-range.smt2
   regress0/bv/bvmul-pow2-only.smt2
@@ -2075,6 +2075,7 @@ set(regress_2_tests
   regress2/bug812.smt2
   regress2/bv/opStructure_MBA_6.scrambled.min.smt2
   regress2/bv_to_int_ashr.smt2
+  regress2/bv_to_int_inc1.smt2
   regress2/bv_to_int_mask_array_1.smt2
   regress2/bv_to_int_mask_array_2.smt2
   regress2/bv_to_int_shifts.smt2

diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
new file mode 100644 (file)
index 0000000..c621aa1
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_UFBV)
+(declare-fun a () (_ BitVec 4))
+(declare-fun b () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4) )
+(assert (distinct (bvadd a b) (f a)))
+(check-sat)

diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
new file mode 100644 (file)
index 0000000..6196b2b
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
@@ -0,0 +1,81 @@
+;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores
+;EXPECT: unsat
+
+(set-logic QF_UFBV)
+(declare-fun z$n0s32 () (_ BitVec 32))
+(declare-fun dataOut () (_ BitVec 32))
+(declare-fun z$2 () (_ BitVec 1))
+(declare-fun stageOne () (_ BitVec 32))
+(declare-fun z$4 () (_ BitVec 1))
+(declare-fun stageTwo () (_ BitVec 32))
+(declare-fun z$6 () (_ BitVec 1))
+(declare-fun tmp_stageOne () (_ BitVec 32))
+(declare-fun z$8 () (_ BitVec 1))
+(declare-fun tmp_stageTwo () (_ BitVec 32))
+(declare-fun z$10 () (_ BitVec 1))
+(declare-fun reset_ () (_ BitVec 1))
+(declare-fun z$14 () (_ BitVec 1))
+(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
+(declare-fun z$15 () (_ BitVec 32))
+(declare-fun z$17 () (_ BitVec 32))
+(declare-fun dataOut$next () (_ BitVec 32))
+(declare-fun z$19 () (_ BitVec 1))
+(declare-fun c1 () (_ BitVec 32))
+(declare-fun dataIn () (_ BitVec 32))
+(declare-fun z$23 () (_ BitVec 32))
+(declare-fun stageOne$next () (_ BitVec 32))
+(declare-fun z$25 () (_ BitVec 1))
+(declare-fun c2 () (_ BitVec 32))
+(declare-fun z$28 () (_ BitVec 32))
+(declare-fun stageTwo$next () (_ BitVec 32))
+(declare-fun z$30 () (_ BitVec 1))
+(declare-fun tmp_stageOne$next () (_ BitVec 32))
+(declare-fun z$32 () (_ BitVec 1))
+(declare-fun tmp_stageTwo$next () (_ BitVec 32))
+(declare-fun z$34 () (_ BitVec 1))
+(declare-fun z$35 () (_ BitVec 1))
+(declare-fun z$55 () (_ BitVec 32))
+(declare-fun z$57 () (_ BitVec 1))
+(declare-fun z$58 () (_ BitVec 1))
+(declare-fun z$59 () (_ BitVec 1))
+(declare-fun prop$next () (_ BitVec 1))
+(declare-fun z$61 () (_ BitVec 1))
+(declare-fun z$54 () (_ BitVec 1))
+(declare-fun z$63 () (_ BitVec 1))
+(assert
+ (= z$15 (Add_32_32_32 stageTwo stageOne)))
+(assert
+ (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32)))
+(assert
+ (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1))))
+
+ 
+(assert
+ (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1))))
+(assert
+ (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1)))))
+ (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1)))))
+(assert
+ (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next)))
+(assert
+ (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
+(assert
+ (let (($x52 (= z$2 (_ bv1 1))))
+ (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1)))))
+ (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1))))))
+(assert
+ (= z$63 (_ bv1 1)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
new file mode 100644 (file)
index 0000000..8fbe96e
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_UFBV)
+(declare-sort S 0)
+(declare-fun s () S)
+(declare-fun a () (_ BitVec 4))
+(declare-fun b () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4) )
+(declare-fun g (S) (_ BitVec 4))
+(declare-fun h ((_ BitVec 4)) S)
+(assert (distinct (bvadd a b) (f a)))
+(assert (distinct (f a) (g s)))
+(assert (distinct (h a) s))
+(check-sat)

diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bvuf_to_intuf.smt2
deleted file mode 100644 (file)
index c621aa1..0000000
--- a/test/regress/regress0/bv/bvuf_to_intuf.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
-; EXPECT: sat
-(set-logic QF_UFBV)
-(declare-fun a () (_ BitVec 4))
-(declare-fun b () (_ BitVec 4))
-(declare-fun f ((_ BitVec 4)) (_ BitVec 4) )
-(assert (distinct (bvadd a b) (f a)))
-(check-sat)

diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
deleted file mode 100644 (file)
index 6196b2b..0000000
--- a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
+++ /dev/null
@@ -1,81 +0,0 @@
-;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores
-;EXPECT: unsat
-
-(set-logic QF_UFBV)
-(declare-fun z$n0s32 () (_ BitVec 32))
-(declare-fun dataOut () (_ BitVec 32))
-(declare-fun z$2 () (_ BitVec 1))
-(declare-fun stageOne () (_ BitVec 32))
-(declare-fun z$4 () (_ BitVec 1))
-(declare-fun stageTwo () (_ BitVec 32))
-(declare-fun z$6 () (_ BitVec 1))
-(declare-fun tmp_stageOne () (_ BitVec 32))
-(declare-fun z$8 () (_ BitVec 1))
-(declare-fun tmp_stageTwo () (_ BitVec 32))
-(declare-fun z$10 () (_ BitVec 1))
-(declare-fun reset_ () (_ BitVec 1))
-(declare-fun z$14 () (_ BitVec 1))
-(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
-(declare-fun z$15 () (_ BitVec 32))
-(declare-fun z$17 () (_ BitVec 32))
-(declare-fun dataOut$next () (_ BitVec 32))
-(declare-fun z$19 () (_ BitVec 1))
-(declare-fun c1 () (_ BitVec 32))
-(declare-fun dataIn () (_ BitVec 32))
-(declare-fun z$23 () (_ BitVec 32))
-(declare-fun stageOne$next () (_ BitVec 32))
-(declare-fun z$25 () (_ BitVec 1))
-(declare-fun c2 () (_ BitVec 32))
-(declare-fun z$28 () (_ BitVec 32))
-(declare-fun stageTwo$next () (_ BitVec 32))
-(declare-fun z$30 () (_ BitVec 1))
-(declare-fun tmp_stageOne$next () (_ BitVec 32))
-(declare-fun z$32 () (_ BitVec 1))
-(declare-fun tmp_stageTwo$next () (_ BitVec 32))
-(declare-fun z$34 () (_ BitVec 1))
-(declare-fun z$35 () (_ BitVec 1))
-(declare-fun z$55 () (_ BitVec 32))
-(declare-fun z$57 () (_ BitVec 1))
-(declare-fun z$58 () (_ BitVec 1))
-(declare-fun z$59 () (_ BitVec 1))
-(declare-fun prop$next () (_ BitVec 1))
-(declare-fun z$61 () (_ BitVec 1))
-(declare-fun z$54 () (_ BitVec 1))
-(declare-fun z$63 () (_ BitVec 1))
-(assert
- (= z$15 (Add_32_32_32 stageTwo stageOne)))
-(assert
- (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32)))
-(assert
- (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1))))
-
- 
-(assert
- (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1))))
-(assert
- (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1)))))
- (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1)))))
-(assert
- (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next)))
-(assert
- (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
-(assert
- (let (($x52 (= z$2 (_ bv1 1))))
- (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1)))))
- (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1))))))
-(assert
- (= z$63 (_ bv1 1)))
-(check-sat)
-(exit)

diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
deleted file mode 100644 (file)
index 8fbe96e..0000000
--- a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
+++ /dev/null
@@ -1,14 +0,0 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
-; EXPECT: sat
-(set-logic QF_UFBV)
-(declare-sort S 0)
-(declare-fun s () S)
-(declare-fun a () (_ BitVec 4))
-(declare-fun b () (_ BitVec 4))
-(declare-fun f ((_ BitVec 4)) (_ BitVec 4) )
-(declare-fun g (S) (_ BitVec 4))
-(declare-fun h ((_ BitVec 4)) S)
-(assert (distinct (bvadd a b) (f a)))
-(assert (distinct (f a) (g s)))
-(assert (distinct (h a) s))
-(check-sat)

diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2
new file mode 100644 (file)
index 0000000..0d09a72
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_inc1.smt2
@@ -0,0 +1,30 @@
+; COMMAND-LINE: --incremental --solve-bv-as-int=sum
+; EXPECT sat
+; EXPECT sat
+; EXPECT unsat
+; EXPECT sat
+(set-logic QF_BV)
+(set-option :incremental true)
+(declare-fun a () (_ BitVec 3))
+(declare-fun b () (_ BitVec 3))
+(declare-fun c () (_ BitVec 3))
+
+(assert (bvult a (bvand b c)))
+(check-sat)
+; EXPECT: sat
+
+(push 1)
+(assert (bvult c b))
+(check-sat)
+; EXPECT: sat
+
+
+(push 1)
+(assert (bvugt c b))
+(check-sat)
+; EXPECT: unsat
+(pop 2)
+
+(check-sat)
+; EXPECT: sat
+(exit)