Skip to content

Commit

Permalink
Do not rewrite datatype inferences prior to proof reconstruction (cvc…
Browse files Browse the repository at this point in the history
…5#11465)

It is not clear why this was done, it makes proof reconstruction fail in
rare cases, added a regression for this.
ajreynol authored Dec 20, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
1 parent 5ee60a5 commit 96a35d7
Showing 3 changed files with 16 additions and 5 deletions.
5 changes: 0 additions & 5 deletions src/theory/datatypes/inference_manager.cpp
Original file line number Diff line number Diff line change
@@ -150,11 +150,6 @@ Node InferenceManager::prepareDtInference(Node conc,
{
Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp
<< " by " << id << std::endl;
if (conc.getKind() == Kind::EQUAL && conc[0].getType().isBoolean())
{
// must turn (= conc false) into (not conc)
conc = rewrite(conc);
}
if (isProofEnabled())
{
Assert(ipc != nullptr);
1 change: 1 addition & 0 deletions test/regress/cli/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1461,6 +1461,7 @@ set(regress_0_tests
regress0/quantifiers/cond-var-elim-binary.smt2
regress0/quantifiers/dd_german169_semi_eval.smt2
regress0/quantifiers/dd_spark2014-pat.smt2
regress0/quantifiers/dd_SA10-027-dt-ipc.smt2
regress0/quantifiers/dd.german169-ieval.smt2
regress0/quantifiers/dd.german169-lemma-inp.smt2
regress0/quantifiers/dd.ho-matching-enum.smt2
15 changes: 15 additions & 0 deletions test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
; EXPECT: unsat
; DISABLE-TESTER: cpc
; Disabled cpc due to congruence on overloaded user functions.
(set-logic ALL)
(declare-sort i 0)
(declare-sort s 0)
(declare-datatypes ((u 0)) (((us (r Bool) (e Int) (c s)))))
(declare-datatypes ((us_ 0)) (((us (c i) (e u)))))
(declare-datatypes ((_r 0)) (((s_ (_s us_)))))
(declare-fun s_ (s) _r)
(declare-fun us (_r) s)
(assert (forall ((x _r)) (= x (s_ (us x)))))
(declare-const n u)
(assert (exists ((x_ us_)) (not (=> (r n) (= (s_ x_) (s_ (c (us false 0 (us (s_ (us (c (_s (s_ (c n)))) n))))))) (forall ((o u)) (or (forall ((x us_)) (or (forall ((o u)) (or (forall ((x us_)) (or (forall ((o u)) (or (forall ((x us_)) (or (exists ((t u)) (= (r o) (= (r o) (r (e (_s (s_ (c t)))))))) (= (s_ x_) (s_ (c (us false 0 (us (s_ (us (c (_s (s_ (c o)))) (us (r (e (_s (s_ (c (us false 0 (us (s_ x_)))))))) (e (e (_s (s_ (c o))))) (us (s_ x_))))))))))))))))))))))))))
(check-sat)

0 comments on commit 96a35d7

Please sign in to comment.