mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
8155 commits 23 branches 48 tags 157 MiB
Commit graph

6720 commits

Author SHA1 Message Date
Nikolaj Bjorner d7f9a3b37d fix crash bugs in sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-11 11:27:10 -08:00
Nikolaj Bjorner a6da207b65 fix crash bugs in sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-11 11:25:43 -08:00
Nikolaj Bjorner c522487a86 add iterators to C++ vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-10 16:59:35 -08:00
Nikolaj Bjorner 454e12fc49 update to vector format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-10 15:28:16 -08:00
Nikolaj Bjorner cb7e53aae4 reset backtrack level at each cube 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-09 10:04:32 -08:00
Nikolaj Bjorner ee3ed3a27a Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-11-09 09:55:41 -08:00
Nikolaj Bjorner 700f413e26 updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-09 09:55:37 -08:00
Nikolaj Bjorner bc8681a0ea reset backtrack level after first backtrack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 22:14:59 -08:00
Nikolaj Bjorner 75b8d10f48 add backtrack level to cuber interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 21:44:21 -08:00
Nikolaj Bjorner 0a9946578b use failed literal to asym branching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 09:14:21 -08:00
Nikolaj Bjorner b099449ce1 asymm branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 07:21:49 -08:00
Nikolaj Bjorner 2746528aab fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-07 17:16:36 -08:00
Nikolaj Bjorner 16555d4886 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-11-07 11:30:09 -08:00
Nikolaj Bjorner 1a687a31b6 missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-07 11:29:51 -08:00
Nikolaj Bjorner 34c5ce7f09 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-11-07 11:28:47 -08:00
Nikolaj Bjorner 303157d3b7 allow incremental mode override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 15:00:52 -08:00
Nikolaj Bjorner 6f8ff46ddb Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-11-06 10:03:03 -08:00
Nikolaj Bjorner d97f800390 update error code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 10:02:59 -08:00
Nikolaj Bjorner 5813e22032 fix race condition, exception handling/throwing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 18:24:15 -08:00
Nikolaj Bjorner 9a4fb4ff76 remove ad-hoc parameters, deprecating dimacs cube mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 14:08:55 -08:00
Nikolaj Bjorner 70ee030228 updates to parallel tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 10:53:25 -08:00
Nikolaj Bjorner e46e9cf86d work on parallel-tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-04 15:56:05 -05:00
Nikolaj Bjorner 59ea11b1a3 cube and conquer parallel tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-04 13:40:31 -05:00
Nikolaj Bjorner 6df3e47b07 disable symbol fixing in pretty printer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 09:53:47 -05:00
Nikolaj Bjorner 7c743b3d16 add direct FromFile method to solvers so that model transformations are loaded along with assertions. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 09:25:18 -05:00
Nikolaj Bjorner fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05:00
Nikolaj Bjorner caaf0ba33c model-add/del 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-01 22:32:22 -05:00
Murphy Berzish 2d25355611 Merge remote-tracking branch 'upstream/master' into issue1274-crash 2017-10-31 17:07:54 -04:00
Nikolaj Bjorner 24a44a0b29
Merge pull request #1336 from mtrberzi/clean-rewriter-patch 
fix rewriter in theory_str
 2017-10-31 08:45:14 -07:00
Nikolaj Bjorner 3de8c193ea implementing model updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 16:11:51 -05:00
Nikolaj Bjorner 29d643cc23
Merge pull request #1337 from mtrberzi/fix-length-testing 
Optimizations for length testing in theory_str
 2017-10-30 12:00:47 -07:00
