Mate Soos

OK, it works as I expected. I added some tests to make this clear. Note that `str_to_cl` is just a helper and "1" in there is `Lit(0, false)` and "-2"...

Yep, assumptions are not being used to deduce zero-level assignments. In case you need how many variables would be propagated given the assumptions, I can create a function for that....

The above works, yes. Note that if you are not using assumptions (i.e. inserting the clauses all the time) then you are probably best off running simplify() **after** you added...

OK, thanks! Note that I can do the assumption stuff in about 20-30 minutes so, don't suffer for that :) Note that if in the real world you'll be adding...

This way seems OK. Note that some variables are better to be asserted -- so check what variables get asserted -- if only some intermediary ones are asserted, maybe that's...

Waaait... we build this thing on Windows on every push :D I fixed this a while ago (it was tons of work too), so it's easy to be sure it...

Hmm... that only broke riss. Riss didn't use the trick of `add_cxx_flag_if_supported("-Wclass-memaccess")` and defining `add_cxx_flag_if_supported` as: ``` include(CheckCXXCompilerFlag) macro(add_cxx_flag_if_supported flagname) check_cxx_compiler_flag("${flagname}" HAVE_FLAG_${flagname}) if(HAVE_FLAG_${flagname}) SET(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flagname}" ) endif() endmacro() ```...

@conp-solutions I agree about the commit-ID stuff, actually :) Can you please add that to the travis-ci script that git clones Riss? It's file "travis-cmake.sh" and the offending code is:...

Thanks for the request! This is very valid... do you know if you could take a shot at it and create a pull request perhaps? Thanks!

First of all ``` >>> S.check() False ``` Means that system has no model. So printing the non-existent model is wrong. The reason it doesn't have a model is that...