3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

SLS refactoring

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-03-19 17:26:05 +00:00
parent b1eeb9adf4
commit a6227d5446

View file

@ -18,6 +18,10 @@ Notes:
This file should go away completely once we have evaluated all options.
--*/
#ifndef _SLS_COMPILATION_SETTINGS_H_
#define _SLS_COMPILATION_SETTINGS_H_
// which unsatisfied assertion is selected? only works with _FOCUS_ > 0
// 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score
#define _BFS_ 0
@ -155,4 +159,6 @@ InvalidConfiguration;
#endif
#if (_PERC_STICKY_ && !_FOCUS_)
InvalidConfiguration;
#endif
#endif