projects
/
cvc5.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
50e44068903501b76612873e9bf69f5fe91df442
[cvc5.git]
/
test
/
regress
/
regress0
/
push-pop
/
bug821-check_sat_assuming.smt2
1
; COMMAND-LINE: --incremental
2
; EXPECT: sat
3
; EXPECT: unsat
4
; EXPECT: sat
5
(set-logic UF)
6
(declare-fun _substvar_4_ () Bool)
7
(check-sat-assuming (_substvar_4_ _substvar_4_))
8
(check-sat-assuming (_substvar_4_ false))
9
(check-sat-assuming ((= _substvar_4_ _substvar_4_)))