From: Morgan Deters Date: Tue, 16 Jul 2013 22:28:03 +0000 (-0400) Subject: Fix bug 516; include some bug testcases. X-Git-Tag: cvc5-1.0.0~7287^2~58 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=004bcc12f592991db93ffd92cfb5925940c80980;p=cvc5.git Fix bug 516; include some bug testcases. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b72f52092..2cddc29cf 100644 --- 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 75187b7bd..234b137c8 100644 --- 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 b1c15c73a..92574d5a6 100644 --- 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 index 000000000..b5f5d49eb --- /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 index 000000000..4bdb968d8 --- /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 index 000000000..6751d4077 --- /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 index 000000000..47b73e8aa --- /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 index 000000000..7c47c5fd6 --- /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)