From 038f992ff485d0bf93f962dc9e45330ff1e2e47d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 14 Mar 2019 12:48:27 -0700
Subject: [PATCH] remove platformtarget for dotnetcore spec

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/mk_util.py     | 10 +---------
 src/smt/theory_lra.cpp |  2 +-
 2 files changed, 2 insertions(+), 10 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 18ed0f74e..f57394f3e 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1889,20 +1889,12 @@ class DotNetCoreDLLComponent(Component):
             key = "<AssemblyOriginatorKeyFile>%s</AssemblyOriginatorKeyFile>" % self.key_file
             key += "\n<SignAssembly>true</SignAssembly>"
 
-        if VS_X64:
-            platform = 'x64'
-        elif VS_ARM:
-            platform = 'ARM'
-        else:
-            platform = 'x86'
-
         version = get_version_string(3)
 
         core_csproj_str = """<Project Sdk="Microsoft.NET.Sdk">
 
   <PropertyGroup>
     <TargetFramework>netstandard1.4</TargetFramework>
-    <PlatformTarget>%s</PlatformTarget>    
     <DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants>
     <DebugType>portable</DebugType>
     <AssemblyName>Microsoft.Z3</AssemblyName>
@@ -1923,7 +1915,7 @@ class DotNetCoreDLLComponent(Component):
     <Compile Include="..\%s\*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
   </ItemGroup>
 
-</Project>""" % (platform, version, key, self.to_src_dir)
+</Project>""" % (version, key, self.to_src_dir)
 
         mk_dir(os.path.join(BUILD_DIR, 'dotnet'))
         csproj = os.path.join('dotnet', 'z3.csproj')
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 27362fc77..11a9fa6f7 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1517,7 +1517,7 @@ public:
     }
 
     final_check_status final_check_eh() {
-        IF_VERBOSE(2, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
+        IF_VERBOSE(12, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
         m_use_nra_model = false;
         lbool is_sat = l_true;
         if (m_solver->get_status() != lp::lp_status::OPTIMAL) {