projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 21ac21a) | patch
Do not eliminate non-standard arithmetic operators in recursive function definitions...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 28 Apr 2017 16:46:53 +0000 (11:46 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 28 Apr 2017 16:46:53 +0000 (11:46 -0500)
commit24385c4c5f9c17610f10ed2f8d44c10a16c1567f
tree801876270012b2f3541b363f4f1cc881c432ebd2tree
parent21ac21a2ff3ba3eeac4deabf0c4b79ca4cc8df77commit | diff
Do not eliminate non-standard arithmetic operators in recursive function definitions, add regression.
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2 [new file with mode: 0644] blob