Nikolaj Bjorner 34f24aee72 fix order of instantiation for recursive functions, #1274 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 13:50:31 -05:00
Murphy Berzish 6e31d9c3f5 internalize free var before iterating eqc in theory_str 2017-10-30 14:34:27 -04:00
Murphy Berzish 2ffffa9bed Merge remote-tracking branch 'upstream/master' into fix-length-testing 2017-10-30 14:04:10 -04:00
Murphy Berzish a8d025f5b4 Merge remote-tracking branch 'upstream/master' into HEAD 2017-10-30 13:55:31 -04:00
Nikolaj Bjorner 92b5301b7f adding Cube method to .NET API, removing lookahead and get-lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-29 08:57:24 -07:00
Nikolaj Bjorner 9e20bfe7f9 fix virtual method override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 17:23:35 -07:00
Nikolaj Bjorner 2227db215e fix build break with virtual method override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:58:16 -07:00
Nikolaj Bjorner b556f3ca42 fix stack overflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:41:29 -07:00
Nikolaj Bjorner 2774d6896b fix variable naming bug for internal (fresh) constants clashing with external names 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:11:29 -07:00
Nikolaj Bjorner e4b595d490 add solver pool abstraction for Spacer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:10:20 -07:00
Nikolaj Bjorner ba53fc1230 fix scc omitting blocked clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-27 17:29:26 -07:00
Nikolaj Bjorner 2a8a28bb59 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-27 15:41:24 -07:00
Nikolaj Bjorner 829c140087 ensure that bca takes also lemmas into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-27 15:40:25 -07:00
Miguel Angelo Da Terra Neves f1bad91609 Clean-up 2017-10-27 12:39:36 -07:00
Miguel Angelo Da Terra Neves 3a05313c67 Python API context fix 2017-10-27 12:36:09 -07:00
Nikolaj Bjorner c886b6d500 fix #1330. Interpolation transformation needs to handle TRANSITIVITY_STAR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 20:53:10 -07:00
Nikolaj Bjorner e7aa6455bc fix #1326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 19:25:25 -07:00
Nikolaj Bjorner 0589a20b46 fix #1326 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 19:24:45 -07:00
Miguel Angelo Da Terra Neves 8bb2be1fba Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-25 17:08:10 -07:00
Miguel Angelo Da Terra Neves e1ff6304ed Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-25 17:06:08 -07:00
Nikolaj Bjorner 0919fd4075 fix bca condition for tautology check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 16:46:22 -07:00
Nikolaj Bjorner ac0202630e fix non-termination bug with retained clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 15:40:11 -07:00
Nikolaj Bjorner 32711790e8 bug fixes reported by Miguel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 13:36:48 -07:00
Nikolaj Bjorner 0268f2243e remove ast.h reference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 09:49:53 -07:00
Nikolaj Bjorner f5f1d019d8 missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 09:00:35 -07:00
Nikolaj Bjorner 371f0b193c move min_cut, fix #1321 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 02:59:04 -07:00
Nikolaj Bjorner 8acc924c21 ifndef/define match 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 16:34:49 -07:00
Miguel Angelo Da Terra Neves 4d9492176e Removed incremental disabling 2017-10-24 15:19:45 -07:00
Nikolaj Bjorner b72225d7d0 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 15:16:59 -07:00
Miguel Angelo Da Terra Neves 8915d0a21f Tidy 2017-10-24 14:08:44 -07:00
Miguel Angelo Da Terra Neves 80041d7131 Fixed infinite loop bugs in blocked clause retention. Added option to 
disable incremental sat solver
 2017-10-24 13:51:27 -07:00
Nikolaj Bjorner ee320fa025 fix build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 13:32:40 -07:00
Nikolaj Bjorner 31dfc0c610 fix build, fix #1322 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 13:20:19 -07:00
Nikolaj Bjorner 6300a78b82 more build errors in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 12:57:30 -07:00
Nikolaj Bjorner 48d144a6dd missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 12:51:47 -07:00
Nikolaj Bjorner db65cc007a move more proof utils 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 10:27:48 -07:00
Nikolaj Bjorner fc822af707 move proof utils under ast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 09:59:55 -07:00
Nikolaj Bjorner f6ee6894c7 fix bugs related to reading configuration flags 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 09:59:23 -07:00
Nikolaj Bjorner 1315c8d7de rename repeated class apart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 09:03:28 -07:00
Nikolaj Bjorner 2c3b56315d Merge branch 'master' of https://github.com/z3prover/z3 2017-10-24 08:49:56 -07:00
Nikolaj Bjorner 637a0fa139 unused warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 08:49:25 -07:00
Christoph M. Wintersteiger eda3c6258b backward comp 2017-10-24 12:53:24 +01:00
Nikolaj Bjorner e6e1d94cf9 fix build issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:39:00 -07:00
Nikolaj Bjorner bce143b2b2 Merge pull request #1323 from c-cube/pp-proof-graphviz 
print proofs in graphviz
 2017-10-24 03:28:04 -07:00
