diff options
Diffstat (limited to 'test/regress/regress0/difficulty-simple.smt2')
| -rw-r--r-- | test/regress/regress0/difficulty-simple.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/difficulty-simple.smt2 b/test/regress/regress0/difficulty-simple.smt2 new file mode 100644 index 000000000..a82a96550 --- /dev/null +++ b/test/regress/regress0/difficulty-simple.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --produce-difficulty +; SCRUBBER: sed 's/.*//g' +; EXIT: 0 + +(set-logic ALL) +(set-option :produce-difficulty true) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) + +(assert (or (> a 0) (> b 0) (> c 0))) + +(assert (< (ite (> a b) a b) 0)) + +(check-sat) +(get-difficulty) |