summaryrefslogtreecommitdiff
path: root/test/regress/regress0/let.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/let.smt')
-rw-r--r--test/regress/regress0/let.smt3
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress0/let.smt b/test/regress/regress0/let.smt
index 45d0eaecb..8b747c3e1 100644
--- a/test/regress/regress0/let.smt
+++ b/test/regress/regress0/let.smt
@@ -2,4 +2,5 @@
:logic QF_UF
:status unsat
:extrafuns ((a U) (b U) (f U U))
- :formula (let (?x a) (not (= ?x a)))) \ No newline at end of file
+ :formula (let (?x a) (and (= a b) (not (= ?x b))))
+) \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback