3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +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 3d6f8840c6
commit e3ae0ba0bd

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