Nikolaj Bjorner d701702735 remove model converter operator on expr_ref&		2025-09-07 16:42:20 -07:00
..
aig
arith
bv	remove model converter operator on expr_ref&	2025-09-07 16:42:20 -07:00
core	enable conditional euf-completion with (optional) solver	2025-06-06 11:42:31 +02:00
fd_solver
fpa
portfolio	Add virtual translate method to solver_factory class (#7780)	2025-08-14 11:54:34 -07:00
sls
smtlogics
ufbv
CMakeLists.txt
dependency_converter.cpp
dependency_converter.h
dependent_expr_state_tactic.h	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
goal.cpp	fix #7725 - proofs are only possible if context was created with proofs enabled	2025-07-12 09:14:23 +02:00
goal.h
goal_num_occurs.cpp
goal_num_occurs.h
goal_proof_converter.h
goal_shared_occs.cpp
goal_shared_occs.h
goal_util.cpp
goal_util.h
probe.cpp
probe.h
tactic.cpp
tactic.h
tactic_exception.h
tactical.cpp	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
tactical.h
user_propagator_base.h	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00