From 561522f882f6467864f25ae65b8d8a9136b89586 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 9 May 2017 14:20:13 -0700
Subject: [PATCH] missing file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/shell/lp_frontend.h | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 src/shell/lp_frontend.h

diff --git a/src/shell/lp_frontend.h b/src/shell/lp_frontend.h
new file mode 100644
index 000000000..68e6a736e
--- /dev/null
+++ b/src/shell/lp_frontend.h
@@ -0,0 +1,8 @@
+/*
+  Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+  Released under Apache 2.0 license as described in the file LICENSE.
+
+  Author: Lev Nachmanson
+*/
+#pragma once
+unsigned read_mps_file(char const * mps_file_name);