Compiler error while Building Boolector 4.2.0 on ubuntu

[Maryam Mehraban]

Hello,

I configured Boolector with -python and -shared option successfully. But when I ran "make" command, I got the below error:

src/btorcore.c: In function ‘btor_sat_btor’:

src/btorcore.c:3728:29: error: ‘BTOR_OPT_LOGLEVEL’ undeclared (first use in this function)

       btor_set_opt (mclone, BTOR_OPT_LOGLEVEL, 0);

                             ^

src/btorcore.c:3728:29: note: each undeclared identifier is reported only once for each function it appears in

src/btorcore.c: In function ‘check_failed_assumptions’:

src/btorcore.c:4160:24: error: ‘BTOR_OPT_LOGLEVEL’ undeclared (first use in this function)

   btor_set_opt (clone, BTOR_OPT_LOGLEVEL, 0);

Note that I downloaded source code from http://fmv.jku.at/boolector/.

Thanks.

[Mathias Preiner]

Hi,

I can not reproduce this behavior with these options. Can you provide me
with more details (output of configure script...)?

Mathias

On 03/12/2017 04:21 AM, Maryam Mehraban wrote:
> Hello,
> I configured Boolector with -python and -shared option successfully. But
> when I ran "make" command, I got the below error:
>
> src/btorcore.c: In function ‘btor_sat_btor’:

> src/btorcore.c:3728:29: *error: ‘BTOR_OPT_LOGLEVEL’ undeclared (first
> use in this function)*

> btor_set_opt (mclone, BTOR_OPT_LOGLEVEL, 0);
> ^
> src/btorcore.c:3728:29: note: each undeclared identifier is reported
> only once for each function it appears in
> src/btorcore.c: In function ‘check_failed_assumptions’:

> src/btorcore.c:4160:24:*error: ‘BTOR_OPT_LOGLEVEL’ undeclared (first use
> in this function)*

> btor_set_opt (clone, BTOR_OPT_LOGLEVEL, 0);
>
> Note that I downloaded source code from http://fmv.jku.at/boolector/.
> Thanks.
>

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To post to this group, send email to bool...@googlegroups.com
> <mailto:bool...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/boolector.
> For more options, visit https://groups.google.com/d/optout.

[ludwi...@gmx.net]

Hi there,

I've got the same error message when building boolector.

I'm running the Makefile provided from here (). Which yields:

rm -rf boolector*

tar xf archives/boolector*.tar.gz

mv boolector* boolector

cd boolector && ./configure.sh && make

[configure.sh] optimized compilation (no '-g')

[configure.sh] compiling without logging support (default for no debugging)

[configure.sh] disabling PicoSAT: '/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../picosat' missing

[configure.sh] using Lingeling in '/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling'

[configure.sh] not using YalSAT

[configure.sh] not using Druplig

[configure.sh] disabling MiniSAT: '/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../minisat' missing

[configure.sh] linking against 'libm'

[configure.sh] CC=gcc

[configure.sh] CFLAGS=-march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING

[configure.sh] LIBS=-Wl\,-rpath\,/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/build -Lbuild -L/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -llgl -lm

[configure.sh] OBJS=

[configure.sh] INCS=-Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling

[configure.sh] makefile generated

make[1]: Entering directory '/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector'

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btorclone.c -o build/btorclone.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btordcr.c -o build/btordcr.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btoraigvec.c -o build/btoraigvec.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btorbitvec.c -o build/btorbitvec.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btortrapi.c -o build/btortrapi.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btorexp.c -o build/btorexp.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btorabort.c -o build/btorabort.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btordbg.c -o build/btordbg.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btorchkclone.c -o build/btorchkclone.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btorslvsls.c -o build/btorslvsls.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btormc.c -o build/btormc.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btorslvaigprop.c -o build/btorslvaigprop.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btorbeta.c -o build/btorbeta.o

gcc -march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING -Isrc -Ibuild  -I/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector/../lingeling -c src/btorcore.c -o build/btorcore.o

src/btorcore.c: In function 'btor_sat_btor':

src/btorcore.c:3728:29: error: 'BTOR_OPT_LOGLEVEL' undeclared (first use in this function); did you mean 'BTOR_OPT_SEED'?

       btor_set_opt (mclone, BTOR_OPT_LOGLEVEL, 0);

                             ^~~~~~~~~~~~~~~~~

                             BTOR_OPT_SEED

src/btorcore.c:3728:29: note: each undeclared identifier is reported only once for each function it appears in

src/btorcore.c: In function 'check_failed_assumptions':

src/btorcore.c:4160:24: error: 'BTOR_OPT_LOGLEVEL' undeclared (first use in this function); did you mean 'BTOR_OPT_SEED'?

   btor_set_opt (clone, BTOR_OPT_LOGLEVEL, 0);

                        ^~~~~~~~~~~~~~~~~

                        BTOR_OPT_SEED

make[1]: *** [makefile:38: build/btorcore.o] Error 1

make[1]: Leaving directory '/home/marc/packages/symbiyosys-git/src/boolector-2.4.1-with-lingeling-bbc/boolector'

make: *** [makefile:9: all] Error 2

Thanks for any help and best regards,

Marc 

[Mathias Preiner]

Hi Marc,

What OS and gcc version do you use?

Mathias

[ludwi...@gmx.net]

Hi Mathias,

I'm on Arch Linux

$ uname -a

Linux think 4.10.3-1-ck #1 SMP PREEMPT Thu Mar 16 19:50:59 CET 2017 x86_64 GNU/Linux

and my GCC Version is

$ gcc --version
gcc (GCC) 7.2.0
Copyright (C) 2017 Free Software Foundation, Inc.
Dies ist freie Software; die Kopierbedingungen stehen in den Quellen. Es
gibt KEINE Garantie; auch nicht für MARKTGÄNGIGKEIT oder FÜR SPEZIELLE ZWECKE.

If you nedd any other information to reproduce the error/configuration failure, please let me know.

Thanks for your time and best regards,

Marc

[Mathias Preiner]

Hmm, seems like -DNDEBUG is not set in your case even though the configure script says that it does not compile with debug code. I also run Arch Linux with gcc 7.2.0, but it seems on your system the configure script produces different CFLAGS?

configure.sh on my machine:
[configure.sh] CFLAGS=-W -Wall -Wextra -Wredundant-decls -O3 -DNDEBUG -DNBTORLOG -DBTOR_USE_LINGELING

configure.sh on your machine:

[configure.sh] CFLAGS=-march=x86-64 -mtune=generic -O2 -pipe -fstack-protector-strong -fno-plt -DNBTORLOG -DBTOR_USE_LINGELING

Try to add -DNDEBUG to CFLAGS in the generated makefile (boolector/makefile).


Mathias

[ludwi...@gmx.net]

Hi Mathias,

Looks like my $CFLAGS where set before running './configure.sh' so I get around with that:

$ unset CFLAGS && ./configure.sh -O

so boolector builds fine.

Furthermore the README (boolector/README) states to run './configure' which should be './configure.sh' I guess?!

I added a patch if this is from interest, which also removes some trailing whitespaces (my editor removes them automatically so they where removed with the patch).

Thanks for your help and best regards,

Marc