3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 22:35:35 +00:00
z3/src
Leonardo de Moura 2633dc56ab Fix non ASCII character
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-03-24 08:59:43 -07:00
..
api significant update to Horn routines: add module hnf to extract Horn normal form (removed from rule_manager). Associate proof objects with rules to track (all) rewrites, so that proof traces can be tracked back to original rules after transformations 2013-03-23 14:11:54 -07:00
ast missing hnf 2013-03-23 16:56:47 -07:00
cmd_context Add new probes for arithmetic. Check for LIA and LRA (and activate qe if applicable). Modify echo tactic to send results to the regular stream. 2013-02-20 13:41:08 -08:00
math Fix cygwin (with python 2.6) compilation problems. 2013-01-28 17:29:55 -08:00
model Fix bug reported at http://stackoverflow.com/questions/15226944/segmentation-fault-in-z3 2013-03-05 09:04:03 -08:00
muz_qe Fix non ASCII character 2013-03-24 08:59:43 -07:00
nlsat Add nlsat.factor option. This is a workaround for the slow factorization procedure. 2013-01-02 21:18:02 -08:00
parsers Fix uninterpreted sort definition. There was a mismatch in the behavior of the API and SMT front-ends. The SMT front-ends were using user_sorts to be able to support parametric uninterpreted sorts. After this fix, the API also creates user_sorts. 2013-02-12 14:34:31 -08:00
sat exposed sat params 2012-12-02 16:38:33 -08:00
shell make model and proof converters a reference 2013-03-20 10:36:36 -07:00
smt Move ast_counter to location for common utilities. It depends on get_free_vars, so is in rewriter directory 2013-03-19 09:47:52 -07:00
solver Fix memout detected in nightly regressions 2012-12-15 13:26:11 -08:00
tactic Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-03-08 13:22:06 +00:00
test add unit test for previous commit 2013-03-22 11:51:28 -07:00
util significant update to Horn routines: add module hnf to extract Horn normal form (removed from rule_manager). Associate proof objects with rules to track (all) rewrites, so that proof traces can be tracked back to original rules after transformations 2013-03-23 14:11:54 -07:00