diff options
| -rw-r--r-- | src/theory/rep_set.cpp | 20 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/issue3689.smt2 | 10 |
3 files changed, 29 insertions, 2 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 55cef5ea7..243846b33 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -350,6 +350,7 @@ int RepSetIterator::incrementAtIndex(int i) #ifdef DISABLE_EVAL_SKIP_MULTIPLE i = (int)d_index.size()-1; #endif + Trace("rsi-debug") << "RepSetIterator::incrementAtIndex: " << i << std::endl; //increment d_index if( i>=0){ Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl; @@ -361,6 +362,7 @@ int RepSetIterator::incrementAtIndex(int i) } } if( i==-1 ){ + Trace("rsi-debug") << "increment failed" << std::endl; d_index.clear(); return -1; }else{ @@ -371,6 +373,8 @@ int RepSetIterator::incrementAtIndex(int i) } int RepSetIterator::do_reset_increment( int i, bool initial ) { + Trace("rsi-debug") << "RepSetIterator::do_reset_increment: " << i + << ", initial=" << initial << std::endl; for( unsigned ii=(i+1); ii<d_index.size(); ii++ ){ bool emptyDomain = false; int ri_res = resetIndex( ii, initial ); @@ -385,10 +389,22 @@ int RepSetIterator::do_reset_increment( int i, bool initial ) { //force next iteration if currently an empty domain if (emptyDomain) { - Trace("rsi-debug") << "This is an empty domain, increment." << std::endl; - return increment(); + Trace("rsi-debug") << "This is an empty domain (index " << ii << ")." + << std::endl; + if (ii > 0) + { + // increment at the previous index + return incrementAtIndex(ii - 1); + } + else + { + // this is the first index, we are done + d_index.clear(); + return -1; + } } } + Trace("rsi-debug") << "Finished, return " << i << std::endl; return i; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 012fde3b8..3bcdec380 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1232,6 +1232,7 @@ set(regress_1_tests regress1/fmf/issue3587.smt2 regress1/fmf/issue3615.smt2 regress1/fmf/issue3626.smt2 + regress1/fmf/issue3689.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 regress1/fmf/ko-bound-set.cvc diff --git a/test/regress/regress1/fmf/issue3689.smt2 b/test/regress/regress1/fmf/issue3689.smt2 new file mode 100644 index 000000000..83b64ba29 --- /dev/null +++ b/test/regress/regress1/fmf/issue3689.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: sat +(set-logic ALL) +(declare-sort S 0) +(declare-fun c () S) +(declare-fun b () S) +(declare-fun d (S Int) Bool) +(assert (distinct b c)) +(assert (forall ((e S) (f Int)) (=> (and (> f 1) (< f 0)) (d e f)))) +(check-sat) |