Assertion `!InsideSubstitutionMap(e0) && "e0 MUST NOT be in the SolverMap"' failed.

[mdempsky]

I'm seeing this assert failure + stack trace trying to use STP in Chromium:

symbolic_unittests: ../../third_party/stp/src/include/stp/Simplifier/SubstitutionMap.h:161: bool stp::SubstitutionMap::UpdateSubstitutionMapFewChecks(const stp::ASTNode &, const stp::ASTNode &): Assertion `!InsideSubstitutionMap(e0) && "e0 MUST NOT be in the SolverMap"' failed.
Received signal 6
#0 0x00000057ff0e base::debug::StackTrace::StackTrace()
#1 0x00000057fa4f base::debug::(anonymous namespace)::StackDumpSignalHandler()
#2 0x7f3407c2b340 <unknown>
#3 0x7f340788ccc9 gsignal
#4 0x7f34078900d8 abort
#5 0x7f3407885b86 <unknown>
#6 0x7f3407885c32 __assert_fail
#7 0x0000007a284b stp::SubstitutionMap::UpdateSubstitutionMapFewChecks()
#8 0x000000783fd7 stp::Simplifier::UpdateSubstitutionMapFewChecks()
#9 0x000000777132 stp::RemoveUnconstrained::replace()
#10 0x00000077660a stp::RemoveUnconstrained::topLevel_other()
#11 0x000000770aa4 stp::RemoveUnconstrained::topLevel()
#12 0x0000007c87e5 stp::STP::sizeReducing()
#13 0x0000007c45d2 stp::STP::TopLevelSTPAux()
#14 0x0000007c3edb stp::STP::solve_by_sat_solver()
#15 0x0000007c7b9b stp::STP::TopLevelSTP()
#16 0x0000006efc8f vc_query_with_timeout
#17 0x0000006efad2 vc_query

Here's a minimized test case:

VC vc = vc_createValidityChecker();
Expr falseExpr = vc_falseExpr(vc);

Expr A = vc_varExpr(vc, "A", vc_bv32Type(vc));
Expr B = vc_varExpr(vc, "B", vc_bv32Type(vc));

vc_push(vc);

Expr AplusB = vc_bv32PlusExpr(vc, A, B);
Expr AplusBplus42 = vc_bv32PlusExpr(vc, AplusB, vc_bv32ConstExprFromInt(vc, 42));

vc_assertFormula(vc, vc_bvGtExpr(vc, AplusB, vc_bv32ConstExprFromInt(vc, 100)));
assert(0 == vc_query(vc, falseExpr));
vc_assertFormula(vc, vc_bvGtExpr(vc, AplusBplus42, vc_bv32ConstExprFromInt(vc, 5)));
assert(0 == vc_query(vc, falseExpr));

vc_Destroy(vc);

I'm using 05e2e26 and stp/minisat@3db5894.

Also, I'm building stp and minisat as part of the Chromium build rather than using the standard stp Makefile. Here's a representative compile invocation so you can know what custom flags we're setting that might be relevant:

