From d461833fcd5bb1b774c7fa31f0ee3ad88ccdbc0b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Feb 2019 14:31:08 -0800
Subject: [PATCH] fix(library/compiler/llnf): `_sset` and `_uset` were taking
 invalid LLNF arguments

---
 src/library/compiler/llnf.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index d639f1c3fa..b71cab829f 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -793,7 +793,7 @@ class to_llnf_fn {
         for (field_info const & info : k_info.m_field_info) {
             switch (info.m_kind) {
             case field_info::Scalar:
-                if (first && obj_args.size() > 0) {
+                if (first) {
                     r = mk_let_decl(mk_enf_object_type(), r);
                 }
                 r = mk_let_decl(mk_enf_object_type(), mk_sset(r, info.m_size, (k_info.m_num_objs + k_info.m_num_usizes), offset, args[j]));
@@ -801,7 +801,7 @@ class to_llnf_fn {
                 first = false;
                 break;
             case field_info::USize:
-                if (first && obj_args.size() > 0) {
+                if (first) {
                     r = mk_let_decl(mk_enf_object_type(), r);
                 }
                 r = mk_let_decl(mk_enf_object_type(), mk_uset(r, k_info.m_num_objs + uidx, args[j]));