projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 747c971) | patch
SMT-LIBv2 compliance regarding outputting "unknown".
authorMorgan Deters <mdeters@gmail.com>
Tue, 18 Sep 2012 14:50:45 +0000 (14:50 +0000)
committerMorgan Deters <mdeters@gmail.com>
Tue, 18 Sep 2012 14:50:45 +0000 (14:50 +0000)
commit283822d8dc26004cd5b15a5b8e198d4f3068ebd0
treefce9a276c2c5278f461ef49b09c592ca71c1f6ebtree
parent747c97106c6a6f8f8718b4b5ddfd61f505f3bf5fcommit | diff
SMT-LIBv2 compliance regarding outputting "unknown".

Thanks to Peter Collingbourne for the report, and the patch!

(this commit was certified error- and warning-free by the test-and-commit script.)
17 files changed:
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.h diff | blob | history
test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 diff | blob | history
test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect diff | blob | history
test/regress/regress0/quantifiers/array-unsat-simp3.smt2 diff | blob | history
test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect diff | blob | history
test/regress/regress0/quantifiers/bug291.smt2 diff | blob | history
test/regress/regress0/quantifiers/bug291.smt2.expect diff | blob | history
test/regress/regress0/quantifiers/ex1.smt2 diff | blob | history
test/regress/regress0/quantifiers/ex1.smt2.expect diff | blob | history
test/regress/regress0/quantifiers/ex7.smt2 diff | blob | history
test/regress/regress0/quantifiers/ex7.smt2.expect diff | blob | history
test/regress/regress0/tptp_parser5.p diff | blob | history
test/regress/regress0/tptp_parser6.p diff | blob | history
test/regress/regress0/tptp_parser7.p diff | blob | history
test/regress/regress0/tptp_parser8.p diff | blob | history
test/regress/regress0/tptp_parser9.p diff | blob | history