projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 62d3610) | patch
Add the problematic input from issue 2183 as a regression test (#3008)
authorMartin <martin.brain@cs.ox.ac.uk>
Fri, 17 May 2019 23:10:19 +0000 (00:10 +0100)
committerAndres Noetzli <noetzli@stanford.edu>
Fri, 17 May 2019 23:10:19 +0000 (16:10 -0700)
commit5c38c59cb40df00e29cbd9d30495833f88c6d4fb
tree5602ee8294a1e4df3bffc0452fe648706cd7748etree
parent62d361071ea54c9b7cba882313ab4dedef6f1286commit | diff
Add the problematic input from issue 2183 as a regression test (#3008)

Although CVC4's behaviour is actually correct, this is to make
things a bit clearer and prevent confusion in the future.
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/fp/down-cast-RNA.smt2 [new file with mode: 0644] blob