diff options
Diffstat (limited to 'test/regress/regress1/fmf/bug723-irrelevant-funs.smt2')
| -rw-r--r-- | test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 index b9141f2e2..d700d3b18 100644 --- a/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 +++ b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 @@ -5,7 +5,7 @@ (define-fun $$isFalse$$ ((b Bool)) Bool (not b)) (define-fun $$toString$$ ((b Bool)) String (ite b "true" "false")) (define-fun $$fromString$$ ((s String)) Bool (= s "true")) -(define-fun $$inttostr$$ ((i Int)) String (ite (< i 0) (str.++ "-" (int.to.str (- i))) (int.to.str i))) +(define-fun $$inttostr$$ ((i Int)) String (ite (< i 0) (str.++ "-" (str.from_int (- i))) (str.from_int i))) (declare-fun $$takeWhile$$ (String String) String) (declare-fun $$takeWhileNot$$ (String String) String) (declare-fun $$dropWhile$$ (String String) String) |