projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b539a16) | patch
Set default language to smt lib 2.6 (including as a base language for sygus), update...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 4 Aug 2017 14:51:35 +0000 (16:51 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 4 Aug 2017 14:51:35 +0000 (16:51 +0200)
commit59620e0dcafd8224ce609785c37dd8350c33683f
tree1bd882ba00e2716ace9f520bcfc32ac6374f9b38tree
parentb539a167fa56deea34472a9725693f45ae325dd8commit | diff
Set default language to smt lib 2.6 (including as a base language for sygus), update regressions.
86 files changed:
src/main/driver_unified.cpp diff | blob | history
src/options/language.cpp diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
test/regress/regress0/arith/bug716.0.smt2 diff | blob | history
test/regress/regress0/bug296.smt2 diff | blob | history
test/regress/regress0/bug484.smt2 diff | blob | history
test/regress/regress0/bug507.smt2 diff | blob | history
test/regress/regress0/bug541.smt2 diff | blob | history
test/regress/regress0/bug567.smt2 diff | blob | history
test/regress/regress0/bug681.smt2 diff | blob | history
test/regress/regress0/datatypes/bug597-rbt.smt2 diff | blob | history
test/regress/regress0/datatypes/bug604.smt2 diff | blob | history
test/regress/regress0/datatypes/bug625.smt2 diff | blob | history
test/regress/regress0/datatypes/cdt-model-cade15.smt2 diff | blob | history
test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 diff | blob | history
test/regress/regress0/datatypes/coda_simp_model.smt2 diff | blob | history
test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 diff | blob | history
test/regress/regress0/datatypes/dt-param-2.6.smt2 diff | blob | history
test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 diff | blob | history
test/regress/regress0/datatypes/dt-param-card4-unsat.smt2 diff | blob | history
test/regress/regress0/datatypes/example-dailler-min.smt2 diff | blob | history
test/regress/regress0/datatypes/is_test.smt2 diff | blob | history
test/regress/regress0/datatypes/jsat-2.6.smt2 diff | blob | history
test/regress/regress0/datatypes/pair-real-bool.smt2 diff | blob | history
test/regress/regress0/datatypes/sc-cdt1.smt2 diff | blob | history
test/regress/regress0/datatypes/stream-singleton.smt2 diff | blob | history
test/regress/regress0/datatypes/tenum-bug.smt2 diff | blob | history
test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2 diff | blob | history
test/regress/regress0/fmf/agree466.smt2 diff | blob | history
test/regress/regress0/fmf/agree467.smt2 diff | blob | history
test/regress/regress0/fmf/bug0909.smt2 diff | blob | history
test/regress/regress0/fmf/bug651.smt2 diff | blob | history
test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 diff | blob | history
test/regress/regress0/fmf/bug764.smt2 diff | blob | history
test/regress/regress0/fmf/cons-sets-bounds.smt2 diff | blob | history
test/regress/regress0/fmf/constr-ground-to.smt2 diff | blob | history
test/regress/regress0/fmf/datatypes-ufinite-nested.smt2 diff | blob | history
test/regress/regress0/fmf/datatypes-ufinite.smt2 diff | blob | history
test/regress/regress0/fmf/dt-proper-model.smt2 diff | blob | history
test/regress/regress0/fmf/fmc_unsound_model.smt2 diff | blob | history
test/regress/regress0/fmf/forall_unit_data2.smt2 diff | blob | history
test/regress/regress0/fmf/fore19-exp2-core.smt2 diff | blob | history
test/regress/regress0/fmf/german169.smt2 diff | blob | history
test/regress/regress0/fmf/german73.smt2 diff | blob | history
test/regress/regress0/fmf/jasmin-cdt-crash.smt2 diff | blob | history
test/regress/regress0/fmf/krs-sat.smt2 diff | blob | history
test/regress/regress0/fmf/loopy_coda.smt2 diff | blob | history
test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 diff | blob | history
test/regress/regress0/fmf/nun-0208-to.smt2 diff | blob | history
test/regress/regress0/fmf/sc-crash-052316.smt2 diff | blob | history
test/regress/regress0/fmf/sc_bad_model_1221.smt2 diff | blob | history
test/regress/regress0/fmf/tail_rec.smt2 diff | blob | history
test/regress/regress0/fmf/with-ind-104-core.smt2 diff | blob | history
test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 diff | blob | history
test/regress/regress0/push-pop/bug654-dd.smt2 diff | blob | history
test/regress/regress0/push-pop/bug674.smt2 diff | blob | history
test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 diff | blob | history
test/regress/regress0/push-pop/bug765.smt2 diff | blob | history
test/regress/regress0/push-pop/fmf-fun-dbu.smt2 diff | blob | history
test/regress/regress0/quantifiers/bug822.smt2 diff | blob | history
test/regress/regress0/quantifiers/bug_743.smt2 diff | blob | history
test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 diff | blob | history
test/regress/regress0/quantifiers/cdt-0208-to.smt2 diff | blob | history
test/regress/regress0/quantifiers/macro-subtype-param.smt2 diff | blob | history
test/regress/regress0/quantifiers/parametric-lists.smt2 diff | blob | history
test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 diff | blob | history
test/regress/regress0/quantifiers/rew-to-scala.smt2 diff | blob | history
test/regress/regress0/quantifiers/simp-len.smt2 diff | blob | history
test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 diff | blob | history
test/regress/regress0/quantifiers/subtype-param-unk.smt2 diff | blob | history
test/regress/regress0/quantifiers/subtype-param.smt2 diff | blob | history
test/regress/regress0/rewriterules/native_datatypes.smt2 diff | blob | history
test/regress/regress0/rewriterules/native_datatypes2.smt2 diff | blob | history
test/regress/regress0/sep/trees-1.smt2 diff | blob | history
test/regress/regress0/sets/dt-simp-mem.smt2 diff | blob | history
test/regress/regress0/strings/bug686dd.smt2 diff | blob | history
test/regress/regress0/sygus/clock-inc-tuple.sy diff | blob | history
test/regress/regress0/sygus/dt-no-syntax.sy diff | blob | history
test/regress/regress0/sygus/dt-test-ns.sy diff | blob | history
test/regress/regress0/sygus/list-head-x.sy diff | blob | history
test/regress/regress0/sygus/max.smt2 diff | blob | history
test/regress/regress0/sygus/sygus-dt.sy diff | blob | history
test/regress/regress1/datatypes/manos-model.smt2 diff | blob | history
test/regress/regress1/fmf/ForElimination-scala-9.smt2 diff | blob | history
test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2 diff | blob | history
test/regress/regress1/strings/cmu-dis-0707-3.smt2 diff | blob | history