../../third_party/llvm-build/Release+Asserts/bin/clang++ -MMD -MF obj/third_party/stp/src/lib/Sat/minisat/minisat/simp/stp.SimpSolver.o.d -DV8_DEPRECATION_WARNINGS -DCLD_VERSION=2 -DENABLE_MDNS=1 -DENABLE_NOTIFICATIONS -DENABLE_PEPPER_CDMS -DENABLE_PLUGINS=1 -DENABLE_PRINTING=1 -DENABLE_BASIC_PRINTING=1 -DENABLE_PRINT_PREVIEW=1 -DENABLE_SPELLCHECK=1 -DDONT_EMBED_BUILD_METADATA -DUSE_UDEV -DUI_COMPOSITOR_IMAGE_TRANSPORT -DUSE_ASH=1 -DUSE_AURA=1 -DUSE_PANGO=1 -DUSE_CAIRO=1 -DUSE_CLIPBOARD_AURAX11=1 -DUSE_DEFAULT_RENDER_THEME=1 -DUSE_GLIB=1 -DUSE_NSS_CERTS=1 -DUSE_X11=1 -DENABLE_WEBRTC=1 -DENABLE_EXTENSIONS=1 -DENABLE_CONFIGURATION_POLICY -DENABLE_TASK_MANAGER=1 -DENABLE_THEMES=1 -DENABLE_CAPTIVE_PORTAL_DETECTION=1 -DENABLE_SESSION_SERVICE=1 -DENABLE_APP_LIST=1 -DENABLE_SETTINGS_APP=1 -DENABLE_SUPERVISED_USERS=1 -DENABLE_SERVICE_DISCOVERY=1 -DENABLE_AUTOFILL_DIALOG=1 -DENABLE_REMOTING=1 -DENABLE_GOOGLE_NOW=1 -DENABLE_ONE_CLICK_SIGNIN -DENABLE_HIDPI=1 -DV8_USE_EXTERNAL_STARTUP_DATA -DENABLE_BACKGROUND=1 -DENABLE_PRE_SYNC_BACKUP -DFULL_SAFE_BROWSING -DSAFE_BROWSING_CSD -DSAFE_BROWSING_DB_LOCAL -DSAFE_BROWSING_SERVICE -DCHROMIUM_BUILD -DENABLE_MEDIA_ROUTER=1 -DCR_CLANG_REVISION=239765-1 -D_FILE_OFFSET_BITS=64 -D_LARGEFILE_SOURCE -D_LARGEFILE64_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D_DEBUG -DDYNAMIC_ANNOTATIONS_ENABLED=1 -DWTF_USE_DYNAMIC_ANNOTATIONS=1 -D_GLIBCXX_DEBUG=1 -I../.. -Igen -I../../third_party/stp/config -I../../third_party/stp/src/include -I../../third_party/stp/src/lib -I../../third_party/stp/src/lib/Sat -I../../third_party/stp/src/lib/Sat/cryptominisat2/mtl -I../../third_party/stp/src/lib/extlib-abc -Igen/third_party/stp/src/include -I../../third_party/stp/src/include -fno-strict-aliasing -fstack-protector --param=ssp-buffer-size=4 -m64 -march=x86-64 -funwind-tables -fPIC -pipe -pthread -B../../third_party/binutils/Linux_x64/Release/bin -fcolor-diagnostics -Wall -Wsign-compare -Wendif-labels -Werror -Wno-missing-field-initializers -Wno-unused-parameter -Wno-c++11-narrowing -Wno-char-subscripts -Wno-covered-switch-default -Wno-deprecated-register -Wno-unneeded-internal-declaration -Wno-reserved-user-defined-literal -Wno-inconsistent-missing-override -fvisibility=hidden -Xclang -load -Xclang ../../third_party/llvm-build/Release+Asserts/lib/libFindBadConstructs.so -Xclang -plugin-arg-find-bad-constructs -Xclang check-templates -Xclang -add-plugin -Xclang find-bad-constructs -Wheader-hygiene -Wstring-conversion -O0 -g2 -gsplit-dwarf -U_DEBUG -Wno-dangling-else -Wno-empty-body -Wno-header-guard -Wno-implicit-function-declaration -Wno-mismatched-tags -Wno-overloaded-virtual -Wno-parentheses-equality -Wno-return-type -Wno-sign-compare -Wno-sometimes-uninitialized -Wno-string-conversion -Wno-tautological-constant-out-of-range-compare -Wno-unused-const-variable -Wno-unused-function -Wno-unused-private-field -fno-threadsafe-statics -fvisibility-inlines-hidden -Wno-undefined-bool-conversion -Wno-tautological-undefined-compare -std=gnu++11 -fno-rtti -fno-exceptions -fexceptions -c ../../third_party/stp/src/lib/Sat/minisat/minisat/simp/SimpSolver.cc -o obj/third_party/stp/src/lib/Sat/minisat/minisat/simp/stp.SimpSolver.o

The only local modification I've made is that in stp/lib/Sat/MinisatCore.cpp and stp/lib/Sat/SimplifyingMinisat.cpp I had to comment out the "#define __STDC_FORMAT_MACROS" lines because they caused "macro redefined" errors as Chromium builds with -D__STDC_FORMAT_MACROS already.

[mdempsky]

BTW, I should caution I have no idea if I'm using the API properly/optimally. I picked up the vc_query(vc, falseExpr) trick from KLEE, which I understand to mean that as long as it returns INVALID (i.e., it's not possible to "prove" false), then the set of asserted expressions/formulas are satisfiable (and satisfying values for A and B can be retrieved using vc_getCounterExample + getBVUnsigned).

If there's a better way to write the above, please let me know.

[msoos]

Before you think I haven't done anything with this... I spent an hour or two on this one during the weekend but gave up. I need to dig deeper and I was a bit distracted. Anyway, I did actually spend time on it. I'll try to get to the bottom of it. I think the pop/push is the issue here. I the meanwhile, the python API has that fixed and you may be able to use that to your advantage. It's easier and it handles the delicate C api in a very robust manner.

[mdempsky]

If I comment out the vc_push(vc); call, I still get the same assert failure.

On the other hand, it seems if I wrap each call to vc_query(vc, expr); with an extra vc_push(vc); / vc_pop(vc); pair (following the Python bindings as an example), then it runs without crashing. (Seems calling vc_assertFormula and vc_query at the same scope is problematic?) That's a bit clunky, but I could live with that as a workaround for now if you're not sure what's going wrong.

