diff options
Diffstat (limited to 'test/regress/regress1/sym/q-constant.smt2')
| -rw-r--r-- | test/regress/regress1/sym/q-constant.smt2 | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/regress1/sym/q-constant.smt2 b/test/regress/regress1/sym/q-constant.smt2 new file mode 100644 index 000000000..b8fee6c8d --- /dev/null +++ b/test/regress/regress1/sym/q-constant.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic ALL) +(set-info :status unsat) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) +(declare-fun R (Int Int) Bool) + +(assert (or (forall ((x Int)) (R x a)) (forall ((x Int)) (R x b)))) +(assert (not (R c a))) +(assert (not (R c b))) + +(check-sat) |