Home
last modified time | relevance | path

Searched refs:BTOR_QUANT_SYNTH_ELMR (Results 1 – 5 of 5) sorted by relevance

/dports/math/boolector/boolector-3.2.2/src/
H A Dbtoropt.h113 #define BTOR_QUANT_SYNTH_MAX BTOR_QUANT_SYNTH_ELMR
114 #define BTOR_QUANT_SYNTH_DFLT BTOR_QUANT_SYNTH_ELMR
H A Dbtortypes.h962 BTOR_QUANT_SYNTH_ELMR, enumerator
H A Dbtoropt.c1204 BTOR_QUANT_SYNTH_ELMR, in btor_opt_init_opts()
H A Dbtorsynth.c994 assert (btor_opt_get (btor, BTOR_OPT_QUANT_SYNTH) != BTOR_QUANT_SYNTH_ELMR in synthesize()
H A Dbtorslvquant.c1537 else if (opt_synth_mode == BTOR_QUANT_SYNTH_ELMR) in synthesize()
1539 assert (opt_synth_mode == BTOR_QUANT_SYNTH_ELMR); in synthesize()