projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5ce46e8) | patch
Do not eliminate extended arithmetic symbols when finite model finding is on, add...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 5 May 2017 22:41:18 +0000 (17:41 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 5 May 2017 22:41:18 +0000 (17:41 -0500)
commitf4b158635255affcafe52c7664fc5de4660c3f83
treec22a6b39b7b8137b5ca476188b4d8fad1430f45ctree
parent5ce46e8a6ac10388b7a2032c7d67a81da0edbd5ecommit | diff
Do not eliminate extended arithmetic symbols when finite model finding is on, add regression.
src/options/quantifiers_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 [new file with mode: 0644] blob