Fix bug 516; include some bug testcases.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b72f520920a49d79176129c098f80de778bfd426..2cddc29cf9a5f9f5b09ee5069ddbe9dcf1b11275 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3541,6 +3541,12 @@ void SmtEngine::checkModel(bool hardFailure) {
     Debug("boolean-terms") << "++ got " << n << endl;
     Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
 
+    if(Theory::theoryOf(n) != THEORY_REWRITERULES) {
+      // In case it's a quantifier (or contains one), look up its value before
+      // simplifying, or the quantifier might be irreparably altered.
+      n = m->getValue(n);
+    }
+
     // Simplify the result.
     n = d_private->simplify(n);
     Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
@@ -3562,6 +3568,7 @@ void SmtEngine::checkModel(bool hardFailure) {
     // but don't show up in our substitution map above.
     n = m->getValue(n);
     Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl;
+    AlwaysAssert(n.isConst() || n.getKind() == kind::LAMBDA);
 
     // The result should be == true.
     if(n != NodeManager::currentNM()->mkConst(true)) {

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 75187b7bd3312e2cc720e3b0ec3a89ab2841541f..234b137c8adbc0e564a16c45b64076984232aaaf 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -28,7 +28,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 
 TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) :
-  d_substitutions(c), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
+  d_substitutions(c, false), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
@@ -48,14 +48,13 @@ void TheoryModel::reset(){
   d_uf_models.clear();
 }
 
-Node TheoryModel::getValue( TNode n ) const{
+Node TheoryModel::getValue(TNode n) const {
   //apply substitutions
-  Node nn = d_substitutions.apply( n );
+  Node nn = d_substitutions.apply(n);
   //get value in model
-  nn = getModelValue( nn );
+  nn = getModelValue(nn);
   //normalize
   nn = Rewriter::rewrite(nn);
-  Assert(nn.isConst() || nn.getKind() == kind::LAMBDA);
   return nn;
 }
 
@@ -97,8 +96,10 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     // no good.  Instead, return the quantifier itself.  If we're in
     // checkModel(), and the quantifier actually matters, we'll get an
     // assert-fail since the quantifier isn't a constant.
-    if(!d_equalityEngine.hasTerm(n)) {
+    if(!d_equalityEngine.hasTerm(Rewriter::rewrite(n))) {
       return n;
+    } else {
+      n = Rewriter::rewrite(n);
     }
   } else {
     if(n.getKind() == kind::LAMBDA) {

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index b1c15c73af5ec9e81b0c21946d6551d2f52b47e8..92574d5a69e626140893af6316e0ea1c14506280 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -144,11 +144,16 @@ BUG_TESTS = \
        bug507.smt2 \
        bug512.smt2 \
        bug512.minimized.smt2 \
-       bug519.smt2
+       bug516.smt2 \
+       bug519.smt2 \
+       bug520.smt2 \
+       bug522.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
+       bug521.smt2 \
+       bug521.minimized.smt2 \
        simplification_bug4.smt2.expect \
        bug216.smt2.expect
 

diff --git a/test/regress/regress0/bug516.smt2 b/test/regress/regress0/bug516.smt2
new file mode 100644 (file)
index 0000000..b5f5d49
--- /dev/null
+++ b/test/regress/regress0/bug516.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --finite-model-find --fmf-bound-int
+; EXPECT: sat
+; EXIT: 10
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :incremental true)
+(declare-fun P (Int) Bool)
+(declare-fun ten () Int)
+
+(assert (forall ((x Int)) (=> (<= 1 x ten) (P x))))
+
+(push)
+(assert (= ten 10))
+
+(check-sat)
+(pop)

diff --git a/test/regress/regress0/bug520.smt2 b/test/regress/regress0/bug520.smt2
new file mode 100644 (file)
index 0000000..4bdb968
--- /dev/null
+++ b/test/regress/regress0/bug520.smt2
@@ -0,0 +1,173 @@
+; Automatically generated by SBV. Do not edit.
+(set-option :produce-models true)
+(set-logic QF_UFBV)
+(set-info :status sat)
+; --- uninterpreted sorts ---
+; --- literal constants ---
+(define-fun s_2 () Bool false)
+(define-fun s_1 () Bool true)
+(define-fun s77 () (_ BitVec 8) #x00)
+(define-fun s78 () (_ BitVec 8) #x04)
+(define-fun s81 () (_ BitVec 8) #x01)
+(define-fun s83 () (_ BitVec 8) #xff)
+; --- skolem constants ---
+(declare-fun s0 () (_ BitVec 8))
+(declare-fun s1 () (_ BitVec 8))
+(declare-fun s2 () (_ BitVec 8))
+(declare-fun s3 () Bool)
+(declare-fun s4 () (_ BitVec 8))
+(declare-fun s5 () Bool)
+(declare-fun s6 () (_ BitVec 8))
+(declare-fun s7 () Bool)
+(declare-fun s8 () (_ BitVec 8))
+(declare-fun s9 () Bool)
+(declare-fun s10 () (_ BitVec 8))
+(declare-fun s11 () Bool)
+(declare-fun s12 () (_ BitVec 8))
+(declare-fun s13 () Bool)
+(declare-fun s14 () (_ BitVec 8))
+(declare-fun s15 () Bool)
+(declare-fun s16 () (_ BitVec 8))
+(declare-fun s17 () Bool)
+(declare-fun s18 () (_ BitVec 8))
+(declare-fun s19 () Bool)
+(declare-fun s20 () (_ BitVec 8))
+(declare-fun s21 () Bool)
+(declare-fun s22 () (_ BitVec 8))
+(declare-fun s23 () Bool)
+(declare-fun s24 () (_ BitVec 8))
+(declare-fun s25 () Bool)
+(declare-fun s26 () (_ BitVec 8))
+(declare-fun s27 () Bool)
+(declare-fun s28 () (_ BitVec 8))
+(declare-fun s29 () Bool)
+(declare-fun s30 () (_ BitVec 8))
+(declare-fun s31 () Bool)
+(declare-fun s32 () (_ BitVec 8))
+(declare-fun s33 () Bool)
+(declare-fun s34 () (_ BitVec 8))
+(declare-fun s35 () Bool)
+(declare-fun s36 () (_ BitVec 8))
+(declare-fun s37 () Bool)
+(declare-fun s38 () (_ BitVec 8))
+(declare-fun s39 () Bool)
+(declare-fun s40 () (_ BitVec 8))
+(declare-fun s41 () Bool)
+(declare-fun s42 () (_ BitVec 8))
+; --- constant tables ---
+; --- skolemized tables ---
+(declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))
+(declare-fun table1 ((_ BitVec 8)) Bool)
+(declare-fun table2 ((_ BitVec 8)) (_ BitVec 8))
+(declare-fun table3 ((_ BitVec 8)) Bool)
+; --- arrays ---
+; --- uninterpreted constants ---
+; --- user given axioms ---
+; --- formula ---
+(assert ; no quantifiers
+   (let ((s43 (and s3 s5)))
+   (let ((s44 (or s3 s5)))
+   (let ((s45 (not s44)))
+   (let ((s46 (= (bvcomp s4 s6) #b1)))
+   (let ((s47 (and s45 s46)))
+   (let ((s48 (or s43 s47)))
+   (let ((s49 (and s11 s13)))
+   (let ((s50 (or s11 s13)))
+   (let ((s51 (not s50)))
+   (let ((s52 (= (bvcomp s12 s14) #b1)))
+   (let ((s53 (and s51 s52)))
+   (let ((s54 (or s49 s53)))
+   (let ((s55 (and s19 s21)))
+   (let ((s56 (or s19 s21)))
+   (let ((s57 (not s56)))
+   (let ((s58 (= (bvcomp s20 s22) #b1)))
+   (let ((s59 (and s57 s58)))
+   (let ((s60 (or s55 s59)))
+   (let ((s61 (and s27 s29)))
+   (let ((s62 (or s27 s29)))
+   (let ((s63 (not s62)))
+   (let ((s64 (= (bvcomp s28 s30) #b1)))
+   (let ((s65 (and s63 s64)))
+   (let ((s66 (or s61 s65)))
+   (let ((s67 (and s35 s37)))
+   (let ((s68 (or s35 s37)))
+   (let ((s69 (not s68)))
+   (let ((s70 (= (bvcomp s36 s38) #b1)))
+   (let ((s71 (and s69 s70)))
+   (let ((s72 (or s67 s71)))
+   (let ((s73 (and s66 s72)))
+   (let ((s74 (and s60 s73)))
+   (let ((s75 (and s54 s74)))
+   (let ((s76 (and s48 s75)))
+   (let ((s79 (bvurem s0 s78)))
+   (let ((s80 (not (= (bvcomp s77 s79) #b1))))
+   (let ((s82 (ite s80 s81 s77)))
+   (let ((s84 (= (bvcomp s82 s83) #b1)))
+   (let ((s85 (bvadd s78 s79)))
+   (let ((s86 (ite s84 s85 s79)))
+   (let ((s87 (ite (bvule #x04 s86) s77 (table0 s86))))
+   (let ((s88 (= (bvcomp s8 s87) #b1)))
+   (let ((s89 (ite (bvule #x04 s86) s_2 (table1 s86))))
+   (let ((s90 (= s7 s89)))
+   (let ((s91 (ite (bvule #x04 s86) s77 (table2 s86))))
+   (let ((s92 (= (bvcomp s10 s91) #b1)))
+   (let ((s93 (ite (bvule #x04 s86) s_2 (table3 s86))))
+   (let ((s94 (= s9 s93)))
+   (let ((s95 (and s92 s94)))
+   (let ((s96 (and s90 s95)))
+   (let ((s97 (and s88 s96)))
+   (let ((s98 (and s7 s9)))
+   (let ((s99 (or s7 s9)))
+   (let ((s100 (not s99)))
+   (let ((s101 (= (bvcomp s8 s10) #b1)))
+   (let ((s102 (and s100 s101)))
+   (let ((s103 (or s98 s102)))
+   (let ((s104 (and s15 s17)))
+   (let ((s105 (or s15 s17)))
+   (let ((s106 (not s105)))
+   (let ((s107 (= (bvcomp s16 s18) #b1)))
+   (let ((s108 (and s106 s107)))
+   (let ((s109 (or s104 s108)))
+   (let ((s110 (and s23 s25)))
+   (let ((s111 (or s23 s25)))
+   (let ((s112 (not s111)))
+   (let ((s113 (= (bvcomp s24 s26) #b1)))
+   (let ((s114 (and s112 s113)))
+   (let ((s115 (or s110 s114)))
+   (let ((s116 (and s31 s33)))
+   (let ((s117 (or s31 s33)))
+   (let ((s118 (not s117)))
+   (let ((s119 (= (bvcomp s32 s34) #b1)))
+   (let ((s120 (and s118 s119)))
+   (let ((s121 (or s116 s120)))
+   (let ((s122 (and s39 s41)))
+   (let ((s123 (or s39 s41)))
+   (let ((s124 (not s123)))
+   (let ((s125 (= (bvcomp s40 s42) #b1)))
+   (let ((s126 (and s124 s125)))
+   (let ((s127 (or s122 s126)))
+   (let ((s128 (and s121 s127)))
+   (let ((s129 (and s115 s128)))
+   (let ((s130 (and s109 s129)))
+   (let ((s131 (and s103 s130)))
+   (let ((s132 (not s131)))
+   (let ((s133 (and s97 s132)))
+   (let ((s134 (and s76 s133)))
+   (and (= (table0 #x00) s12)
+        (= (table0 #x01) s20)
+        (= (table0 #x02) s28)
+        (= (table0 #x03) s36)
+        (= (table1 #x00) s11)
+        (= (table1 #x01) s19)
+        (= (table1 #x02) s27)
+        (= (table1 #x03) s35)
+        (= (table2 #x00) s14)
+        (= (table2 #x01) s22)
+        (= (table2 #x02) s30)
+        (= (table2 #x03) s38)
+        (= (table3 #x00) s13)
+        (= (table3 #x01) s21)
+        (= (table3 #x02) s29)
+        (= (table3 #x03) s37)
+        s134))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)

diff --git a/test/regress/regress0/bug521.minimized.smt2 b/test/regress/regress0/bug521.minimized.smt2
new file mode 100644 (file)
index 0000000..6751d40
--- /dev/null
+++ b/test/regress/regress0/bug521.minimized.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun _substvar_301_ () Bool)
+(declare-fun _substvar_300_ () Bool)
+(declare-fun group_size_x () (_ BitVec 32))
+(declare-fun _WRITE_OFFSET_$$p$1@1 () (_ BitVec 32))
+(declare-fun inline$_LOG_WRITE_$$p$1$_offset$1@0 () (_ BitVec 32))
+(declare-fun _WRITE_OFFSET_$$p$1@0 () (_ BitVec 32))
+(declare-fun group_id_x$1 () (_ BitVec 32))
+(declare-fun local_id_x$1 () (_ BitVec 32))
+(declare-fun inline$_LOG_WRITE_$$p$0$_offset$1@0 () (_ BitVec 32))
+(define-fun $foo () Bool (=> true (let ((inline$_LOG_WRITE_$$p$1$_LOG_WRITE_correct (=> true (=> true (=> (= _WRITE_OFFSET_$$p$1@1 (ite _substvar_300_ inline$_LOG_WRITE_$$p$1$_offset$1@0 _WRITE_OFFSET_$$p$1@0)) false))))) (let ((inline$_LOG_WRITE_$$p$1$Entry_correct (=> true (=> (= inline$_LOG_WRITE_$$p$1$_offset$1@0 (bvadd (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1) #x00000001)) (=> true inline$_LOG_WRITE_$$p$1$_LOG_WRITE_correct))))) (let ((inline$$bugle_barrier$0$anon1_Else_correct (=> true (=> true (=> true inline$_LOG_WRITE_$$p$1$Entry_correct))))) (let ((inline$$bugle_barrier$0$Entry_correct (=> true (and _substvar_301_ (=> true (=> true inline$$bugle_barrier$0$anon1_Else_correct)))))) (let (($0$1_correct (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true inline$$bugle_barrier$0$Entry_correct)))))))))))) (let ((inline$_LOG_WRITE_$$p$0$_LOG_WRITE_correct (=> true (=> true (=> (= _WRITE_OFFSET_$$p$1@0 inline$_LOG_WRITE_$$p$0$_offset$1@0) $0$1_correct))))) (let ((inline$_LOG_WRITE_$$p$0$Entry_correct (=> true (=> (= inline$_LOG_WRITE_$$p$0$_offset$1@0 (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1)) (=> true inline$_LOG_WRITE_$$p$0$_LOG_WRITE_correct))))) (let (($0_correct (=> true (=> true (=> true inline$_LOG_WRITE_$$p$0$Entry_correct))))) $0_correct))))))))))
+(assert (not (=> true $foo)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/bug521.smt2 b/test/regress/regress0/bug521.smt2
new file mode 100644 (file)
index 0000000..47b73e8
--- /dev/null
+++ b/test/regress/regress0/bug521.smt2
@@ -0,0 +1,322 @@
+(set-option :produce-unsat-cores true)
+(set-option :print-success false)
+(set-info :smt-lib-version 2.0)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-logic ALL_SUPPORTED)
+; done setting options
+
+; Boogie universal background predicate
+; Copyright (c) 2004-2010, Microsoft Corp.
+(set-info :category "industrial")
+(declare-sort |T@U| 0)
+(declare-sort |T@T| 0)
+(declare-fun real_pow (Real Real) Real)
+(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
+(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)
+
+(declare-fun group_size_y () (_ BitVec 32))
+(declare-fun group_size_z () (_ BitVec 32))
+(declare-fun num_groups_y () (_ BitVec 32))
+(declare-fun num_groups_z () (_ BitVec 32))
+(declare-fun group_size_x () (_ BitVec 32))
+(declare-fun num_groups_x () (_ BitVec 32))
+(declare-fun ControlFlow (Int Int) Int)
+(declare-fun %lbl%+1458 () Bool)
+(declare-fun %lbl%@3203 () Bool)
+(declare-fun _WRITE_HAS_OCCURRED_$$p$1@2 () Bool)
+(declare-fun _WRITE_SOURCE_$$p$1@2 () (_ BitVec 32))
+(declare-fun %lbl%@3213 () Bool)
+(declare-fun _READ_HAS_OCCURRED_$$p$1 () Bool)
+(declare-fun _READ_SOURCE_$$p$1 () (_ BitVec 32))
+(declare-fun %lbl%@3225 () Bool)
+(declare-fun %lbl%@3240 () Bool)
+(declare-fun %lbl%+1440 () Bool)
+(declare-fun $mv_state (Int Int) Bool)
+(declare-fun $mv_state_const () Int)
+(declare-fun call465formal@_offset$2@0 () (_ BitVec 32))
+(declare-fun group_id_x$2 () (_ BitVec 32))
+(declare-fun local_id_x$2 () (_ BitVec 32))
+(declare-fun call465formal@_value$2@0 () (_ BitVec 32))
+(declare-fun %lbl%@3060 () Bool)
+(declare-fun _WRITE_HAS_OCCURRED_$$p$1@1 () Bool)
+(declare-fun _WRITE_OFFSET_$$p$1@1 () (_ BitVec 32))
+(declare-fun _WRITE_VALUE_$$p$1@1 () (_ BitVec 32))
+(declare-fun %lbl%@3078 () Bool)
+(declare-fun _READ_OFFSET_$$p$1 () (_ BitVec 32))
+(declare-fun _READ_VALUE_$$p$1 () (_ BitVec 32))
+(declare-fun %lbl%@3099 () Bool)
+(declare-fun _WRITE_SOURCE_$$p$1@1 () (_ BitVec 32))
+(declare-fun %lbl%@3109 () Bool)
+(declare-fun %lbl%@3121 () Bool)
+(declare-fun %lbl%@3136 () Bool)
+(declare-fun %lbl%+1434 () Bool)
+(declare-fun inline$_LOG_WRITE_$$p$1$track@1 () Bool)
+(declare-fun _WRITE_HAS_OCCURRED_$$p$1@0 () Bool)
+(declare-fun inline$_LOG_WRITE_$$p$1$_offset$1@0 () (_ BitVec 32))
+(declare-fun _WRITE_OFFSET_$$p$1@0 () (_ BitVec 32))
+(declare-fun inline$_LOG_WRITE_$$p$1$_value$1@0 () (_ BitVec 32))
+(declare-fun _WRITE_VALUE_$$p$1@0 () (_ BitVec 32))
+(declare-fun _WRITE_SOURCE_$$p$1@0 () (_ BitVec 32))
+(declare-fun %lbl%+1432 () Bool)
+(declare-fun group_id_x$1 () (_ BitVec 32))
+(declare-fun local_id_x$1 () (_ BitVec 32))
+(declare-fun %lbl%+1328 () Bool)
+(declare-fun group_id_y$1 () (_ BitVec 32))
+(declare-fun group_id_y$2 () (_ BitVec 32))
+(declare-fun group_id_z$1 () (_ BitVec 32))
+(declare-fun group_id_z$2 () (_ BitVec 32))
+(declare-fun %lbl%+1330 () Bool)
+(declare-fun %lbl%+1324 () Bool)
+(declare-fun %lbl%@2798 () Bool)
+(declare-fun %lbl%+1334 () Bool)
+(declare-fun call397formal@_offset$2@0 () (_ BitVec 32))
+(declare-fun call397formal@_value$2@0 () (_ BitVec 32))
+(declare-fun %lbl%@2667 () Bool)
+(declare-fun %lbl%@2685 () Bool)
+(declare-fun %lbl%@2706 () Bool)
+(declare-fun %lbl%@2716 () Bool)
+(declare-fun %lbl%@2728 () Bool)
+(declare-fun %lbl%@2743 () Bool)
+(declare-fun %lbl%+1189 () Bool)
+(declare-fun inline$_LOG_WRITE_$$p$0$track@1 () Bool)
+(declare-fun _WRITE_HAS_OCCURRED_$$p$1 () Bool)
+(declare-fun inline$_LOG_WRITE_$$p$0$_offset$1@0 () (_ BitVec 32))
+(declare-fun _WRITE_OFFSET_$$p$1 () (_ BitVec 32))
+(declare-fun inline$_LOG_WRITE_$$p$0$_value$1@0 () (_ BitVec 32))
+(declare-fun _WRITE_VALUE_$$p$1 () (_ BitVec 32))
+(declare-fun _WRITE_SOURCE_$$p$1 () (_ BitVec 32))
+(declare-fun %lbl%+1187 () Bool)
+(declare-fun %lbl%+1462 () Bool)
+(declare-fun local_id_y$1 () (_ BitVec 32))
+(declare-fun local_id_y$2 () (_ BitVec 32))
+(declare-fun local_id_z$1 () (_ BitVec 32))
+(declare-fun local_id_z$2 () (_ BitVec 32))
+(assert (not (= (ite (= group_size_y #x00000001) #b1 #b0) #b0)))
+(assert (not (= (ite (= group_size_z #x00000001) #b1 #b0) #b0)))
+(assert (not (= (ite (= num_groups_y #x00000001) #b1 #b0) #b0)))
+(assert (not (= (ite (= num_groups_z #x00000001) #b1 #b0) #b0)))
+(assert (not (= (ite (= group_size_x #x00000400) #b1 #b0) #b0)))
+(assert (not (= (ite (= num_groups_x #x00000400) #b1 #b0) #b0)))
+(define-fun $foo () Bool (=> (= (ControlFlow 0 0) 1462) (let ((GeneratedUnifiedExit_correct (=> (and %lbl%+1458 true) (and
+(or %lbl%@3203 (=> (= (ControlFlow 0 1458) (- 0 3203)) (=> (not _WRITE_HAS_OCCURRED_$$p$1@2) (= _WRITE_SOURCE_$$p$1@2 #x00000000))))
+(=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@2) (= _WRITE_SOURCE_$$p$1@2 #x00000000)) (and
+(or %lbl%@3213 (=> (= (ControlFlow 0 1458) (- 0 3213)) (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000))))
+(=> (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)) (and
+(or %lbl%@3225 (=> (= (ControlFlow 0 1458) (- 0 3225)) (=> _WRITE_HAS_OCCURRED_$$p$1@2 (or
+(= _WRITE_SOURCE_$$p$1@2 #x00000001)
+(= _WRITE_SOURCE_$$p$1@2 #x00000002)))))
+(=> (=> _WRITE_HAS_OCCURRED_$$p$1@2 (or
+(= _WRITE_SOURCE_$$p$1@2 #x00000001)
+(= _WRITE_SOURCE_$$p$1@2 #x00000002))) (and
+(or %lbl%@3240 (=> (= (ControlFlow 0 1458) (- 0 3240)) (=> _READ_HAS_OCCURRED_$$p$1 false)))
+(=> (=> _READ_HAS_OCCURRED_$$p$1 false) true)))))))))))
+(let (($0$3_correct (=> (and %lbl%+1440 true) (=> (and
+($mv_state $mv_state_const 1)
+true
+(= call465formal@_offset$2@0 (bvadd (bvadd (bvmul group_size_x group_id_x$2) local_id_x$2) #x00000001))
+(= call465formal@_value$2@0 (bvadd (bvmul group_size_x group_id_x$2) local_id_x$2))) (and
+(or %lbl%@3060 (=> (= (ControlFlow 0 1440) (- 0 3060)) (not (and
+true
+_WRITE_HAS_OCCURRED_$$p$1@1
+(= _WRITE_OFFSET_$$p$1@1 call465formal@_offset$2@0)
+(not (= _WRITE_VALUE_$$p$1@1 call465formal@_value$2@0))))))
+(=> (not (and
+true
+_WRITE_HAS_OCCURRED_$$p$1@1
+(= _WRITE_OFFSET_$$p$1@1 call465formal@_offset$2@0)
+(not (= _WRITE_VALUE_$$p$1@1 call465formal@_value$2@0)))) (and
+(or %lbl%@3078 (=> (= (ControlFlow 0 1440) (- 0 3078)) (not (and
+true
+_READ_HAS_OCCURRED_$$p$1
+(= _READ_OFFSET_$$p$1 call465formal@_offset$2@0)
+(not (= _READ_VALUE_$$p$1 call465formal@_value$2@0))))))
+(=> (not (and
+true
+_READ_HAS_OCCURRED_$$p$1
+(= _READ_OFFSET_$$p$1 call465formal@_offset$2@0)
+(not (= _READ_VALUE_$$p$1 call465formal@_value$2@0)))) (and
+(or %lbl%@3099 (=> (= (ControlFlow 0 1440) (- 0 3099)) (=> (not _WRITE_HAS_OCCURRED_$$p$1@1) (= _WRITE_SOURCE_$$p$1@1 #x00000000))))
+(=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@1) (= _WRITE_SOURCE_$$p$1@1 #x00000000)) (and
+(or %lbl%@3109 (=> (= (ControlFlow 0 1440) (- 0 3109)) (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000))))
+(=> (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)) (and
+(or %lbl%@3121 (=> (= (ControlFlow 0 1440) (- 0 3121)) (=> _WRITE_HAS_OCCURRED_$$p$1@1 (or
+(= _WRITE_SOURCE_$$p$1@1 #x00000001)
+(= _WRITE_SOURCE_$$p$1@1 #x00000002)))))
+(=> (=> _WRITE_HAS_OCCURRED_$$p$1@1 (or
+(= _WRITE_SOURCE_$$p$1@1 #x00000001)
+(= _WRITE_SOURCE_$$p$1@1 #x00000002))) (and
+(or %lbl%@3136 (=> (= (ControlFlow 0 1440) (- 0 3136)) (=> _READ_HAS_OCCURRED_$$p$1 false)))
+(=> (=> _READ_HAS_OCCURRED_$$p$1 false) (=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@1) (= _WRITE_SOURCE_$$p$1@1 #x00000000)) (=> (and
+(=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000))
+(=> _WRITE_HAS_OCCURRED_$$p$1@1 (or
+(= _WRITE_SOURCE_$$p$1@1 #x00000001)
+(= _WRITE_SOURCE_$$p$1@1 #x00000002)))) (=> (and
+(=> _READ_HAS_OCCURRED_$$p$1 false)
+(= _WRITE_HAS_OCCURRED_$$p$1@2 _WRITE_HAS_OCCURRED_$$p$1@1)
+(= _WRITE_SOURCE_$$p$1@2 _WRITE_SOURCE_$$p$1@1)
+(= (ControlFlow 0 1440) 1458)) GeneratedUnifiedExit_correct)))))))))))))))))))
+(let ((inline$_LOG_WRITE_$$p$1$_LOG_WRITE_correct (=> (and %lbl%+1434 true) (=> (= _WRITE_HAS_OCCURRED_$$p$1@1 (ite (and
+true
+inline$_LOG_WRITE_$$p$1$track@1) true _WRITE_HAS_OCCURRED_$$p$1@0)) (=> (and
+(= _WRITE_OFFSET_$$p$1@1 (ite (and
+true
+inline$_LOG_WRITE_$$p$1$track@1) inline$_LOG_WRITE_$$p$1$_offset$1@0 _WRITE_OFFSET_$$p$1@0))
+(= _WRITE_VALUE_$$p$1@1 (ite (and
+true
+inline$_LOG_WRITE_$$p$1$track@1) inline$_LOG_WRITE_$$p$1$_value$1@0 _WRITE_VALUE_$$p$1@0))
+(= _WRITE_SOURCE_$$p$1@1 (ite (and
+true
+inline$_LOG_WRITE_$$p$1$track@1) #x00000002 _WRITE_SOURCE_$$p$1@0))
+(= (ControlFlow 0 1434) 1440)) $0$3_correct)))))
+(let ((inline$_LOG_WRITE_$$p$1$Entry_correct (=> (and %lbl%+1432 true) (=> (= inline$_LOG_WRITE_$$p$1$_offset$1@0 (bvadd (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1) #x00000001)) (=> (and
+(= inline$_LOG_WRITE_$$p$1$_value$1@0 (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1))
+(= (ControlFlow 0 1432) 1434)) inline$_LOG_WRITE_$$p$1$_LOG_WRITE_correct)))))
+(let ((inline$$bugle_barrier$0$anon1_Else_correct (=> (and %lbl%+1328 true) (=> (=> (and
+(= group_id_x$1 group_id_x$2)
+(= group_id_y$1 group_id_y$2)
+(= group_id_z$1 group_id_z$2)) (=> (= #b1 #b1) (not _READ_HAS_OCCURRED_$$p$1))) (=> (and
+(=> (and
+(= group_id_x$1 group_id_x$2)
+(= group_id_y$1 group_id_y$2)
+(= group_id_z$1 group_id_z$2)) (=> (= #b1 #b1) (not _WRITE_HAS_OCCURRED_$$p$1@0)))
+(= (ControlFlow 0 1328) 1432)) inline$_LOG_WRITE_$$p$1$Entry_correct)))))
+(let ((inline$$bugle_barrier$0$anon1_Then_correct (=> (and %lbl%+1330 true) true)))
+(let ((inline$$bugle_barrier$0$Entry_correct (=> (and %lbl%+1324 true) (and
+(or %lbl%@2798 (=> (= (ControlFlow 0 1324) (- 0 2798)) (=> (and
+(= group_id_x$1 group_id_x$2)
+(= group_id_y$1 group_id_y$2)
+(= group_id_z$1 group_id_z$2)) (= true true))))
+(=> (=> (and
+(= group_id_x$1 group_id_x$2)
+(= group_id_y$1 group_id_y$2)
+(= group_id_z$1 group_id_z$2)) (= true true)) (and
+(=> (= (ControlFlow 0 1324) 1330) inline$$bugle_barrier$0$anon1_Then_correct)
+(=> (= (ControlFlow 0 1324) 1328) inline$$bugle_barrier$0$anon1_Else_correct)))))))
+(let (($0$1_correct (=> (and %lbl%+1334 true) (=> (and
+($mv_state $mv_state_const 0)
+true
+(= call397formal@_offset$2@0 (bvadd (bvmul group_size_x group_id_x$2) local_id_x$2))
+(= call397formal@_value$2@0 (bvadd (bvmul group_size_x group_id_x$2) local_id_x$2))) (and
+(or %lbl%@2667 (=> (= (ControlFlow 0 1334) (- 0 2667)) (not (and
+true
+_WRITE_HAS_OCCURRED_$$p$1@0
+(= _WRITE_OFFSET_$$p$1@0 call397formal@_offset$2@0)
+(not (= _WRITE_VALUE_$$p$1@0 call397formal@_value$2@0))))))
+(=> (not (and
+true
+_WRITE_HAS_OCCURRED_$$p$1@0
+(= _WRITE_OFFSET_$$p$1@0 call397formal@_offset$2@0)
+(not (= _WRITE_VALUE_$$p$1@0 call397formal@_value$2@0)))) (and
+(or %lbl%@2685 (=> (= (ControlFlow 0 1334) (- 0 2685)) (not (and
+true
+_READ_HAS_OCCURRED_$$p$1
+(= _READ_OFFSET_$$p$1 call397formal@_offset$2@0)
+(not (= _READ_VALUE_$$p$1 call397formal@_value$2@0))))))
+(=> (not (and
+true
+_READ_HAS_OCCURRED_$$p$1
+(= _READ_OFFSET_$$p$1 call397formal@_offset$2@0)
+(not (= _READ_VALUE_$$p$1 call397formal@_value$2@0)))) (and
+(or %lbl%@2706 (=> (= (ControlFlow 0 1334) (- 0 2706)) (=> (not _WRITE_HAS_OCCURRED_$$p$1@0) (= _WRITE_SOURCE_$$p$1@0 #x00000000))))
+(=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@0) (= _WRITE_SOURCE_$$p$1@0 #x00000000)) (and
+(or %lbl%@2716 (=> (= (ControlFlow 0 1334) (- 0 2716)) (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000))))
+(=> (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)) (and
+(or %lbl%@2728 (=> (= (ControlFlow 0 1334) (- 0 2728)) (=> _WRITE_HAS_OCCURRED_$$p$1@0 (or
+(= _WRITE_SOURCE_$$p$1@0 #x00000001)
+(= _WRITE_SOURCE_$$p$1@0 #x00000002)))))
+(=> (=> _WRITE_HAS_OCCURRED_$$p$1@0 (or
+(= _WRITE_SOURCE_$$p$1@0 #x00000001)
+(= _WRITE_SOURCE_$$p$1@0 #x00000002))) (and
+(or %lbl%@2743 (=> (= (ControlFlow 0 1334) (- 0 2743)) (=> _READ_HAS_OCCURRED_$$p$1 false)))
+(=> (=> _READ_HAS_OCCURRED_$$p$1 false) (=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@0) (= _WRITE_SOURCE_$$p$1@0 #x00000000)) (=> (and
+(=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000))
+(=> _WRITE_HAS_OCCURRED_$$p$1@0 (or
+(= _WRITE_SOURCE_$$p$1@0 #x00000001)
+(= _WRITE_SOURCE_$$p$1@0 #x00000002)))
+(=> _READ_HAS_OCCURRED_$$p$1 false)
+(= (ControlFlow 0 1334) 1324)) inline$$bugle_barrier$0$Entry_correct))))))))))))))))))
+(let ((inline$_LOG_WRITE_$$p$0$_LOG_WRITE_correct (=> (and %lbl%+1189 true) (=> (= _WRITE_HAS_OCCURRED_$$p$1@0 (ite (and
+true
+inline$_LOG_WRITE_$$p$0$track@1) true _WRITE_HAS_OCCURRED_$$p$1)) (=> (and
+(= _WRITE_OFFSET_$$p$1@0 (ite (and
+true
+inline$_LOG_WRITE_$$p$0$track@1) inline$_LOG_WRITE_$$p$0$_offset$1@0 _WRITE_OFFSET_$$p$1))
+(= _WRITE_VALUE_$$p$1@0 (ite (and
+true
+inline$_LOG_WRITE_$$p$0$track@1) inline$_LOG_WRITE_$$p$0$_value$1@0 _WRITE_VALUE_$$p$1))
+(= _WRITE_SOURCE_$$p$1@0 (ite (and
+true
+inline$_LOG_WRITE_$$p$0$track@1) #x00000001 _WRITE_SOURCE_$$p$1))
+(= (ControlFlow 0 1189) 1334)) $0$1_correct)))))
+(let ((inline$_LOG_WRITE_$$p$0$Entry_correct (=> (and %lbl%+1187 true) (=> (= inline$_LOG_WRITE_$$p$0$_offset$1@0 (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1)) (=> (and
+(= inline$_LOG_WRITE_$$p$0$_value$1@0 (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1))
+(= (ControlFlow 0 1187) 1189)) inline$_LOG_WRITE_$$p$0$_LOG_WRITE_correct)))))
+(let (($0_correct (=> (and %lbl%+1462 true) (=> (and
+(not _READ_HAS_OCCURRED_$$p$1)
+(not _WRITE_HAS_OCCURRED_$$p$1)
+(= _READ_SOURCE_$$p$1 #x00000000)
+(= _WRITE_SOURCE_$$p$1 #x00000000)
+(bvsgt group_size_x #x00000000)
+(bvsgt num_groups_x #x00000000)
+(bvsge group_id_x$1 #x00000000)
+(bvsge group_id_x$2 #x00000000)) (=> (and
+(bvslt group_id_x$1 num_groups_x)
+(bvslt group_id_x$2 num_groups_x)
+(bvsge local_id_x$1 #x00000000)
+(bvsge local_id_x$2 #x00000000)
+(bvslt local_id_x$1 group_size_x)
+(bvslt local_id_x$2 group_size_x)
+(bvsgt group_size_y #x00000000)
+(bvsgt num_groups_y #x00000000)
+(bvsge group_id_y$1 #x00000000)
+(bvsge group_id_y$2 #x00000000)
+(bvslt group_id_y$1 num_groups_y)
+(bvslt group_id_y$2 num_groups_y)
+(bvsge local_id_y$1 #x00000000)
+(bvsge local_id_y$2 #x00000000)
+(bvslt local_id_y$1 group_size_y)
+(bvslt local_id_y$2 group_size_y)
+(bvsgt group_size_z #x00000000)
+(bvsgt num_groups_z #x00000000)
+(bvsge group_id_z$1 #x00000000)
+(bvsge group_id_z$2 #x00000000)
+(bvslt group_id_z$1 num_groups_z)
+(bvslt group_id_z$2 num_groups_z)
+(bvsge local_id_z$1 #x00000000)
+(bvsge local_id_z$2 #x00000000)
+(bvslt local_id_z$1 group_size_z)
+(bvslt local_id_z$2 group_size_z)
+(=> (not _WRITE_HAS_OCCURRED_$$p$1) (= _WRITE_SOURCE_$$p$1 #x00000000))
+(=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000))
+(=> _WRITE_HAS_OCCURRED_$$p$1 (or
+(= _WRITE_SOURCE_$$p$1 #x00000001)
+(= _WRITE_SOURCE_$$p$1 #x00000002)))
+(=> _READ_HAS_OCCURRED_$$p$1 false)
+(=> (and
+(= group_id_x$1 group_id_x$2)
+(= group_id_y$1 group_id_y$2)
+(= group_id_z$1 group_id_z$2)) (or
+(not (= local_id_x$1 local_id_x$2))
+(not (= local_id_y$1 local_id_y$2))
+(not (= local_id_z$1 local_id_z$2))))
+(= (ControlFlow 0 1462) 1187)) inline$_LOG_WRITE_$$p$0$Entry_correct)))))
+$0_correct)))))))))))))
+(push 1)
+(set-info :boogie-vc-id $foo)
+(assert (not
+(=> true $foo)
+))
+(check-sat)
+;(get-value ((ControlFlow 0 0)))
+; (get-value ((ControlFlow 0 1462)))
+; (get-value ((ControlFlow 0 1187)))
+; (get-value ((ControlFlow 0 1189)))
+; (get-value ((ControlFlow 0 1334)))
+; (get-value ((ControlFlow 0 1324)))
+; (get-value ((ControlFlow 0 1328)))
+; (get-value ((ControlFlow 0 1432)))
+; (get-value ((ControlFlow 0 1434)))
+; (get-value ((ControlFlow 0 1440)))
+; (get-model)
+; (assert (not (= (ControlFlow 0 1440) (- 3060))))

diff --git a/test/regress/regress0/bug522.smt2 b/test/regress/regress0/bug522.smt2
new file mode 100644 (file)
index 0000000..7c47c5f
--- /dev/null
+++ b/test/regress/regress0/bug522.smt2
@@ -0,0 +1,15 @@
+; EXPECT: sat
+; EXPECT: sat
+; EXIT: 10
+(set-option :incremental "true")
+(set-logic QF_UF)
+
+(push 1)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
+(assert (= x y))
+(check-sat)
+(pop 1)
+
+(check-sat)