projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 86b8b53) | patch
fix quantifier non-bug
authorKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 14 Jun 2012 18:51:34 +0000 (18:51 +0000)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 14 Jun 2012 18:51:34 +0000 (18:51 +0000)
commit31e1f3402d4cd3da7cdfabc440c3b622432849b8
treef8d08f29f00a81c9eb936760ef2e35948181b581tree
parent86b8b53afbbd2259e297709c99d594a79927184acommit | diff
fix quantifier non-bug
src/prop/minisat/core/Solver.cc diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
test/regress/regress0/decision/Makefile.am diff | blob | history
test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 [new file with mode: 0644] blob
test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect [new file with mode: 0644] blob
test/regress/regress0/decision/quant-ex1.smt2.expect diff | blob | history