[msoos]

Yeah, I got that far too, but I don't get it why that's needed. May be a bug, maybe it's by design. Hard to say, the code is a bit difficult to follow.

[WeberAndreas]

I have the same problem:

REMOVED/stp/include/stp/Simplifier/SubstitutionMap.h:159: bool stp::SubstitutionMap::UpdateSubstitutionMapFewChecks(const stp::ASTNode&, const stp::ASTNode&): Assertion `!InsideSubstitutionMap(e0) && "e0 MUST NOT be in the SolverMap"' failed.

My Stack trace:

#0 0x00007ffff5cb49c8 in GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:55
#1 0x00007ffff5cb665a in __GI_abort () at abort.c:89
#2 0x00007ffff5cad187 in __assert_fail_base (fmt=, assertion=assertion@entry=0x7ffff7a8cd58 "!InsideSubstitutionMap(e0) && "e0 MUST NOT be in the SolverMap"",
file=file@entry=0x7ffff7a8cd00 "REMOVED/stp/include/stp/Simplifier/SubstitutionMap.h", line=line@entry=159,
function=function@entry=0x7ffff7a8dfe0 <stp::SubstitutionMap::UpdateSubstitutionMapFewChecks(stp::ASTNode const&, stp::ASTNode const&)::__PRETTY_FUNCTION> "bool stp::SubstitutionMap::UpdateSubstitutionMapFewChecks(const stp::ASTNode&, const stp::ASTNode&)") at assert.c:92
#3 0x00007ffff5cad232 in GI___assert_fail (assertion=assertion@entry=0x7ffff7a8cd58 "!InsideSubstitutionMap(e0) && "e0 MUST NOT be in the SolverMap"",
file=file@entry=0x7ffff7a8cd00 "REMOVED/stp/include/stp/Simplifier/SubstitutionMap.h", line=line@entry=159,
function=function@entry=0x7ffff7a8dfe0 <stp::SubstitutionMap::UpdateSubstitutionMapFewChecks(stp::ASTNode const&, stp::ASTNode const&)::__PRETTY_FUNCTION> "bool stp::SubstitutionMap::UpdateSubstitutionMapFewChecks(const stp::ASTNode&, const stp::ASTNode&)") at assert.c:101
#4 0x00007ffff79ea370 in UpdateSubstitutionMapFewChecks (e1=..., e0=..., this=0x3e25778) at REMOVED/stp/include/stp/Simplifier/SubstitutionMap.h:159
#5 stp::Simplifier::UpdateSubstitutionMapFewChecks (this=0x3e256d0, e0=..., e1=...) at REMOVED/stp/lib/Simplifier/simplifier.cpp:178
#6 0x00007ffff79e043a in stp::RemoveUnconstrained::topLevel_other (this=this@entry=0x7fffffffc1b0, n=..., simplifier=simplifier@entry=0x3e256d0) at REMOVED/stp/lib/Simplifier/RemoveUnconstrained.cpp:664
#7 0x00007ffff79e595e in stp::RemoveUnconstrained::topLevel (this=this@entry=0x7fffffffc1b0, n=..., simplifier=0x3e256d0) at REMOVED/stp/lib/Simplifier/RemoveUnconstrained.cpp:57
#8 0x00007ffff79801b2 in stp::STP::sizeReducing (this=this@entry=0x40db280, inputToSat=..., bvSolver=bvSolver@entry=0x3b46e60, pe=pe@entry=0x3e1f1b0) at REMOVED/stp/lib/STPManager/STP.cpp:207
#9 0x00007ffff7981dde in stp::STP::TopLevelSTPAux (this=this@entry=0x40db280, NewSolver=..., original_input=...) at REMOVED/stp/lib/STPManager/STP.cpp:317
#10 0x00007ffff7985369 in stp::STP::solve_by_sat_solver (this=this@entry=0x40db280, newS=newS@entry=0x3b9d3a0, original_input=...) at REMOVED/stp/lib/STPManager/STP.cpp:74
#11 0x00007ffff798546d in stp::STP::TopLevelSTP (this=this@entry=0x40db280, inputasserts=..., query=...) at REMOVED/stp/lib/STPManager/STP.cpp:127
#12 0x00007ffff7a4ca41 in vc_query_with_timeout (vc=0x40db280, e=0x3e0bb40, timeout_ms=timeout_ms@entry=-1) at REMOVED/stp/lib/Interface/c_interface.cpp:522

I am using:
STP 2.1.1 1fdabf2
Minisat niklasso/minisat@3db5894

Intervace is directly called in the program.

The workaround:

vc_push(x);
res = vc_query(x, e, timeout);
vc_pop(x);

is working for me too.

[TrevorHansen]

This is fixed in 68ea62c