From 0a4ee1ac60e6b914ca8173c773eb9db54cdf0f61 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Sat, 24 Oct 2020 09:16:52 -0500 Subject: Fix issue 5271 (#5335) This PR fixes #5271 by splitting on the equality of set members which ensures members are distinct when collectModelInfo is called. Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu --- test/regress/regress1/sets/issue5271.smt2 | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test/regress/regress1/sets/issue5271.smt2 (limited to 'test/regress/regress1') diff --git a/test/regress/regress1/sets/issue5271.smt2 b/test/regress/regress1/sets/issue5271.smt2 new file mode 100644 index 000000000..ba8180b5e --- /dev/null +++ b/test/regress/regress1/sets/issue5271.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun s () (Set Int)) +(assert (> (card s) 1)) +(assert (and (member 0 s) (exists ((x Int)) (member (mod x 1) s)))) +(check-sat) -- cgit v1.2.3