mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
added fixedpoint.conjecture_file option
This commit is contained in:
parent
f4790a183d
commit
a4f3afd70d
|
@ -77,6 +77,7 @@ def_module_params('fixedpoint',
|
|||
('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'),
|
||||
('batch_expand', BOOL, False, 'DUALITY: use batch expansion'),
|
||||
('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
|
||||
('conjecture_file', STRING, '', 'DUALITY: save conjectures to file'),
|
||||
))
|
||||
|
||||
|
||||
|
|
|
@ -211,6 +211,7 @@ lbool dl_interface::query(::expr * query) {
|
|||
rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0");
|
||||
rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
|
||||
rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
|
||||
rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file());
|
||||
unsigned rb = m_ctx.get_params().recursion_bound();
|
||||
if(rb != UINT_MAX){
|
||||
std::ostringstream os; os << rb;
|
||||
|
|
Loading…
Reference in a new issue