| .. |
|
aig
|
Bugfix for AIG tactic.
|
2015-05-14 13:44:39 +01:00 |
|
arith
|
added missing Copyright forms
|
2015-06-10 11:54:02 -07:00 |
|
bv
|
fixes to #52, #53
|
2015-04-28 14:48:59 -07:00 |
|
core
|
bypass simplifier if (m_is_clausal) {
|
2014-10-22 09:02:08 -07:00 |
|
fpa
|
Merge branch 'unstable' of https://github.com/AleksandarZeljic/z3 into smallFloats
|
2015-06-12 18:35:59 +02:00 |
|
nlsat_smt
|
add count of memory allocations and way to limit allocations globally. Fix purification in nlsat_smt to fix regressions on QF_UFNRA
|
2015-06-22 07:45:40 +02:00 |
|
portfolio
|
hide new behavior until tested
|
2015-06-21 02:25:02 -07:00 |
|
sls
|
fix debian amd64 warnings
|
2015-05-18 15:17:21 -07:00 |
|
smtlogics
|
Parameter fix for the qflia default tactic
|
2015-06-08 15:37:17 +01:00 |
|
ufbv
|
address race condition in cleanup methods
|
2014-09-05 11:18:34 -07:00 |
|
converter.h
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
equiv_proof_converter.cpp
|
re-organization of muz
|
2013-08-28 22:11:33 -07:00 |
|
equiv_proof_converter.h
|
re-organization of muz
|
2013-08-28 22:11:33 -07:00 |
|
extension_model_converter.cpp
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
extension_model_converter.h
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
filter_model_converter.cpp
|
fix model transformation bug in bit blaster rule transformer, reported by Sagar Chaki
|
2014-07-08 11:21:19 +02:00 |
|
filter_model_converter.h
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
goal.cpp
|
some confusion about proof generation
|
2013-06-27 12:24:18 -07:00 |
|
goal.h
|
cleanning solver initialization, and fixing named assertion support
|
2012-11-02 16:35:08 -07:00 |
|
goal_num_occurs.cpp
|
Fix file name (use same naming convention)
|
2012-12-14 09:04:20 -08:00 |
|
goal_num_occurs.h
|
Fix file name (use same naming convention)
|
2012-12-14 09:04:20 -08:00 |
|
goal_shared_occs.cpp
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
goal_shared_occs.h
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
goal_util.cpp
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
goal_util.h
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
horn_subsume_model_converter.cpp
|
have free variable utility use a class for more efficient re-use
|
2014-09-15 16:14:22 -07:00 |
|
horn_subsume_model_converter.h
|
break on small cores
|
2015-02-08 10:22:06 +01:00 |
|
model_converter.cpp
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
model_converter.h
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
probe.cpp
|
pull unstable
|
2015-04-01 14:57:11 -07:00 |
|
probe.h
|
Added is_qfaufbv_probe and is_qfauflia_probe.
|
2015-01-19 18:19:43 +00:00 |
|
proof_converter.cpp
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
proof_converter.h
|
checkpoint
|
2012-10-21 18:12:34 -07:00 |
|
replace_proof_converter.cpp
|
re-organization of muz
|
2013-08-28 22:11:33 -07:00 |
|
replace_proof_converter.h
|
break on small cores
|
2015-02-08 10:22:06 +01:00 |
|
tactic.cpp
|
add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core
|
2015-05-09 19:40:34 -07:00 |
|
tactic.h
|
fix openmp nested critical section
|
2015-05-18 12:43:55 -07:00 |
|
tactic_exception.h
|
reorganizing the code
|
2012-10-25 11:28:03 -07:00 |
|
tactical.cpp
|
Various variable renamings to avoid conflicts with previously defined local variables, function parameters, or members (Visual Studio 2015 warnings).
|
2015-05-29 18:13:39 +01:00 |
|
tactical.h
|
add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core
|
2015-05-09 19:40:34 -07:00 |
