blob: 603c783d3eb38947753f9a8ce1125b231d15f89c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
; COMMAND-LINE: --fmf-fun --no-check-models
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(define-fun $$Bool.isTrue$$ ((b Bool)) Bool b)
(define-fun $$Bool.isFalse$$ ((b Bool)) Bool (not b))
(define-funs-rec
(
(f123454321$multipleArgsFunction((x$$645421 Bool) (y$$645422 Bool)) Bool)
(f12345678$myConst() Int)
)
(
(= x$$645421 y$$645422)
3
)
)
(declare-fun i1000$$1000() Bool)
(declare-fun i1001$$1001() Bool)
(declare-fun i1002$$1002() Int)
(assert (f123454321$multipleArgsFunction i1000$$1000 i1001$$1001))
(assert (= i1002$$1002 f12345678$myConst))
(check-sat)
|
