diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-17 12:08:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-17 12:08:48 -0500 |
| commit | 1f9d6858f2d9cc21e6869ad743d18d07e82b30e7 (patch) | |
| tree | ffee6c2cbbb68c2600fee103049579cf643309a8 /test/regress/regress0/fmf | |
| parent | 8931c69d4dd1afe689cda92f6a9628898f980f30 (diff) | |
Fix spurious warning in sort inference (#2331)
Diffstat (limited to 'test/regress/regress0/fmf')
| -rw-r--r-- | test/regress/regress0/fmf/sort-inf-int.smt2 | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/test/regress/regress0/fmf/sort-inf-int.smt2 b/test/regress/regress0/fmf/sort-inf-int.smt2 deleted file mode 100644 index e4a8978d4..000000000 --- a/test/regress/regress0/fmf/sort-inf-int.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -; COMMAND-LINE: --finite-model-find --sort-inference --no-check-models -; EXPECT: sat -(set-logic UFLIRA) -(set-info :status sat) -(declare-fun f (Int) Int) -(declare-fun g (Int) Int) -(declare-fun h (Int) Int) -(assert (forall ((x Int)) (or (= (f x) (h x)) (= (f x) (g x))))) -(assert (not (= (f 3) (h 3)))) -(assert (not (= (f 5) (g 5)))) -(assert (= (f 4) (g 8))) - -(check-sat) |