projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dd67f7c) | patch
Fix cardinality of uninterpreted types when univset is not used (#3663)
authormudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu>
Mon, 3 Feb 2020 18:44:34 +0000 (12:44 -0600)
committerGitHub <noreply@github.com>
Mon, 3 Feb 2020 18:44:34 +0000 (12:44 -0600)
commit25ee78ea4a4111ca7e72e9d81cb7f23f3d1c2fb7
tree1abea753035b49c0dded334158f02531c03138c0tree
parentdd67f7c0250a0725f2afc9fa38d3fca219eb2088commit | diff
Fix cardinality of uninterpreted types when univset is not used (#3663)

* Fixed bug 3662

* format

* small change

* added bug3663.smt2 file

* throw Logic Exception

* throw Logic Exception

* ;EXIT: 1

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
src/theory/sets/cardinality_extension.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sets/finite-type/bug3663.smt2 [new file with mode: 0644] blob