diff options
Diffstat (limited to 'test/regress/regress1/ho/NUM638^1.smt2')
| -rw-r--r-- | test/regress/regress1/ho/NUM638^1.smt2 | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/NUM638^1.smt2 b/test/regress/regress1/ho/NUM638^1.smt2 new file mode 100644 index 000000000..bee17b21a --- /dev/null +++ b/test/regress/regress1/ho/NUM638^1.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --uf-ho --finite-model-find +; EXPECT: unsat + +(set-option :incremental false) +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-sort nat 0) +(declare-fun x () nat) +(declare-fun n_1 () nat) +(assert (not (= x n_1))) +(declare-fun suc (nat) nat) +(declare-fun some ((-> nat Bool)) Bool) +(assert (forall ((Xx nat) (Xy nat)) (=> (= (suc Xx) (suc Xy)) (= Xx Xy)) )) +(assert (forall ((Xx nat)) (=> (not (= Xx n_1)) (some (lambda ((Xu nat)) (= Xx (suc Xu))))) )) +(assert (not (not (=> (forall ((Xx_0 nat) (Xy nat)) (=> (= x (suc Xx_0)) (=> (= x (suc Xy)) (= Xx_0 Xy))) ) (not (some (lambda ((Xu nat)) (= x (suc Xu))))))))) +(meta-info :filename "NUM638^1") +(check-sat-assuming ( (not false) )) |