projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b16e3a3) | patch
if running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as...
authorMorgan Deters <mdeters@gmail.com>
Mon, 11 Jul 2011 18:48:16 +0000 (18:48 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 11 Jul 2011 18:48:16 +0000 (18:48 +0000)
commit4c428c8f74ae913f05287c0595c8887c31089520
treeab3041c59d6d8700e96c623675a1570208c6374ftree
parentb16e3a3187ce721e32042f241cc718529cdd0573commit | diff
if running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as well as pre-registration of free constants of uninterpreted sort, etc..
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
test/regress/regress0/arrays/Makefile.am diff | blob | history
test/regress/regress0/arrays/incorrect2.minimized.smt diff | blob | history
test/regress/regress0/arrays/incorrect8.minimized.smt [new file with mode: 0644] blob