projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ea514f2) | patch
Minor change to F-Length inference in strings. No internal tracking of cardinality...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 7 Mar 2016 18:39:50 +0000 (12:39 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 7 Mar 2016 18:39:50 +0000 (12:39 -0600)
commitb4c7be882b88c6741212ecd9c6be4e91fec76087
tree0f96427e0e6f84ff6ac60ac81ff6f13459515295tree
parentea514f2aa787998ac31f8546bd202890f6bac056commit | diff
Minor change to F-Length inference in strings. No internal tracking of cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.h diff | blob | history
test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/Makefile.am diff | blob | history