From 1f9d6858f2d9cc21e6869ad743d18d07e82b30e7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 Aug 2018 12:08:48 -0500 Subject: Fix spurious warning in sort inference (#2331) --- test/regress/regress0/fmf/sort-inf-int.smt2 | 13 ------------- 1 file changed, 13 deletions(-) delete mode 100644 test/regress/regress0/fmf/sort-inf-int.smt2 (limited to 'test/regress/regress0/fmf') 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) -- cgit v1.2.3