git.libre-soc.org Git - cvc5.git/commit

author	Gereon Kremer <gkremer@stanford.edu>
	Tue, 7 Dec 2021 23:47:15 +0000 (15:47 -0800)
committer	GitHub <noreply@github.com>
	Tue, 7 Dec 2021 23:47:15 +0000 (23:47 +0000)
commit	099043243897f4d216224e7be652a00a81e9bb6c
tree	77a631ad7f9392028cf2978f17bc2ecf1bf4abfb	tree
parent	e5aa96010b548a8ec0964fb002246e21ced2cac9	commit \| diff

Remove more static accesses to options (#7764)

This PR removes a bunch of the remaining places where options are accessed statically.

21 files changed:

src/proof/unsat_core.cpp		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/model.cpp		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/theory/bv/int_blaster.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_list.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_verify.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/template_infer.cpp		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history