Nikolaj Bjorner 70f7846af5 move spacer_marshal to under parsers/smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:18:59 -07:00
Nikolaj Bjorner d67f3c1466 create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:08:56 -07:00
Simon Cruanes 607eba1720 account for review 2017-10-24 11:44:28 +02:00
Nikolaj Bjorner 72c9134424 fixing regressions introduced when reducing astm proof dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 02:26:39 -07:00
Simon Cruanes ed526b808d add parameter to specify the file into which dot proofs are to be printed 2017-10-24 10:16:56 +02:00
Simon Cruanes 24edb8fb47 add some colors to the proof output 2017-10-24 09:51:47 +02:00
Simon Cruanes d630838b38 add a basic printer into graphviz (http://graphviz.org/) for proofs 
- proofs are output into file `proof.dot` if `(get-proof-graph)` is
  in the input
- use `dot -Txlib proof.dot` to see the proof
- use `dot -Tsvg proof.dot` to get a svg file
 2017-10-24 09:41:38 +02:00
Nikolaj Bjorner 7f254710aa patch build failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-23 21:38:10 -07:00
Nikolaj Bjorner f63439603d streamlining proof generation (initial step of removing ast-manager dependency). Detect error in model creation when declaring constant with non-zero arity. See #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-23 21:16:46 -07:00
Murphy Berzish 5e19e905fa Merge remote-tracking branch 'upstream/master' into fix-length-testing 2017-10-23 17:59:54 -04:00
Miguel Angelo Da Terra Neves 63545c1e7b Fixes 2017-10-23 12:51:19 -07:00
Nikolaj Bjorner 77bbae65f5 fix #1319, fix #1320 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-23 08:17:38 -07:00
Nikolaj Bjorner ee6cfb8eef updates to simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-23 01:00:06 -04:00
Nikolaj Bjorner 1a859d4591 Merge branch 'master' of https://github.com/z3prover/z3 2017-10-21 18:56:50 -04:00
Nikolaj Bjorner 42fbe19814 fix #1316, segmentation fault when numeric value is not internalized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-21 18:56:36 -04:00
Nikolaj Bjorner 183bad69c8 Merge pull request #1315 from mtrberzi/str-equals-str-bug 
Add special case handling for theory_str constant backpropagation
 2017-10-21 15:47:14 -07:00
Nikolaj Bjorner b2191cab02 disable eager clear of check-sat-result to fix #1318 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-21 18:46:35 -04:00
Nikolaj Bjorner 42749e7b22 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-19 22:19:12 -07:00
Nikolaj Bjorner 76eed064eb bug fixes, prepare for retaining blocked clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-19 22:19:05 -07:00
Miguel Neves d58f42c821 Merge 2017-10-19 20:02:05 -07:00
Miguel Neves 3dd5630255 Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-19 19:53:25 -07:00
Miguel Neves ba6b024ac4 Reverted to March_CU like lookahead 2017-10-19 19:52:56 -07:00
Murphy Berzish ce1c8f7be2 remove debug code 2017-10-19 17:01:10 -04:00
Nikolaj Bjorner d2e27f6f1f remove redundant and wrong range type, in extension to changes made for #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-19 11:25:44 -07:00
Nikolaj Bjorner c9f540b066 additional array functions exposed over API, ping #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-19 11:08:48 -07:00
Nikolaj Bjorner 636f740b1a fixup bdd reordering, assertions and perf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 19:32:49 -07:00
Nikolaj Bjorner 553bf74f47 testing bdd for elim-vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 17:38:39 -07:00
Nikolaj Bjorner dc6ed64da1 testing bdd for elim-vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 17:37:38 -07:00
Murphy Berzish abdb41c5df add special case handling for string constant backpropagation in theory_str 
avoid a crash when asserting that a constant string is equal to itself
by not generating this assert in the first place
 2017-10-18 16:09:10 -04:00
Nikolaj Bjorner 6155362571 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-18 08:57:43 -07:00
Nikolaj Bjorner edea879864 expose missed propagations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 08:57:32 -07:00
Nikolaj Bjorner 80f24c29ab debugging reordering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 08:52:03 -07:00
Nikolaj Bjorner 8811d78415 compress elimination stack representation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 21:28:48 -07:00
Miguel Neves cf2512ce90 Added literal promotion 2017-10-17 16:03:58 -07:00
Nikolaj Bjorner e0e7836c12 working on BDD reordering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 14:20:49 -07:00
Nikolaj Bjorner 4944a86478 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-17 13:25:21 -07:00
Nikolaj Bjorner 43f8214453 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 13:25:08 -07:00
Nikolaj Bjorner f39a4ece0d Merge pull request #6 from TheRealNebus/opt 
Lookahead clause size optimization. Fixed some missing propagations
 2017-10-17 13:22:40 -07:00
Miguel Neves 806690571e Lookahead clause size optimization. Fixed some missing propagations 2017-10-17 13:15:34 -07:00
Nikolaj Bjorner 7f590b5419 gift for Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 10:27:58 -07:00
Nikolaj Bjorner 448cf8c31d fix scope accounting for dom simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 10:14:26 -07:00
Nikolaj Bjorner 42e9a0156b add elimination stack for model reconstruction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 04:52:06 -07:00
Nikolaj Bjorner da4e8118b2 adding elim sequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 17:58:56 -07:00
Nuno Lopes 4e92caa553 nnf: let's try a different version of compatible frames wo/ copying 2017-10-16 22:33:23 +01:00
Christoph M. Wintersteiger 01f642a6f3 Backward compatibility 2017-10-16 18:19:55 +01:00
Nikolaj Bjorner 019edcb822 frame, again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:35:00 -07:00
Nikolaj Bjorner 5f9891c235 moving out construction of expr_ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:29:26 -07:00
Nikolaj Bjorner a93f1f88cc trying to fix mac build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:23:50 -07:00
Nikolaj Bjorner 256c9d76d3 add macro for _Exit under WINDOWS 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:14:10 -07:00
Nikolaj Bjorner b36f512879 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 09:07:44 -07:00
Christoph M. Wintersteiger a10ad79f2b Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 17:07:10 +01:00
Christoph M. Wintersteiger f9adf8e62a Backwards compatibility 2017-10-16 17:07:03 +01:00
Nikolaj Bjorner d9ccb3928e fix debug build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:05:25 -07:00
Christoph M. Wintersteiger cda03b4238 Whitespace 2017-10-16 17:01:09 +01:00
Christoph M. Wintersteiger 0169417c64 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 16:40:39 +01:00
Dan Liew dbb7f616c1 More LSan workarounds. 2017-10-16 08:56:17 +01:00
Dan Liew 35f6746c60 Workaround regressions/smt2/error.smt2 test timing out. 
When ASan's LeakSanitizer is enabled leak checking is triggered
when `exit()` is called and it returns so many false positives that
it takes a long time to write them to the console.

To workaround this we simply call `_Exit()` instead.
 2017-10-16 08:56:17 +01:00
Nikolaj Bjorner 00a401260e fixing cce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-15 21:19:02 -07:00
Nikolaj Bjorner b63754e362 adding explicit assignment for auto-generated function. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-15 21:16:54 -07:00
Nuno Lopes 2905bdebef make vector friendly to gcc < 5 2017-10-16 00:54:31 +01:00
Nuno Lopes 6cefb700ac add move constructor to ref_vector 2017-10-16 00:54:31 +01:00
Nuno Lopes 82b25a0608 add move constructor to watch_list 2017-10-16 00:54:31 +01:00
Nuno Lopes d18e975a49 vector: make expand_vector() less prone to mem leaks by calling the destructors after move 2017-10-16 00:54:30 +01:00
Nuno Lopes e7f0f3b834 add move constructor to obj_ref 2017-10-16 00:54:30 +01:00
Nuno Lopes 29acec672f nnf: remove ast incref 2017-10-16 00:54:30 +01:00
Nuno Lopes 6c2d0394ac add move constructor to rational 2017-10-16 00:54:30 +01:00
Nuno Lopes 912a729097 fix build of unit tests 2017-10-16 00:54:30 +01:00
Nuno Lopes 468e0207f7 add move constructor to mpf 2017-10-16 00:54:30 +01:00
Nuno Lopes d1c13f17b0 remove noexcept since MSVC 2012 doest support it 2017-10-16 00:54:30 +01:00
Nuno Lopes b53d69be18 fpa_rewriter: remove a mpq copy 2017-10-16 00:54:30 +01:00
Nuno Lopes 3cc6dd1cbd bv_decl_plugin: remove mem allocation 2017-10-16 00:54:29 +01:00
Nuno Lopes d30a099cd0 fix crash in vector::expand() 2017-10-16 00:54:29 +01:00
Nuno Lopes 27e84c5ffc mpz.h: fix typo in previous commit (found by Nikolaj) 2017-10-16 00:54:29 +01:00
Nuno Lopes 9b54b4e784 fix vector<> to support non-POD types 
adjust code to std::move and avoid unnecessary/illegal
 2017-10-16 00:54:29 +01:00
Nikolaj Bjorner 9f9ae4427d add cce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-15 15:13:43 -07:00