diff options
Diffstat (limited to 'test/regress/regress0/bug217.smt2')
| -rw-r--r-- | test/regress/regress0/bug217.smt2 | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2 new file mode 100644 index 000000000..92b72c87d --- /dev/null +++ b/test/regress/regress0/bug217.smt2 @@ -0,0 +1,14 @@ +; EXPECT: unsat +; EXIT: 20 +(set-logic QF_UF) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun f (Bool) Bool) +(declare-fun x () Bool) +(declare-fun y () Bool) +(declare-fun z () Bool) +(assert (or (f x) (f y) (f z))) +(assert (not (f false))) +(assert (not (f true))) +(check-sat) +;(get-value ((f true) (f false) (f x) (f y) (f z) x y z)) |