projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 72a0afb) | patch
Do not solve for 0-ary non-constant symbols (for which isVar returns true), add regre...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 4 Apr 2017 14:59:45 +0000 (09:59 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 4 Apr 2017 14:59:57 +0000 (09:59 -0500)
commit6cb3f49d3933061000fe63d2ee7e004cae06d6ba
tree1a8fc7ed586968a872476deb3f5db3dc0f6ae389tree
parent72a0afbd73f1d2505285a965eb0ff3312e201f2ccommit | diff
Do not solve for 0-ary non-constant symbols (for which isVar returns true), add regressions.
src/expr/node.h diff | blob | history
src/theory/theory.cpp diff | blob | history
test/regress/regress0/rels/Makefile.am diff | blob | history
test/regress/regress0/rels/atom_univ2.cvc [new file with mode: 0644] blob
test/regress/regress0/sep/Makefile.am diff | blob | history
test/regress/regress0/sep/nil-no-elim.smt2 [new file with mode: 0644] blob