We've got some updates regarding OBS and GitHub/GitLab integration. Have a look and let us know what you think! 🧐


File z3.spec of Package z3

# spec file for package z3
# Copyright (c) 2018 SUSE LINUX GmbH, Nuernberg, Germany.
# All modifications and additions to the file contributed by third parties
# remain the property of their copyright owners, unless otherwise agreed
# upon. The license for this file, and modifications and additions to the
# file, is the same license as for the pristine package itself (unless the
# license for the pristine package is not an Open Source License, in which
# case the license is the MIT License). An "Open Source License" is a
# license that conforms to the Open Source Definition (Version 1.9)
# published by the Open Source Initiative.

# Please submit bugfixes or comments via http://bugs.opensuse.org/

%define version_unconverted 4.6.0+git.20180112
%define sover 4_6
%if 0%{?suse_version} >= 1500
# Use python3 n SLE/Leap 15.0 and Tumbleweed
%define _python python3
%define _python_sitelib %{python3_sitelib}
%define _python python
%define _python_sitelib %{python_sitelib}
# USe python2 on older distros
Name:           z3
Version:        4.6.0+git.20180112
Release:        0
Summary:        Theorem prover from Microsoft Research
License:        MIT
Group:          Productivity/Scientific/Other
URL:            https://github.com/Z3Prover/z3/wiki
Source0:        %{name}-%{version}.tar.xz
Patch0:         remove-timestamp.patch
BuildRequires:  %{_python}-devel
BuildRequires:  cmake
BuildRequires:  gcc-c++
BuildRequires:  gmp-devel
BuildRequires:  ninja
BuildRequires:  xz

Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates
several decision procedures: Linear real and integer arithmetic,
fixed-size bit vectors, uninterpreted functions, extensional arrays,
quantifiers and model generation.

%package -n libz3-%{sover}
Summary:        Library for the Z3 SMT theorem prover
Group:          System/Libraries

%description -n libz3-%{sover}
Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates
several decision procedures.

This subpackage contains the Z3 runtime library needed for Z3 and
other projects.

%package devel
Summary:        Development files for Z3
Group:          Development/Languages/C and C++
Requires:       libz3-%{sover} = %{version}

%description devel
Development files for the Z3 library.

%package -n %{_python}-%{name}
Summary:        Python bindings for Z3
Group:          Development/Languages/Python
Requires:       %{name} = %{version}
Provides:       %{name}-%{_python} = %{version}
Obsoletes:      %{name}-%{_python} < %{version}

%description -n %{_python}-%{name}
Python bindings for the Z3 library.

%setup -q
%patch0 -p1

%define __builder ninja
%{_python} contrib/cmake/bootstrap.py create
%cmake \
  -DUSE_LIB_GMP=true \
  -DPYTHON_EXECUTABLE=%{_bindir}/%{_python} \


%post -n libz3-%{sover} -p /sbin/ldconfig
%postun -n libz3-%{sover} -p /sbin/ldconfig

%license LICENSE.txt

%files -n libz3-%{sover}

%files devel
%dir %{_libdir}/cmake/z3/

%files -n %{_python}-%{name}
%dir %{_python_sitelib}/%{name}

openSUSE Build Service is sponsored by