diff options
Diffstat (limited to 'test/regress/regress0/arith/integers/ackermann1.smt2')
| -rw-r--r-- | test/regress/regress0/arith/integers/ackermann1.smt2 | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/integers/ackermann1.smt2 b/test/regress/regress0/arith/integers/ackermann1.smt2 new file mode 100644 index 000000000..b04210f36 --- /dev/null +++ b/test/regress/regress0/arith/integers/ackermann1.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_UFLIA) + +(declare-fun a () Int) +(declare-fun b () Int) + +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) + +(assert (= (f (g (f (f a)))) (f (g (f a))))) +(assert (= (f a) b)) +(assert (= (f b) a)) +(assert (not (= a b))) +(assert (= (g a) (f a))) +(assert (= (g b) (f b))) + +(check-sat) +(exit)
\ No newline at end of file |