oops, reverting a change to a regression test that had intentionally caused a typeche...

diff --git a/test/regress/regress0/simple-rdl-definefun.smt2 b/test/regress/regress0/simple-rdl-definefun.smt2
index c04a1ed64ecc7bcfad8d1b2809b88cd067dc5b6b..08e99867afc61bc4762e2ab60c1763a11ea6b56a 100644 (file)
--- a/test/regress/regress0/simple-rdl-definefun.smt2
+++ b/test/regress/regress0/simple-rdl-definefun.smt2
@@ -7,7 +7,7 @@
 (define-sort F (x) (A Real Real))
 (declare-fun x2 () (F Real))
 (define-fun minus ((x Real) (z Real)) Real (- x z))
-(define-fun less ((x Real) (z Real)) Real (< x z))
+(define-fun less ((x Real) (z Real)) Bool (< x z))
 (define-fun foo ((x Real) (z Real)) Bool (less x z))
 (assert (not (=> (foo (minus x y) 0) (less x y))))
 (check-sat)